Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Networks of queues model systems in which jobs visit a sequence of service stations: items in a manufacturing job-shop, packets in a communication network, patients moving between hospital departments. The open migration process of Chapter 2 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979), and the job-shop networks of Jackson (Jackson 1963) route a customer leaving a queue at random, independently of where he has been. That rules out the most common situation in practice: an item that has passed machines 1 and 3 must next go to machine 4, while an item that has passed machines 2 and 3 must go to machine 5.
Section 3.1 of the book removes this restriction. Customers are divided into types, a type fixes a deterministic route through the queues, and a stochastic routing rule is recovered by using one type per possible route. Within each queue, the order of service is described by two position-dependent functions, which cover first-come first-served -server queues, last-come first-served, processor sharing and service in random order. Theorem 3.1 states that, for every such network, the equilibrium distribution is a product of explicit single-queue factors. This is the result behind the "Kelly network" and "Kelly-type queue" terminology of later work (Kelly 1975; Baskett, Chandy, Muntz, Palacios 1975).
There are customer types and queues. Customers of type enter the system in a Poisson stream of rate and visit the queues in that order before leaving; two successive stages of a route are at different queues.
Queue holds its customers in positions . Each customer needs an exponentially distributed amount of service with unit mean. The queue supplies total service effort at rate , with for ; a proportion goes to the customer in position . An arriving customer takes position with probability . For each , and are probability vectors on .
The class of the customer in position of queue is , his type and the stage of his route. The state of queue is and the state of the network is . Its transition rates , displays (3.1)–(3.6), are the sums of the intensities of all events taking to : a departure from the system (intensity ), a move from position of queue to position of the next queue (intensity ), and an arrival into position of the first queue of a route (intensity ).
With if and otherwise, set
If every series defining converges, then
is positive, sums to over all network states, and satisfies the equilibrium equations
Theorem 3.1 gives the full joint law of a network in which routes carry memory, and its corollaries turn it into usable performance formulas: each queue behaves, in its marginal law and as seen by arriving customers, like an isolated queue fed by a Poisson stream of rate , even though the actual arrival stream at queue is not Poisson. Mean sojourn times along a route then follow from Little's result. Theorem 3.2 identifies the reversed process as a network of the same kind; it is the source of the departure-stream results (Corollary 3.3) and of the arrival theorem (Corollary 3.5). Lemma 3.13 isolates the condition (3.26) under which state-dependent arrival rates preserve the product form (Theorem 3.14).
The results are classical and proved in the book. None of them has a machine-checked proof: the Prove2Me catalogue holds the rate-level theorems for migration processes (Chapter 2 of Kelly–Yudovina), and open targets for the BCMP and Jackson models, which have different state descriptions. This mission adds a formal model of the position-structured multiclass network itself, with the summation over coinciding transitions that (3.2), (3.4) and (3.6) require, and product-form, reversal and arrival-theorem statements over it.
The obvious first attempt, detailed balance, fails: and differ in general, because a customer's route cannot be run backwards inside the same network ( is usually when ). The equilibrium equations therefore involve, for each state, all its predecessors at once. The rates are themselves sums over coinciding transitions, so a statement about individual events does not transfer to the rates without accounting for which positions lead to the same successor state. In Lean this brings in insertion into and deletion from position lists, the relabelling of stages, and the normalization of a product over a countable space of -tuples of lists, reorganized by queue length together with the identity .
Fin I, queues Fin J; the book allows countably many types with . A network state is a function assigning to each queue a list of classes with ; the state space is countable and all sums over it are tsum/HasSum.KellyStochasticNetworks.FullBalance). The existence of the Markov process, irreducibility and non-explosion are not formalized. "The reversed process" (Theorem 3.2) is read through the reversed rates ; "the probability he finds" (Corollary 3.5) is read as a ratio of equilibrium arrival fluxes; quasi-reversibility is its rate characterization (3.8), (3.10).tsum, which Lean sets to for a divergent series; every theorem assumes the series converges, the book's "none of is zero".Infrastructure that a complete development needs: list insertion/deletion lemmas for position bookkeeping, sums of products over , and a bijection-of-events argument for summed rates. The quasi-reversibility predicate and the reversed-rate apparatus are reusable for the closed networks of §3.4 and the symmetric queues of §3.3. Contributions are welcome on any milestone, in any order.
The classical product-form results for queueing networks (Jackson, Kelly, Baskett–Chandy–Muntz–Palacios) assume exponentially distributed service requirements, because then the state of a queue need not record how much service each customer has received. Real service times are rarely exponential: telephone call lengths, job sizes in time-shared computers and web transfers are far from it. Symmetric queues, introduced in §3.3 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979), form the class of single queues for which the stationary distribution of the number of customers, and of their classes, depends on the service requirement distribution only through its mean. This property, insensitivity, is what makes Erlang's loss formula valid for arbitrarily distributed call lengths (Kelly, p. 79), and it is the reason processor-sharing, last-come-first-served preemptive and infinite-server stations may appear with general service in product-form networks.
Timeline. Sevastyanov (1957) proved that Erlang's loss formula holds for arbitrarily distributed call lengths. Kelly (1975, 1976) introduced queues with customers of different types whose effort and arrival-position functions coincide, and showed product form for networks of them with non-exponential service built from exponential stages; Barbour (1976) extended the method of stages; Baskett, Chandy, Muntz and Palacios (1975) gave product form for networks containing processor-sharing, LCFS-preemptive and infinite-server stations with phase-type service. Kelly's 1979 book presents the symmetric queue in the form formalized here.
A symmetric queue holds customers in positions , where is the number present. It operates as follows (Kelly, p. 72):
Server-sharing (), the stack (, last come first served preemptive), the queue with no waiting room and the infinite-server queue are examples (pp. 73–74).
Customers of class arrive in a Poisson stream of rate . On arrival a class- customer receives a refined class with probability , , and then needs independent stages of service, each exponentially distributed with mean . The class- service requirement is therefore a mixture of gamma distributions with mean
and the work arriving per unit time is . The record of the customer in position is , the stage in progress, and is a Markov process. Its transitions are: an arrival of class into position at stage , at rate ; and, at rate , completion of the current stage of the customer in position , which moves him to the next stage or, after stage , out of the queue. The normalizing constant is
When (3.15) converges, the distribution
is the equilibrium distribution of , and under it
and the queue is quasi-reversible with respect to the classification and to : from every state, the rate of arrivals of each class does not depend on the state, both for the process and its time reversal (relations (3.8) and (3.10) of p. 67).
Theorem 3.8 gives the stationary law of a symmetric queue in closed form and shows that it depends on the service requirement distributions only through their means . Quasi-reversibility (part (iii)) is the property that lets symmetric queues be placed in networks: Kelly's §3.2 shows that a network of quasi-reversible queues has a product-form equilibrium, so Theorem 3.8 is the single-queue input to product-form networks with processor-sharing, LCFS-preemptive and infinite-server stations and class-dependent, non-exponential service. Lemma 3.9 is the approximation step behind the extension to arbitrary service distributions (Theorem 3.10).
These results are classical and proved in the book. To our knowledge none of them is machine-checked; Mathlib has the gamma distribution and distribution functions but no queueing theory. The mission produces a formal model of the symmetric queue as a countable-state Markov process, its equilibrium distribution, the insensitive marginals and the rate characterization of quasi-reversibility, all reusable by the chapter on networks of quasi-reversible queues.
The obvious first attempt, detailed balance, fails: the stage process is not reversible in general, since an intermediate stage completion has no transition back. The equilibrium equations must be verified in full, over a countable state space in which a single state is reached from infinitely many others. The symmetry condition is essential and must enter the argument: without it (for first-come-first-served, say) the distribution (3.18) is false for non-exponential service. Positions shift on every arrival and departure, so the bookkeeping of which list results from which event, including coincidences when neighbouring customers have identical records, is the main formal burden. The marginal computations sum (3.18) over lists of records, where convergence must be tracked, and Lemma 3.9 needs an explicit construction of approximating gamma mixtures.
List of customer records (class, refined class, stage); list index is position , and , keep the book's -based indexing. The state space consists of the lists whose records have and : records of a refined class arriving at rate zero are unreachable and excluded.HasSum or tsum with explicit convergence hypotheses: (finite exit rates, the book's standing assumption of §1.1), convergence of , of , and of (3.15). "Equilibrium distribution" means positive, summing to one, and satisfying the equilibrium equations with convergent series.Welcome contributions: proofs of the milestones, lemmas about List.insertIdx/List.eraseIdx bookkeeping for queues with positions, and summation over lists of records.
Periodic-review inventory control with backorders is one of the basic models of operations research: in each period a manager decides how much to order, orders arrive after a lead time, unmet demand is backlogged at a penalty, and stock left over is charged a holding cost. When demands in different periods are independent, dynamic programming yields an optimal base-stock policy and computing it is tractable. In practice demands are correlated and forecasts evolve over time, for example under the martingale model of forecast evolution (Heath and Jackson, 1994, doi:10.1080/07408179408966604). The dynamic program then has to range over all possible information states, whose number is typically exponential in the input (Zipkin, 2000), so optimal policies are out of reach and the heuristics in use came without performance guarantees.
Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2):284–302, 2007) gave the first policy for this model with a worst-case guarantee that holds for arbitrary correlated, nonstationary demand distributions: the dual-balancing policy costs at most twice the optimum in expectation. The analysis rests on a marginal cost accounting that charges each order, at the time it is placed, all the holding cost its units will ever incur. This mission formalizes that guarantee.
There are periods and a known lead time : an order placed in period arrives in period . Period has a per-unit holding cost and a per-unit backlogging penalty . Ordering costs are zero (), which is the standing assumption of the paper's §4. The initial data are the net inventory and the pipeline orders .
Demands are nonnegative random variables on a probability space with a filtration ; is the information at the beginning of period , and is -measurable. A feasible policy places orders that are -measurable. Write (with for ), for the inventory position before ordering and after ordering.
The marginal holding cost of period is the holding cost that the units ordered in incur until the end of the horizon, and the marginal backlogging cost is the penalty incurred one lead time later:
The cost of is ; by Eq. (3) it differs from the total holding and backlogging cost only by a policy-independent nonnegative term.
A dual-balancing policy orders nothing after period , and in each period orders the quantity that balances the two conditional expected marginal costs:
For every dual-balancing policy and every feasible policy ,
The paper writes ; quantifying over all feasible is the same statement whenever an optimum exists and needs no existence assumption.
Two further items are not milestones. Eq. (3) states that, along every realization, the period-by-period holding and backlogging cost equals , which is why the cost of Eq. (4) is the right objective. The other states that a dual-balancing policy exists when and the demands are integrable, so the goal is not about an empty class.
The theorem gives a policy that is computable period by period, by a one-dimensional search, with a factor-two guarantee that holds for every joint demand distribution, including correlated, nonstationary and forecast-driven ones, where the optimal policy cannot be computed. The constant is tight: the paper exhibits instances where the ratio tends to two. The second mission of this series treats the stochastic lot-sizing problem of the same paper, which uses the same marginal cost accounting.
The result is proved in the paper; no machine-checked proof of it is known. Formalizing it produces a reusable model of the periodic-review backlogging system with lead times and adapted policies, a verified marginal cost identity, and a formal approximation guarantee for a stochastic inventory policy. The pathwise comparison lemmas are stated for arbitrary pairs of order sequences and so apply to other balancing-type policies.
The obvious attempt compares the two policies period by period. That fails: in a given period the dual-balancing policy may hold far more or far less inventory than the comparison policy, and neither the holding nor the backlogging cost of one period is bounded by the comparator's cost in that period. The comparison only works after re-charging holding costs to the period in which the units were ordered, which requires the identity Eq. (3) to be established exactly, including the pipeline units, the initial stock and the lead-time shift. The probabilistic step then needs the random index sets and to be determined by the information of period , so that conditioning on commutes with the indicators; this is where the nonanticipativity of both policies enters. The existence of a balancing quantity needs a measurable selection from conditional laws, and it fails without a positive late holding cost.
ℤ). Orders and demands are functions ℤ → Ω → ℝ; only periods are read, and the pipeline is substituted for .Filtration ℤ to which demands are adapted with a one-period lag; the paper's information vectors are a special case, and randomized policies are covered when their randomness is part of the information.A complete development needs finite-sum manipulations for Eq. (3) and Lemma 4.2, conditional expectation (tower property, pulling out bounded -measurable factors) for Lemma 4.1 and the goal, and regular conditional distributions with a measurable selection for the existence item. Theorem 4.2 (the randomized policy for integer demands) is outside this mission.
The stochastic multi-armed bandit is the basic model of sequential decisions under uncertainty with partial feedback: a forecaster repeatedly picks one of options and observes only the reward of the option it picked. It models clinical trials, ad placement, routing and dynamic pricing, and is the building block of many reinforcement-learning algorithms. The question is how much reward is lost, compared with always playing the best option, through having to learn which option is best.
Chapter 2 of Bubeck and Cesa-Bianchi's monograph (arXiv:1204.5721v2) answers this for upper confidence bound (UCB) strategies.
There are arms. Arm has an unknown reward distribution with mean . At each round the forecaster selects an arm based on the past and receives a reward drawn from , independently of the past. Write , for the gap of arm , and for the number of times arm is selected in rounds . The pseudo-regret is
Moment condition (2.2). There is a convex with and for all and every arm's reward . Its Legendre–Fenchel transform is . For rewards one may take , for which .
-UCB. With the mean of the first rewards of arm , at round select
If the rewards satisfy (2.2), then -UCB with satisfies, for every ,
This is the bound the book's proof establishes. The printed statement has in place of ; see Formalization scope.
Theorem 2.1 says that the cost of learning grows only logarithmically in the horizon, with a constant set by how well each suboptimal arm can be told apart from the best one. Theorem 2.2 shows that, up to constants, this cannot be improved: for Bernoulli rewards any strategy that is good on every instance must pay per suboptimal arm, with constant . By (2.8) this constant is at least of order , matching (2.4). Together they are the template for the analysis of most optimistic algorithms: KL-UCB, linear and contextual UCB, and UCB-style reinforcement learning.
All results of the chapter are classical and proved on paper. This mission makes them machine-checked in a common model. That model has an explicit pseudo-regret, an explicit (generalized) inverse of , an explicit initialization rule for the algorithm, and a randomized-strategy model for the lower bound. Later chapters of the series and later papers on optimistic algorithms can build on it.
The deterministic part of the upper bound is short, so the main difficulty is probabilistic. The sample mean is taken over a random number of samples that depends on the algorithm's past. A Chernoff bound for a fixed sample size does not apply to it directly. The proof needs a union bound over all possible sample sizes, together with the representation in which the -th reward of each arm is a fixed random variable. Summing the resulting tail over rounds is where enters.
The lower bound needs a change-of-measure argument between two Bernoulli instances, applied to a forecaster that may be randomized and never knows the horizon. Expressing "the forecaster cannot distinguish the instances" requires the law of the whole interaction under two environments.
Model. Arms are Fin K with , rounds are , and the natural logarithm is used. Rewards are a stack: is the reward of the -st pull of arm , all mutually independent, identically distributed per arm. For every strategy this gives the same law of arms and rewards as the book's protocol. , and are the published definitions of ImprovedLinBandits.UCBDelta.armModel. The pseudo-regret is (2.1), , not the expected regret. The arms played are measurable random variables, so that every expectation is genuine.
and its inverse. takes values in the extended reals. .
Algorithm. The index is undefined while . Unplayed arms are therefore played first, so each arm is played once in rounds . Ties are broken arbitrarily.
Corrected misprint. The book prints Theorem 2.1 with constant term . Its proof yields (bound on times ). The printed form is false for Gaussian rewards with large gaps. The goal states the proof's version. (2.4) is correct as printed because .
Constants. No O(·) appears in the chapter's statements. The constants are the book's: in Theorem 2.1 and (2.4), and the factor in (2.4) and (2.8).
Conventions made explicit.
Conventions 1–3 hold for every the book uses.
Theorem 2.2. The forecaster is a measurable rule from the history and a fresh uniform seed to an arm. It does not depend on the horizon. Consistency is required on every Bernoulli instance, every suboptimal arm and every . A term with () is , and the is taken in the extended reals. The book proves only .
Ruled out. The algorithm cannot see unplayed rewards (its index uses only the sample means of rewards already received). Non-measurable arm choices, which would make the expectations vanish in Lean, are excluded. Consistency cannot be assumed only on the instance of the conclusion.
Needed infrastructure. Cramér–Chernoff bounds for sums of i.i.d. variables, Hoeffding's lemma, the stack representation of bandit interactions, and the divergence decomposition for randomized strategies. All are reusable beyond this mission, and contributions of any of them are welcome.
A revenue-sharing contract lets a supplier charge a retailer a wholesale price per unit and, in addition, collect the share of the retailer's revenue. The video-rental industry adopted such contracts at scale in the late 1990s, and Cachon and Lariviere showed that in a broad class of models they coordinate the supply chain: the retailer's privately optimal decisions coincide with those that maximize total channel profit, and the profit can be split arbitrarily between the firms (missions 1 and 2 of this series).
The same authors also studied where revenue sharing breaks down. The most practically relevant limitation is retailer effort: shelf space, service, store cleanliness and promotion raise demand, cost the retailer money, and cannot be written into a contract. Once the retailer gives away part of its revenue, it earns only a share of the return on its effort while still paying the whole cost. This mission formalizes Section 4.2 of the authors' working paper, which shows that revenue sharing then cannot coordinate the channel while leaving the supplier any profit, and, in an explicit linear-demand example, determines exactly when the supplier is better off with the plain wholesale-price contract.
The source is the June 2000 working paper (Cachon and Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations), whose results are displayed claims inside numbered sections rather than numbered theorems; the milestones cite section, printed page and display. The published version appeared in Management Science 51(1), 2005.
General model (Sec. 4.2.1). A supplier produces at unit cost . The retailer chooses an order quantity and an effort level after observing the contract . Expected revenue is continuous, differentiable, strictly increasing in and concave in ; effort costs the retailer , where is continuous, increasing, differentiable and convex with . The profits of the integrated channel, the retailer and the supplier are
The integrated solution maximizes over .
Linear example (Sec. 4.2.2). Inverse demand is with an effort-impact parameter , revenue is and effort costs . For a share the supplier's profit when the retailer responds optimally to is , and the supplier's optimal profit is
The share is the wholesale-price contract.
For , and every , the supremum defining is attained at the price , and
Consequently is strictly increasing on if (the wholesale-price contract is the supplier's unique best share), constant if , and strictly decreasing if , with as .
The general result (milestones 1–2) is a clean impossibility statement: with non-contractible effort, the only contract in the revenue-sharing family that coordinates the channel is the wholesale-price contract at marginal cost, which leaves the supplier zero profit. It marks the boundary of the coordination results of the earlier sections, and contrasts with the price-dependent newsvendor, where revenue sharing does coordinate price and quantity because the cost of expanding demand is captured in the revenue function and shared by both firms.
The example turns the impossibility into a design rule. Because coordination is out of reach, the supplier compares contracts by her own profit, and the threshold separates two regimes: when effort matters a lot she should leave the retailer all revenue and charge only a wholesale price ("a smaller share of a larger pie"); when it matters little she should take as much revenue as possible. The same threshold governs the counterintuitive comparative static that the integrated channel's retail price falls as production cost rises.
All results are proved on paper in the source. None has a machine-checked proof; this mission produces the first. The example is a fully explicit two-stage optimization problem, so the formal development also yields a verified computation of a Stackelberg equilibrium with moral hazard that other contract-design missions can reuse.
The individual calculations are elementary, and the work lies in getting the optimization statements right. The page solves the retailer's problem sequentially (effort first, then quantity) and writes the supplier's objective by substituting closed forms. A faithful proof must instead show that these closed forms are global optima over the constrained domains: the retailer optimizes jointly over the quadrant , the corner is optimal whenever , and the supplier's objective is a quadratic on glued to the zero function on , which is not concave on all of . The first-order-condition argument of the general model similarly needs an interior integrated optimum and a strictly positive marginal effect of effort, which "strictly increasing in " alone does not provide.
All quantities are real numbers. The general model is a structure RevShareCoord.Effort.Model carrying , its partial derivatives, , and ; derivatives are one-sided within , and joint differentiability of is replaced by its partial derivatives and joint continuity. The example lives in RevShareCoord.Effort.Linear. "Optimal" always means a maximizer over the whole admissible set ( for the retailer, for the supplier), and the supplier's value is defined as the supremum of her attainable profits, not by the printed formula.
Deviations from the page, each disclosed in the item's Formalization Note:
Plugging the printed into and comparing across would turn the dichotomy into a statement about an arbitrary price schedule; the goal instead asserts that attains the supremum over all , with the retailer best-responding jointly in .
No external library beyond Mathlib's real analysis and convexity is needed. Contributions welcome: proofs of the milestones, reusable lemmas on maximizing strictly concave quadratics over orthants, and a generalization of milestone 2 to non-interior optima.
Temporal-difference learning estimates the value of a policy from observed state transitions and rewards. In a finite Markov decision process, fixing a policy produces a Markov chain, so policy evaluation becomes the task of estimating the expected return from each state. Bradtke and Barto's 1996 paper introduced a least-squares temporal-difference method, LS TD, that uses each observed transition in a linear system instead of selecting a learning-rate schedule. Their Theorem 1 states probability-one convergence for trials that end at absorbing states under explicit conditions on state access, rewards, and features. This mission formalizes that result and the statements the authors use to reach it. Bradtke and Barto, 1996.
The result matters for episodic policy evaluation: a learner may collect many short trajectories, each begun from a prescribed start distribution, and update the same estimate as data accumulate. The theorem identifies conditions under which the limit is the true value parameter even when the discount factor is one. That endpoint is useful for undiscounted tasks ending in an absorbing goal state; it also makes the convergence claim more delicate than the standard discounted case. The paper proves the result mathematically. The Lean statements in this mission are targets for machine-checked proofs, not claims of proofs already present in Mathlib. Bradtke and Barto, Theorem 1, pp. 43–44.
Let be a finite, nonempty set of states. After a policy is fixed, is the probability of a transition from to , so each row of is nonnegative and sums to one. A transition earns a deterministic real reward . A state is absorbing when ; let be the absorbing states and the others. The chain is absorbing when some absorbing state can be reached with positive probability from every state. A start distribution gives the state at the beginning of each trial. No state is inaccessible when every state can be reached from the positive support of .
For a discount , the expected immediate reward is . The true value function is defined by the expected return
A feature vector represents state . The matrix has row equal to . The target parameter is a vector for which at every state; it is something the theorem must establish, not an input chosen by a formula. Equation (11) forms an LS TD estimate from the observed feature differences and rewards. Bradtke and Barto, §2, Table 1, Eq. (11).
Figure 2 collects trials. Each starts from , follows while the current state is non-absorbing, and ends upon entry into . The next trial starts with a fresh draw from . The estimator includes transitions taken within trials; a draw that starts the next trial is not an observed transition for Eq. (11). Bradtke and Barto, Figure 2, p. 42.
If every state is accessible from , rewards between absorbing states vanish, the feature vectors on are linearly independent, features on are zero, , and , then the expected-return series converges and there is a parameter satisfying
The theorem keeps the paper's endpoint . The return series' convergence is explicit because a real infinite sum in Lean has a default value when it diverges. Bradtke and Barto, Theorem 1, p. 43.
The milestone list follows the statements used in the paper: almost-sure visits and departure proportions for the trials; invertibility of the non-absorbing block of ; invertibility of for positive non-absorbing weights; Lemma 5's probability-one limit ; and Eq. (12), , together with finiteness of the true parameter. Here . Bradtke and Barto, Lemma 5, p. 43; Proof of Theorem 1, p. 44.
Theorem 1 identifies the target of the asymptotic LS TD estimate: the value function defined from rewards, rather than merely a vector satisfying a sampled linear system. It covers an undiscounted absorbing chain, where a general fixed-point equation for values would fail to determine the values of absorbing states. The zero-reward and zero-feature conditions determine that boundary correctly. The result also explains the dimension condition: one independent feature vector for each non-absorbing state permits exact representation of the return. Bradtke and Barto, pp. 43–44.
A complete formal development would connect finite-state stochastic-process laws, visit frequencies, matrix limits, and the return-defined value function in one checked statement. The reusable parts include a finite row-stochastic chain model, a path-law description of restarts, a filtered least-squares estimator, and results about transient blocks of stochastic matrices. The paper's mathematical proof exists; this mission asks for formal proofs of its Lean targets. It also leaves room for alternative proofs and sharper, separately stated variants without weakening Theorem 1.
Ordinary matrix convergence cannot be applied until the observed transition frequencies are known to converge and the limiting matrix is invertible. A trial has random length, and the process resets after absorption, so a sequence indexed by all restart-process steps does not have the same raw state proportions as a count indexed by trials. The proof must account for both clocks while retaining the in-trial data of Eq. (11). At , a direct geometric-series argument for the value function is unavailable; its finiteness depends on absorption and the reward convention. The matrix itself is singular at the undiscounted endpoint because of absorbing states, while its non-absorbing block is the relevant invertible matrix. Bradtke and Barto, Proof of Theorem 1, p. 44.
The Lean state type is finite and nonempty. The paper evaluates one fixed policy, so is a real row-stochastic matrix and is a deterministic real reward on transitions; there is no action type in the formal statement. Absorbing states are exactly those with , and “absorbing chain” means that an absorbing state is reachable from every state. The paper does not define “inaccessible”; the formalization reads it as unreachable from the positive support of . The state space carries the discrete measurable structure. Theorem 1's restart process and Lemma 5's ordinary Markov chain are each constrained by their finite-dimensional cylinder probabilities, not by assumed transition frequencies.
The feature space is , and equals the cardinality of the subtype . LS TD uses only departures from . Index counts restart-process steps, so the estimate repeats at a restart draw; the paper counts in-trial transitions. These indices have the same asymptotic estimate when transitions continue. The factors in Eq. (11) cancel, and early singular inverses take Lean's total-inverse default. The value function is the return series, and the goal explicitly asserts its summability. The true parameter is existential, never defined by the formula whose convergence the theorem is meant to prove.
The paper defines for absorbing chains as expected departures from per trial. The Theorem 1 visit-frequency milestone normalizes by restart-process steps, which rescales all weights by one positive common factor; Lemma 5's matrix expression is invariant under that rescaling. Lemma 5 itself counts every ordinary-chain transition and carries the paper's “any Markov chain” scope. The milestone on invertibility allows arbitrary weights at absorbing states because their feature rows are zero. These conventions are recorded with each Lean item. Contributions toward the path-law frequency theorem, transient-matrix invertibility, return-series summability, and the matrix limit are all within scope. A vacuous path law or a value function defined from the desired linear equation would not establish the stated goal.
A call center has to decide how many agents to staff. In practice the decision is often posed as a service-level constraint rather than a cost trade-off: use the fewest agents for which the expected waiting cost, or the fraction of customers who wait, stays below a target. Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; journal version in Operations Research 52(1), 2004, doi:10.1287/opre.1030.0081) treat this constraint problem in Section 8 of their paper, alongside the cost-minimization problem of Sections 5–7, and show that a simple square-root staffing rule solves it asymptotically as the arrival rate grows.
The rule matters because it is what practitioners use. Under the classical Erlang-C model, the exact optimum requires evaluating the Erlang-C formula over many staffing levels. The asymptotic rule replaces this with a single equation in the Halfin–Whitt function : when the target is a delay probability (Example 8.5 of the paper), it reduces to staffing servers.
Timeline. Erlang's formula for the M/M/N delay probability dates from 1917. Halfin and Whitt (Operations Research 29, 1981) identified the limit of the delay probability under square-root staffing with integer . Jagers and Van Doorn (Operations Research Letters 5, 1986; SIAM Review 33, 1991) studied the continued Erlang loss and delay functions at non-integer numbers of servers, including their convexity, which is what lets the staffing problem be relaxed to a continuous one. Borst, Mandelbaum and Reiman (2000/2004) used these to prove asymptotic optimality of square-root rules for both the cost and the constraint formulations.
Customers arrive at rate to identical servers, each with service rate ; is fixed while . Stability requires . A customer who waits time units costs , where , is strictly increasing on and for all .
The Erlang-C probability of waiting is
and the conditional waiting cost is . The waiting cost per unit time with servers is
Given a target , the optimal staffing level is the least integer with ; call it .
In the continuous parametrization , define , the continuous Erlang-C function with , and . The Halfin–Whitt function is with the standard normal hazard rate. A staffing function is judged by the rounding gap
It is asymptotically optimal when as .
Suppose that for some and , , i.e. the waiting cost is comparable to the target. Let solve . Then
If for every and solves , then .
The theorem certifies the staffing rule used in workforce-management practice: the excess staffing is determined by one scalar equation involving the Gaussian function and the scaled waiting cost, and rounding the resulting staffing level misses the constraint by a vanishing fraction of the target. Lemma 8.1 is a reusable framework: any approximation that is asymptotically exact at the proposed staffing level yields an asymptotically optimal rule, and the paper instantiates it in three regimes (Theorems 8.2, 8.6, 8.9).
The results are proved on paper. To the best of current knowledge none of them, nor the Halfin–Whitt limit for the continuous Erlang-C extension, has a machine-checked proof. A formalization would produce the first verified heavy-traffic limit of the Erlang-C delay probability, a verified continuous Erlang-C extension with its integer identity, and the convexity facts about and that many staffing papers cite without proof.
The obvious argument is to quote Halfin and Whitt: the delay probability converges to under square-root staffing, so can replace the Erlang-C formula. That limit, as published in 1981, is about integer server counts along sequences with a convergent excess-staffing parameter. The paper needs it for the continuous function at non-integer server counts and for staffing functions that are merely bounded, and it also needs the identity at integers and the monotonicity of in , both cited from Jagers and Van Doorn rather than proved. None of these is in Mathlib. A second obstacle is that the staffing function is defined only implicitly by an equation involving , which depends on the arbitrary cost functions ; nothing a priori prevents it from escaping to infinity, outside the range where the Halfin–Whitt approximation applies. Finally, compares integer-level costs given by the Erlang-C formula with a continuous approximation, so both representations of the delay probability are in play at once.
The queue itself is not formalized: there is no Markov chain and no waiting-time distribution. Every statement is about the closed-form waiting cost with given by the Erlang-C formula, exactly as the paper's analysis is. Conventions, all in the namespace DimCallCenters.Constraint:
lam : ℝ is the arrival rate (λ is a Lean keyword); limits are Filter.atTop in lam, with μ fixed. Objects indexed by λ (, , ) are functions of lam constrained only for lam > 0.WaitModel packages μ > 0 and with , strict monotonicity on , and integrability of on for θ > 0 (the paper's finiteness of ; integrability is required because Lean's integral of a non-integrable function is 0).Nstar : ℝ → ℕ given with its two defining properties (feasible; below every feasible integer level above λ/μ). and are any positive solutions of their equations; existence and uniqueness are not hypotheses.∃ᶠ ("frequently"), as eventual boundedness.A trivializing formalization is ruled out: keeps all of the paper's terms and is never replaced by a smaller quantity, and the hypotheses are jointly satisfiable — with satisfies (33) for every with .
Infrastructure needed: the continuous Erlang-C function and its integer identity; the Halfin–Whitt limit (a Gaussian approximation of Poisson/gamma tails); calculus facts about the normal hazard rate. These are reusable beyond this mission, notably by the sibling missions on the cost-minimization problem. Example 8.5 (delay-probability target with ) motivates the rule but violates the strict monotonicity of , so it is not an instance of the theorem as stated. Contributions on any milestone, and on Theorem 8.9 (quality-driven regime, which needs Lemma 4.2), are welcome.
How many agents should a call center staff? Telephone call centers employ millions of people, and staffing is their largest cost, so the question is asked every half hour of every day (Gans, Koole & Mandelbaum, 2003). The classical model is the M/M/N (Erlang-C) queue: calls arrive at rate , service times are exponential with mean , and agents serve in parallel. Practitioners use the square-root safety staffing rule , which Halfin and Whitt (1981) justified in the regime where the probability of waiting stays bounded away from and .
Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; published as Operations Research 52(1), 2004) asked when such a rule is actually optimal: given a staffing cost and a waiting cost, which staffing level minimizes total cost as the arrival rate grows? They identified three regimes according to how the two costs compare. This mission formalizes their third case, the quality-driven regime, in which waiting is so expensive relative to staffing that the optimal number of agents exceeds the offered load by more than any fixed multiple of its square root.
Fix a service rate . For every arrival rate a waiting-cost function assigns cost to a wait of time units; it satisfies , is strictly increasing, and is integrable on for every . A staffing cost , defined for real , is convex and strictly increasing.
For an integer the probability of waiting is the Erlang-C formula
the expected waiting cost of a delayed customer is , and the total cost per unit time is . An optimal staffing level minimizes over the integers .
Write , and for put , , and , where extends the Erlang-C formula to real . The normalized cost is , and a surrogate cost is . Rounding is measured by .
Two special functions appear. The Halfin–Whitt delay function is with the standard normal hazard rate. The Stirling-type approximation is
Asymptotic relations are limits of ratios as : means , and means .
Assume the regime is quality-driven, display (27): for every . Let minimize over . Then
The statement fixes no constants and no rate; it asserts only that rounding the surrogate optimum loses a vanishing fraction of the excess cost.
In attack order: Lemma C.1 ( strictly convex decreasing); the identity at integer (Section 3, p. 12); Lemma 3.1 and Lemma 3.2; Corollary 3.3 (the asymptotic optimality criterion); Lemma B.1 ( strictly convex decreasing); display (15); Lemma 4.1 (Halfin and Whitt); and the first statement of Lemma 4.2, whenever .
Theorem 7.1 completes the paper's picture of optimal staffing. In the rationalized regime the square-root rule with the Halfin–Whitt function is optimal; in the efficiency-driven regime staffing barely exceeds the load; in the quality-driven regime the staffing excess outgrows and must be replaced by the Stirling-type expression . The theorem gives a one-dimensional minimization whose solution is asymptotically optimal, which turns a discrete optimization over into a smooth problem, and it marks the boundary of validity of square-root staffing.
The result is proved in the paper; it is not formalized anywhere to our knowledge. A complete development formalizes the Section 3 framework (shared with the other regimes of the same paper), the convexity of and of , the Halfin–Whitt limit for the continuous extension , and the Stirling-type asymptotics of the Erlang-C formula. Each of these is a reusable piece of queueing theory in Lean.
The regime theorem itself is short once the framework is in place; the weight lies in the analytic lemmas. Lemma 4.2 requires uniform asymptotics of at a staffing excess that may grow at any rate, from barely faster than a constant to faster than , where neither the central-limit picture of Halfin and Whitt nor a single Stirling expansion covers all cases. Lemma 4.1 concerns the continuous extension at non-integer server counts, whereas Halfin and Whitt's theorem is about integer ones. The natural first idea, that the goal follows from Corollary 3.3 by plugging in Lemma 4.2, does not apply directly: Lemma 4.2 only covers staffing excesses that tend to infinity, and nothing in the definition of the true optimum or the surrogate optimum says that they do.
Lean represents as a positive real, and is the filter atTop on with fixed. The standing assumptions on and are the structure WaitModel; is a function argument with hypotheses ConvexOn and StrictMonoOn on . Staffing levels are natural numbers. Minimizers (, , , ) are function arguments with minimality hypotheses at every , so every statement holds for every choice among ties. Liminf and limsup relations are stated through Filter.Frequently, avoiding boundedness side conditions.
The queue itself (Poisson arrivals, waiting-time law) is not formalized: the paper's analysis and all its theorems concern the closed-form cost with the Erlang-C formula.
Conventions committed to: (i) the goal adds the hypothesis as , which the paper asserts on p. 12 to show the continuous optimum exists but which does not follow from its standing assumptions (it holds exactly when is unbounded); (ii) in the floor term is omitted when , since the cost is undefined at unstable levels; (iii) the integrability of is explicit, because a Lean integral of a non-integrable function is ; (iv) , the value of formula (11) at ; (v) display (15) is stated for , since the ratio is undefined at . The instance , , (Section 9) satisfies every hypothesis of the goal, so the goal is not vacuous; taking or at Lean default values is ruled out by these explicit domain conditions.
Only the first statement of Lemma 4.2 is a milestone: the second, under , fails as printed at . Contributions on the Erlang-C asymptotics, the normal hazard rate, and Laplace transforms of increasing functions are welcome and reusable beyond this mission.
A supplier that sells through independent retailers usually loses part of the profit an integrated firm would earn: each retailer orders to maximize its own profit, not the channel's. Supply chain coordination asks which contracts make the decentralized choices coincide with the integrated optimum. Cachon and Lariviere study revenue-sharing contracts, under which a retailer pays a per-unit wholesale price and keeps only a fraction of its revenue, the rest going to the supplier. The contracts were made prominent by the video rental industry around 1998, where studios lowered tape prices in exchange for a share of rental income.
With a single retailer, revenue sharing at the wholesale price coordinates the channel and splits its profit in the proportion . This mission formalizes the extension in Section 3.2 of the paper to competing retailers: several locations whose revenues depend on each other's stock, so that one retailer's order lowers the others' revenue. Competition creates externalities the single-retailer argument does not have, and the question is whether revenue sharing still coordinates, and at what prices. Section 4.1.2 then works out a Cournot example in closed form, measuring how far the supplier's own optimal wholesale price leaves the channel from the integrated profit.
The source is the authors' working paper of June 2000; the published version (Management Science 51(1), 2005) renumbers and revises the results. The working paper numbers no theorem, so results are cited by section, displayed equation and page.
A single supplier sells one product through locations , each run by an independent retailer. A stocking profile is , and the revenue at location is , which may depend on every location's quantity. The system revenue is , every unit costs the supplier , and the integrated system profit is
Write : the superscript is the variable differentiated, the subscript the revenue function. The paper assumes that each is continuous, that for (locations are substitutes), and that is unimodal in . The system-optimal profile has positive entries and solves the first-order system
Under a revenue-sharing contract retailer earns and the supplier earns ; the wholesale-price contract is , with profits written and . A Nash equilibrium in order quantities is a profile from which no retailer gains by changing its own quantity to any . The coordinating wholesale prices are
The Cournot example (7) is with .
For and :
An interior equilibrium satisfies (Eq. (8)), so marginal-cost pricing does not support when a location imposes a negative externality; the prices make an equilibrium; when cross-effects are nonpositive; and supports exactly the split .
An interior equilibrium satisfies ; the two profit identities hold for every ; and .
At a common price the unique equilibrium is ; the integrated optimum is ; the coordinating price increases in and ; the supplier's optimal price is ; and the efficiency at is
The goal shows that the single-retailer coordination result survives competition, with one change: the coordinating price must charge each retailer for the externality it imposes on the others, so it depends on every location's revenue function, and exceeds the production cost. The supplier's profit then moves along a line between what wholesale prices alone give her and the whole system profit, which is how revenue sharing provides a profit split that linear prices cannot. The Cournot results make the comparison quantitative: when retailers compete intensely, the supplier's own optimal wholesale price already achieves most of the integrated profit, so revenue sharing, which has administrative costs, is less attractive.
No machine-checked proof of these results is known. The mission produces a reusable formal description of an -player quantity game under per-retailer linear contracts, equilibrium conditions for it, and a fully worked Cournot instance, including a uniqueness claim for equilibria among all (not only symmetric) profiles.
The equilibrium claims are global: a retailer must not gain from any nonnegative deviation, not only from small ones. A first-order condition at does not give this by itself. The page assumes unimodal in , but unimodality does not survive subtracting the linear purchase cost, so the first-order condition is not sufficient under that assumption alone; the formalization uses concavity in the own quantity, under which it is. The participation claim is stated on the page without proof and needs a bound on the revenue of a location that stocks nothing.
In the Cournot example, uniqueness of the equilibrium must exclude asymmetric profiles and profiles where some retailers stock nothing, and the supplier's optimal price must be compared against every equilibrium at every price, including prices at which the retailers order nothing.
Locations are Fin n; a profile is Fin n → ℝ; revenues are R : Fin n → (Fin n → ℝ) → ℝ, and dR i j q is , given as a partial derivative at every profile with all entries positive. A deviation of retailer to is Function.update q i x, and Nash equilibria quantify over all . The standing assumptions of Section 3.2 are fields of the structure Model: ; continuity of on the nonnegative orthant; the partial derivatives; , encoded as " does not increase in "; and concavity of in , which is the formalization's reading of "unimodal in ". The paper's assumption that marginal revenue eventually falls below every is used only for existence of an equilibrium, which is not formalized, and is omitted.
Deviations from the page, each disclosed in the item concerned:
A formalization that defines "the prices coordinate" as "the prices satisfy the first-order condition at " restates (6) and is ruled out: every equilibrium claim here is the game-theoretic statement about unilateral deviations. Contributions welcome: proofs of the equilibrium lemmas from concavity and the derivative, the Cournot uniqueness argument, and a general existence theorem for the quantity game.
Many problems in optimization, image reconstruction and statistics reduce to the convex feasibility problem: given closed convex sets , , find a point of their intersection . A classical approach is the relaxation method: from the current point, move to the nearest point of one of the sets, and repeat. For Euclidean distance and half-spaces this is the method of Agmon and of Motzkin and Schoenberg (1954); for hyperplanes it is Kaczmarz's method.
L. M. Bregman's 1967 paper replaced the Euclidean distance by an abstract function satisfying six conditions. The resulting D-projections include what are now called Bregman projections, and the paper is the origin of the Bregman divergence , used today in mirror descent, entropy maximization and the theory of row-action methods (Censor and Zenios, 1997).
The paper proves convergence for two rules for choosing which set to project onto. This mission covers the second one, Theorem 2: always project onto the set that is farthest from the current point in the sense of (the "remotest-set" or maximal-distance control).
Let be a real linear topological space and a family of closed convex subsets of ; the index set is arbitrary and may be infinite. Let be convex with , and let satisfy:
A relaxation sequence starts at and sets ; the sequence of indices is the control. The control is remotest-set if at every step realizes
In the Lean development these objects are DConditions A S D P (conditions I–IV and VI), CondV S D ((⋂ j, A j) ∩ S) (condition V), IsRelaxSeq S P i x (in the series' shared namespace BregmanRelax.Cyclic) and IsRemotestControl D P i x (in BregmanRelax.Remotest).
For every remotest-set control and every relaxation sequence it generates, every limiting point is a common point:
Theorem 2 is the first convergence result for greedy (most-violated-constraint) selection in projection methods with a non-Euclidean distance. Unlike the cyclic Theorem 1 of the same paper, it applies to infinite families of sets, which covers semi-infinite systems of convex inequalities. Lemma 1, the generalized Pythagorean inequality, is the basic estimate for Bregman projections and recurs throughout mirror-descent and row-action analyses; Lemma 2 records the Fejér-type monotonicity of the iterates with respect to .
The results are classical and proved in the paper. To our knowledge they are not formalized in Lean or another proof assistant at this level of generality. The mission produces a machine-checked version of the abstract D-projection framework, with the conditions stated so that the Bregman divergence of §2 of the paper, and the Euclidean distance, are instances.
The obvious argument for Euclidean projections uses Fejér monotonicity and the fact that a bounded sequence in has convergent subsequences. Here neither the triangle inequality nor symmetry of is available, and need not be normed or finite-dimensional. The remotest-set rule controls only the D-distance from the iterate to each projection, in that argument order; turning "these distances tend to zero along a subsequence" into "the limit lies in every " requires the interplay of conditions V and VI, and it must hold uniformly over a possibly infinite index set.
Conventions committed to in Lean:
A trivializing formalization is ruled out: the hypotheses are jointly satisfiable with a genuine run (in with , , , and ), checked locally without sorry, so neither the goal nor the lemmas holds vacuously.
A complete development needs subsequence extraction from sequentially compact sets, one-sided limits of difference quotients, and monotone convergence of real sequences — all available in Mathlib. The D-projection framework, Lemma 1 and Lemma 2 are shared with the cyclic-control mission of the same paper and are reusable for any Bregman-projection algorithm. Proofs of the lemmas, of Theorem 2, and of the instance showing the Euclidean distance satisfies conditions I–VI are welcome.
Discounted dynamic programming with bounded cost per stage is the standard setting in which infinite-horizon sequential decision problems are well posed: the optimal cost exists, satisfies Bellman's equation, and can be computed by iterating the DP operator. Shapley proved this for stochastic games in 1953 (Shapley 1953), Blackwell for discounted Markov decision processes in 1965 (Blackwell 1965), and Denardo observed in 1967 that the arguments use only two properties of the DP operator: monotonicity and contraction in the supremum norm (Denardo 1967). Bertsekas (1975, 1977) and Bertsekas and Shreve (1978) turned this observation into an abstract dynamic programming framework, in which a single mapping encodes stochastic, deterministic, minimax and multiplicative-cost problems at once (Bertsekas 1977).
Chapter 4 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case, is the contraction part of that framework. Its results are the abstract form of what every course on Markov decision processes proves for the discounted case, and they are what later work on abstract DP (Bertsekas, Abstract Dynamic Programming, 2022) and on robust and regularized MDPs builds on.
A model consists of a state space , a control space , a nonempty constraint set for each , a mapping , where is the set of functions , and a function with . is monotone: implies .
A selector is a function with ; is the set of selectors, and a policy is a sequence in . The operators are
The cost of is , the optimal cost is , and is the cost of the stationary policy .
is the Banach space of bounded real functions on with . Assumption C asks for a closed set containing and invariant under and every ; that every limit defining exist and be real; and that for some integer and scalars , ,
Under Assumption C,
implies and implies for ; each is the unique fixed point of in ; and for every
The statement carries no constants beyond those of Assumption C.
Proposition 4.2 is the existence-and-uniqueness theorem for Bellman's equation in the contraction regime, together with the convergence of value iteration from an arbitrary start in . Propositions 4.3 to 4.5 turn it into statements about policies: when a stationary optimal policy exists, how one is found from the DP algorithm, and how much is lost when Bellman's equation is solved only approximately. Proposition 4.11 shows the assumption is met by a concrete class of problems, discounted minimax control, and so certifies that the abstract theorems are not vacuous.
The results are classical and have been proved in print since 1978; none of them is open. What this mission adds is a machine-checked version of the abstract theory itself, rather than of a single model. Mathlib has the Banach fixed point theorem for a contracting map of a complete space (ContractingWith) and a lemma for contracting iterates, but not the version on a closed subset with norm convergence of every orbit, and nothing on abstract DP. The platform has proved the finite-state discounted case for a concrete model (BertsekasDP.discounted_main_theorem); the abstract statements here cover infinite state spaces, minimax problems and -step contractions, and are reused by the later missions of this series (generalized models, Chapter 6) and by papers that cite the book.
The first idea is to apply the contraction mapping principle to and read off as its fixed point. That gives a fixed point of but says nothing about , which is defined as an infimum over all, generally nonstationary, policies of limits of compositions. The identification of the fixed point with is the content of the proposition, and it is where the Lipschitz condition (2) on all of , not only on , enters.
Two further features block a direct appeal to Mathlib. The contraction is only -step, so neither nor need be a contraction. And takes extended-real values, so every passage between and the Banach space must be justified by the invariance of .
The state and control spaces are arbitrary types. is S → EReal; is Mathlib's lp (fun _ : S => ℝ) ⊤, whose norm is the supremum norm, and toF embeds into . is an arbitrary closed subset of , not itself, and uniqueness of fixed points is asserted within . Policies are sequences ℕ → M; applies first. is the pointwise limit (limUnder), which exists and is real under Assumption C; is the infimum over all policies.
The book computes in with , whereas Mathlib's EReal has . No statement adds infinities of opposite sign. A norm bound between functions of is the predicate SupDistLe: both functions are real at every point and differ by at most , which is what the bound means under the book's arithmetic. Condition (2) is imposed on all of , as on p. 53. The scalars of Assumption C are explicit parameters, so the constant of Proposition 4.5 is the book's exact expression. The Fixed Point Theorem assumes nonempty, which the page leaves implicit and without which the statement is false.
Defining as the fixed point of , or replacing it by the infimum over stationary policies, would make the goal trivial. Neither is done here: is the infimum of the policy costs, exactly as in Eq. (8) of Chapter 2.
A complete development needs the -step fixed point theorem on closed subsets of a Banach space, which can be reused well beyond dynamic programming; the elementary calculus of SupDistLe and of the embedding of into S → EReal; and the monotone-operator inequalities of Section 2.1. Contributions of any of these, or alternative proofs of the milestones, are welcome.
A call center must choose enough servers to limit waiting while paying for every server it staffs. When arrivals are heavy, small changes in the number of servers can change the probability of delay substantially. Borst, Mandelbaum, and Reiman study how to make this choice when the arrival rate grows and the costs of staffing and waiting need not grow at the same rate. Their CWI report treats several regimes within one queueing model. This mission concerns the efficiency-driven regime, where the incremental staffing cost eventually dominates the conditional waiting cost at every fixed positive square-root staffing offset. The resulting rule chooses an offset by optimizing a simpler cost that treats the probability of waiting as one.
The result is useful when the staffing-cost and waiting-cost primitives change with system scale. It says that the simplified choice still attains the optimal total cost asymptotically, even though the actual staffing decision is an integer and the simplified problem uses a real variable. The report states this as Theorem 6.1 on printed page 19, with its interpretation of asymptotic optimality supplied by Corollary 3.3 on printed page 14.
Customers arrive at rate and receive exponential service at rate per server. The service rate is fixed as grows. For an integer number of servers , the Erlang-C delay probability is the explicit finite-sum expression in Section 2 of the report. A customer who waits has an exponential waiting time with rate . Let be the cost of a wait of length . It is strictly increasing on , satisfies , and has finite exponential expectation at every positive rate. The resulting conditional waiting cost is
The staffing cost is one fixed, convex, strictly increasing function of the server count. Its continuous extension is evaluated at real . Total cost per unit of time at a stable integer level is
Write for any minimizing stable integer level. Ties are permitted. For a positive real offset , define , , and . The report extends Erlang-C continuously to and writes the incremental continuous objective as . These definitions and the integer-extension identity are from Section 3, printed pages 11–12.
The report defines the efficiency-driven regime by
For each , choose to minimize over . Let be the smaller cost of the stable integer levels immediately below and above ; if the lower one is unstable, use the upper one. The goal, Theorem 6.1 together with Corollary 3.3, is
The milestone path includes the convexity of the conditional waiting cost (Lemma C.1), the agreement of the continuous Erlang-C extension with its integer formula, the two approximation lemmas and their corollary (Lemmas 3.1–3.2 and Corollary 3.3), the convex staffing-cost comparison of equation (13), and all three clauses of the Halfin–Whitt limit in Lemma 4.1. This ordering follows the objects each later statement uses.
The theorem certifies a staffing rule defined by a one-variable surrogate rather than the exact Erlang-C probability in the objective. Its guarantee concerns the incremental total cost above the unavoidable baseline , which is the economically relevant quantity when comparing two near-minimal stable staffing levels. The ratio tends to one, so the theorem is stronger than a claim that the two costs merely have the same growth order. The source also presents other regimes with different surrogates; their conclusions are separate targets in this series.
The paper proves the mathematical theorem. This mission asks for a Lean proof of its closed-form model and the surrounding lemmas. The complete development would make the report's approximation framework reusable for later results that combine a continuous queueing approximation, a surrogate minimizer, and integer rounding. It would also expose the exact assumptions needed to pass between real and integer staffing levels. No machine-checked proof of this report's Theorem 6.1 is claimed here.
The simple objective replaces the delay probability by one. That replacement is accurate near zero offset, but the minimizing offset itself changes with . Pointwise asymptotics at a fixed positive offset do not directly control the value of an objective at its moving minimizer. The proof therefore has to relate the regime assumption to the location of the relevant minimizers before using the Halfin–Whitt limit. Integer rounding introduces another boundary issue: when is just above , its floor need not be stable, so evaluating the ordinary Erlang-C formula there would compare the target against a meaningless cost. These difficulties are visible already in the statements of Theorem 6.1 and Lemma 3.2.
Lean represents , , offsets, and costs as real numbers; arrival-rate limits use the real filter at . Staffing counts are natural numbers. The service rate is positive and fixed. A WaitModel packages strict increase and normalization of on nonnegative waits together with integrability against every positive exponential rate. This integrability expresses the report's finiteness assumption for and prevents a nonintegrable real integral from silently evaluating to zero. The hypotheses on are convexity and strict increase on positive real staffing levels; does not depend on .
The report asserts that diverges as decreases to , although the stated assumptions permit bounded increasing waiting penalties for which that assertion fails. The goal therefore includes this explicit divergence hypothesis, which also supports existence of the continuous minimizer used in the report's argument. The integer optimum and the surrogate optimum are functions constrained to be minimizers at every positive arrival rate. They cannot be arbitrary choices that make the conclusion vacuous. The continuous optimum appears only in the framework milestones; it is not a hypothesis of Theorem 6.1.
All formulas are total Lean functions. Their values at , unstable integer counts, nonpositive offsets, or invalid parameters to the continuous Erlang-C integral have no queueing interpretation. Every theorem using them constrains its relevant inputs. The definition of ignores an unstable floor and uses the stable ceiling. At a positive offset and arrival rate this ceiling is above offered load. The Gaussian density, its cumulative integral, the hazard rate, and the delay function use the explicit formulas of Section 4; the value of the delay function at zero is the continuous extension needed by Lemma 4.1.
The queue's stochastic construction is outside this mission. The formal objects are the report's cost formulas and asymptotic comparisons, not a continuous-time Markov chain. Useful contributions include proofs of the special-function limit, convexity of conditional waiting cost, the integer-extension identity, and the reusable approximation lemmas. The regime condition is the full limit in equation (23); weakening it to an unrelated boundedness condition would change the theorem.
In stochastic optimization and statistical learning one chooses a parameter from a set to make the risk small, having seen only a sample from . Generalization bounds suggest trading empirical risk against its standard deviation, but the variance-penalized objective is non-convex even for convex losses. Duchi and Namkoong (arXiv:1610.02581v3) replace it by the robustly regularized risk, the worst-case expected loss over a -divergence ball around the empirical distribution. This objective is convex whenever is, and it agrees with the variance-penalized objective up to a small error.
When the risk has curvature near its minimizers, empirical risk minimization attains rates faster than (Bartlett, Bousquet and Mendelson 2005; Shapiro, Dentcheva and Ruszczyński 2009). Section 4.1 of the paper asks whether minimizers of the robust risk, which carry an extra variance-dependent penalty of order , keep these fast rates. Its Theorem 5 answers yes, and does so for approximate minimizers, which is what iterative solvers return.
A loss is fixed, with convex and -Lipschitz on a convex set for every , and integrable. The risk is .
For a radius , the ball around the empirical distribution is the set of weight vectors
and the robust risk is .
For the -suboptimal sets of the risk and of the robust risk are
with the solution set and the Euclidean projection onto it. The risk satisfies a growth condition of order if, for some and ,
The complexity of the problem enters through the localized class and its empirical Rademacher complexity , with independent uniform signs .
For , , and satisfying
The theorem says that the variance penalty implicit in the robust objective does not cost the fast rates available under curvature. The -dependent condition in (27) is of order , which for quadratic growth () is , the same order as the localized complexity term in typical parametric problems. Corollary 4.1 of the paper derives explicit rates of order from it for a unique minimizer. The result applies to -approximate minimizers, so it covers the output of the stochastic-gradient methods used to solve the robust problem.
The result is proved in the paper (Appendix E). None of it is formalized: no statement about growth conditions, localized deviations of a robust objective, or fast rates for robust minimizers is on Prove2Me. A formal proof would check the printed constants, settle the boundary case (see below), and produce a localization lemma and a reduction from approximate robust minimizers to empirical processes that apply to other estimators.
The obvious argument fails at two points. First, a uniform deviation bound over all of gives only the rate: the speed-up comes from localizing to , which requires transferring the growth condition, assumed only within distance of , to every -suboptimal point by convexity. Second, the robust risk is not an empirical average, so standard comparisons between empirical and population minimizers do not apply. Claim E.1 handles this by moving along the segment from a bad approximate minimizer to its projection, which needs the projection to be preserved along that segment (a normal-cone property of ) and the risk to be continuous there. The robust–empirical gap is then controlled by the variance expansion of Theorem 1. The concentration step needs a bounded-differences inequality for a supremum over an uncountable class, together with symmetrization; neither is in Mathlib in this form.
Parameters live in EuclideanSpace ℝ (Fin d), so norms, distances and projections are Euclidean. The sample is the coordinate process of the product measure on Fin n → X, , and probabilities are measures of sample sets (the outer measure for a set that is not measurable). The ball is the weight-vector form (8). The suboptimal sets are written without infima ( for all ). Each supremum "" is written as "for every some reaches ", so no statement relies on the default value of a real supremum. The Rademacher complexity is the published UnderstandingML.rademacher, and its expectation over the sample is assumed integrable, so that it is the true expectation and not the default value of a Bochner integral. Lipschitz continuity is required on , as printed.
Corrections and presuppositions:
The constant is the printed one; the proof uses a smaller one, which the printed condition implies. The hypotheses , and make every power well defined. A formalization that assumed (26) vacuously, took , or let the Rademacher term be a non-integrable Bochner integral would trivialize the goal; the statements rule these out.
Infrastructure: Euclidean projection onto closed convex sets and its normal-cone characterization (partly in Mathlib), convexity of integral functionals, McDiarmid's bounded-differences inequality, and symmetrization for suprema of empirical processes. The concentration tools and the localization lemma can be reused beyond this mission. Contributions toward McDiarmid's inequality and symmetrization are especially welcome.
Many selection problems assign a value to each subset of a finite collection: the coverage supplied by chosen facilities, the influence reached by chosen seeds, or the value of a coalition. A submodular set function has diminishing returns in the precise sense that the combined value of two sets, counting their overlap once, does not exceed the sum of their separate values. When the function is also monotone, taking more elements never hurts. The unconstrained problem studied here permits nonmonotone functions, so both accepting and rejecting an element can matter. The question is what a single pass through the elements can guarantee when the function is available through value queries. Buchbinder et al., FOCS 2012
The randomized algorithm in this mission attains an expected one-half approximation for every nonnegative submodular function. The paper presents this as tight in the value-oracle setting: it recalls the earlier result of Feige, Mirrokni and Vondrák that a fixed improvement beyond one-half requires exponentially many queries. The contribution here is therefore both the guarantee and a short adaptive rule that attains it in a linear number of iterations. The local proposal follows the FOCS 2012 version of the paper; its theorem numbering differs from the later SIAM Journal on Computing article. Buchbinder et al., §I.A and Theorem I.2
Let be a finite ground set, and let assign a nonnegative real value to every subset. The unconstrained submodular maximization problem asks for the largest value among all . Write for that value when no confusion arises, and for a set attaining it. Submodularity means
There is no monotonicity or normalization assumption: and may both be positive. A value oracle returns for a requested subset . The paper's complexity claim counts such queries, assuming a query takes constant time. Buchbinder et al., §I and footnotes 1–2
Algorithm 2 visits the elements once in an arbitrary order . It keeps two sets, starting at and . At step , it measures the gain from adding to and the gain from removing from . It clips each gain at zero, giving and . It adds to with probability and otherwise removes it from . When both clipped gains vanish, the paper defines the add probability as one. After all elements have been processed, the two sets coincide, and the algorithm returns their common value. The state law is adaptive: its probability at step depends on the actual pair of sets produced by earlier choices. Buchbinder et al., Algorithm 2
The main target is Theorem I.2 for this exact algorithm and for every enumeration of the ground set:
The milestone statements retain the paper's key local quantities. For a comparison optimum , set . Lemma II.1 asserts . The endpoint statement identifies and . Inequality (3) bounds the conditional loss in the positive-gain case; Lemma III.1 compares the expected change of with the expected combined change of and . The telescoped display keeps the initial endpoint values and before using nonnegativity. Buchbinder et al., Lemmas II.1 and III.1, inequality (3), proof of Theorem I.2
A companion target is Theorem I.4 via its second proof. For two normalized monotone submodular utilities , let . The maximum of is exactly the optimal welfare of a two-player partition. Algorithm 2 on is asked to satisfy
This is the paper's three-quarter guarantee in its welfare application. Buchbinder et al., Theorem I.4 and Proof (2)
The main theorem gives a specific randomized rule whose expected value is at least half the best subset value, even when accepting an element can lower the objective. It applies without restricting the cardinality or shape of the chosen subset. The welfare corollary shows that keeping the initial endpoint values in the analysis yields a stronger guarantee for the objective formed from two monotone players. Buchbinder et al., Theorems I.2 and I.4
This mission formalizes the statement of the algorithm, its intermediate state laws, its comparison set, and the paper's numbered proof targets. The algorithmic guarantee is proved in the source paper; the local Lean theorem files are open statements with sorry and do not yet give machine-checked proofs of these results. A completed development would supply a reusable formal model of an adaptive finite random process over pairs of subsets, as well as the specific submodular inequalities. The published Submodular and OPT definitions from the earlier Feige–Mirrokni–Vondrák formalization are reused here.
The two possible updates cannot be assessed independently. The probability of each choice depends on the current state, and the comparison set can gain or lose the processed element in a way that differs from the two algorithm sets. A bound on the expected value of alone does not control the movement of . The proof must handle the clipped gains, including the case when both are zero, while preserving the exact joint law of . Buchbinder et al., proof of Lemma III.1
The ground set is a finite Lean type; subsets are Finset X, and values are real numbers. An order is a list with no repeated elements that covers the type, including the empty type. The run is an explicit finite mass function on pairs of subsets after every prefix of the list. Expectation is a finite weighted sum, so it has no integrability exception. The transition clips the two real marginal gains and handles by assigning probability one to the add branch, exactly as Algorithm 2 specifies. The optimum is the published maximum over all subsets. No ratio divides by a possibly zero optimum.
The theorem fixes Algorithm 2 itself; an arbitrary process with nested sets or a process defined by its desired approximation property does not satisfy this scope. The Lean goal states the value bound and leaves the paper's linear-time claim outside the formal theorem. The algorithm uses four value evaluations per processed element in its printed rule; the Lean development represents those evaluations, not an implementation cost model. The statement that its two final sets coincide is a separate milestone.
The source's main-text decreasing-returns definition has an overbroad quantifier on the added element. This development uses the equivalent lattice inequality given in the paper's footnote, which permits nonmonotone functions. The proof of Lemma II.1 also has a set-index slip, and the proof of Theorem I.2 prints for in one display; neither slip is copied into a formal statement. The one-step inequality (3) is stated for any nested pair with the processed element in , a generalization of the conditioned reachable states in the paper. Contributions proving the endpoint invariant, conditional inequality, one-step expected estimate, and final bound are all within scope.
A stochastic approximation algorithm is a recursion
in , where is a vector field, are small step sizes and is noise. Such recursions go back to Robbins and Monro's root-finding scheme (Robbins–Monro 1951) and underlie stochastic gradient descent, temporal-difference learning, adaptive control and learning in games. The ODE method studies them by comparing the iterates with the trajectories of .
Benaïm's lecture notes (Benaïm 1999) organize the ODE method in two steps. A deterministic step, Proposition 4.1, shows that whenever the noise satisfies a condition called A1 (together with a boundedness condition on the iterates), the interpolated process is an asymptotic pseudotrajectory of the flow of . A probabilistic step then verifies A1 for concrete noise models. Proposition 4.2 does this for martingale difference noise with bounded -th moments, at the price of step sizes with . This mission formalizes the second verification, Proposition 4.4: when the noise is subgaussian, A1 holds almost surely under the much weaker requirement that for every , which allows step sizes decaying only slightly faster than . The notes attribute the result to Duflo (1997), see also Kushner and Yin (1997) and Benaïm and Hirsch (1996).
Let be a deterministic sequence with , and (a step sequence). Put , , and let
be the index of the step that contains time . For a sequence define the piecewise constant processes and , so that step occupies the time interval of length .
Assumption A1 asks that for every
or, in the form the notes call equivalent, for every , where
Let be a probability space with a nondecreasing sequence of sub--algebras, and continuous. A sequence given by the recursion above is a Robbins–Monro algorithm if is deterministic, is -measurable, and . The noise is subgaussian if there is a number such that for all and all
Bounded noise, , is an example.
For a Robbins–Monro algorithm with subgaussian noise and a deterministic step sequence such that
with probability one the realised noise sequence satisfies A1, in both of its forms, simultaneously for all .
is a supermartingale. 2. Directional maximal tail bound. For every unit vector , , and ,
Proposition 4.4 is the sufficient condition for the ODE method when the noise has Gaussian-type tails. Its step-size condition holds whenever , so it admits steps that decrease far more slowly than the of the classical theory; slowly decreasing steps are what practitioners use to keep algorithms responsive. Combined with Proposition 4.1 it shows that the interpolated process of such an algorithm, with bounded iterates, is almost surely an asymptotic pseudotrajectory of the flow of , and the limit set theorems of the notes then locate the limit points of the algorithm.
The result is proved in the notes and in the cited literature; it has not, to our knowledge, been machine-checked. A formal proof would add reusable pieces: an exponential supermartingale and maximal inequality for vector-valued martingale differences with a conditional subgaussian bound (Mathlib's conditional subgaussian notion is scalar), a Borel–Cantelli argument along the grid , and the continuous-time bookkeeping of , and shared with the other missions of this series.
The moment method of Proposition 4.2 does not reach this regime: any fixed polynomial moment of the window sums decays only polynomially in the window's step sizes, and under alone polynomial bounds are not summable over windows. Exponential tail bounds are needed, and they must be maximal (uniform over the window) and must hold for the norm of a vector, not only for a scalar. The continuous-time deviation involves partial steps at both ends of , so the bound must be stated in terms of rather than a sum over whole steps, with constants that do not depend on , or . Finally, A1 quantifies over all : the almost-sure statement must hold on a single event of full probability for every .
The space is as EuclideanSpace ℝ (Fin d) (the paper writes ); time is real. The sequences and are indexed by , and their values at are unused, as the paper indexes them from . The filtration is a Mathlib Filtration ℕ; is -strongly measurable and integrable, and almost surely. The subgaussian condition requires to be integrable for every and . The summand is taken to be when , its limiting value. The suprema in A1 and are taken in ; the supremum over an empty range of is . In Eq. (18) the constants are chosen before the probability space, the algorithm and .
The following readings are excluded and are not acceptable formalizations: a subgaussian condition that holds vacuously because the exponential is not integrable (Lean's conditional expectation of a non-integrable function is ); a summability condition made trivial or false by the convention ; and the conclusion "for each , A1 holds almost surely" in place of "almost surely, A1 holds for all ". The second sentence of Proposition 4.4 (the asymptotic pseudotrajectory conclusion) is outside this mission.
All hypotheses are satisfiable: , , , and satisfy every one of them.
Contributions welcome: a maximal inequality for nonnegative supermartingales in the form needed here, vector subgaussian tail bounds for martingale transforms with deterministic weights (reusable well beyond this mission), lemmas on the step processes and (measurability, local integrability, additivity), and the proofs of the milestones.
Dynamic programming over uncountable state and control spaces needs two things at every stage: the optimal cost-to-go, obtained by minimizing over the control, must be a function that can be integrated against the next stage's transition probabilities, and a policy that nearly attains the minimum must be measurable, so that it defines a stochastic process. With Borel-measurable costs and Borel-measurable policies both requirements fail. Minimizing a Borel function of over produces a function whose level sets are projections of Borel sets, and such projections need not be Borel (Suslin, 1917). The repair, developed by Blackwell, Freedman and Orkin (1974), Shreve and Bertsekas, and set out in Chapter 7 of Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978), is to enlarge the class of costs to the lower semianalytic functions and the class of policies to the analytically or universally measurable ones. Sections 7.6–7.7 of the book establish that this class is closed under partial minimization and admits measurable ε-optimal selectors. Chapters 8–10 of the book, and much of the later literature on Borel-space Markov decision processes (Hernández-Lerma and Lasserre; Feinberg and coauthors), build on these results.
Timeline:
A Borel space is a topological space homeomorphic to a Borel subset of a complete separable metric space (Definition 7.7); its Borel σ-algebra is . The Baire space is with the product topology. A set is analytic if it is empty or the image of under a continuous map; by Proposition 7.41 this is the book's Definition 7.16 (the Suslin operation applied to closed sets). Every Borel set is analytic, and the converse fails when is uncountable.
Three σ-algebras on are in play. The analytic σ-algebra is generated by the analytic sets (Definition 7.19). The universal σ-algebra is , the intersection over all probability measures on of the -completions of (Definition 7.18). For a function from into a Borel space , is analytically measurable if and for every , and universally measurable if the same holds with (Definition 7.20).
Let . A function is lower semianalytic if is analytic and is analytic for every real (Definition 7.21). For write , , and define the partial infimum
A selector is a function whose graph lies in .
Let be Borel spaces, analytic, and lower semianalytic.
(a) For every there is an analytically measurable selector with
(b) The set of points where the infimum is attained is universally measurable, and for every there is a universally measurable selector with on and the bounds of (a) off .
The goal fixes no constant beyond the book's and .
In attack order: Proposition 7.40 (Borel images and preimages of analytic sets are analytic), Corollary 7.42.1 (), Corollary 7.44.2 (composites of analytically measurable maps are universally measurable), and Proposition 7.49, the Jankov–von Neumann theorem:
Further items of the mission, on the same definitions: Proposition 7.39 (projections of analytic sets are analytic, and every analytic set is a projection of a Borel set), Lemma 7.30(1) (strict and non-strict, real and extended level sets give the same class) and Proposition 7.47 (lower semianalytic functions are exactly partial infima of Borel functions).
Proposition 7.50 is the selection theorem behind the existence of ε-optimal policies in Borel-space dynamic programming. In the finite-horizon model of Chapter 8 the optimal cost-to-go at each stage is lower semianalytic, by Propositions 7.47 and 7.48. Proposition 7.50 then turns the one-stage minimization into a measurable policy, analytically measurable when only ε-optimality is required and universally measurable when the minimum is attained. Chapters 8–9 of the book (the finite-horizon recursion and the optimality equation under (P), (N), (D)) use it at every step. Downstream catalog papers on average-cost and stochastic shortest-path problems over Borel spaces cite these results.
All results here are proved in the book and in the descriptive set theory literature (Kechris, Classical Descriptive Set Theory, §18 and §29). None is formalized on Prove2Me. Mathlib has analytic sets in Polish-type settings, the Lusin separation theorem and Suslin's theorem, but it has no universal σ-algebra, no analytic σ-algebra, no lower semianalytic functions and no Jankov–von Neumann uniformization. The definitions in this mission are reusable by the later missions of the series (Chapters 8–10), which restate them locally until these are published.
The obvious route to a selector is to choose, for each , a minimizing or near-minimizing . The axiom of choice provides such a function, but nothing makes it measurable, and the conclusion of the theorem is exactly that measurability. The Borel route fails too: the set is a projection of a Borel set, which is analytic but in general not Borel, so no Borel-measurable selector exists in general. The Jankov–von Neumann theorem needs a lexicographically least branch of a continuous parametrization of by , and an argument that the resulting map is measurable with respect to , which is generated by sets that are not closed under complementation. Part (b) adds a further obstacle: the composite of two analytically measurable maps need not be analytically measurable, so the exact selector is only universally measurable. Proving that requires Lusin's theorem that analytic sets are measurable for every completed probability measure.
IsBorelSpace (Definition 7.7, the ambient complete separable metric space taken in the same universe), together with Mathlib's [MeasurableSpace X] [BorelSpace X], so measurable sets are exactly the Borel sets. On the product σ-algebra is used; it coincides with for separable metrizable spaces (Proposition 7.13).MeasureTheory.AnalyticSet (empty or a continuous image of ℕ → ℕ).EReal. The book uses , and Mathlib's EReal uses . No statement of this mission adds infinities of opposite sign; adds a real number.NullMeasurableSet E p for every probability measure p.Not included: Lusin's theorem in Suslin-scheme form (Proposition 7.42, which needs the Suslin operation as a definition), Proposition 7.43 on , the integration results of Propositions 7.46 and 7.48, and Lemma 7.30(2)–(4). None is used in the proof of the goal. Contributions welcome: the bridge between IsBorelSpace and Mathlib's StandardBorelSpace, the universal σ-algebra API, and the Jankov–von Neumann theorem itself.
A supplier who sells to an independent retailer through a plain per-unit wholesale price faces double marginalization: the retailer orders less than the quantity that maximizes the profit of the supply chain as a whole, because each unit costs him the wholesale price rather than the production cost. Supply chain contracting studies payment schemes under which the retailer's own optimum coincides with the system optimum. Such a scheme is said to coordinate the channel. The usual examples are buy-back contracts (Pasternack, 1985), quantity-flexibility contracts (Tsay and Lovejoy, 1999) and quantity discounts (Jeuland and Shugan, 1983; Moorthy, 1987).
Cachon and Lariviere study revenue sharing, in which the retailer pays a low wholesale price and also hands over a fixed fraction of his revenue. The scheme was common in video-cassette rental in the late 1990s, where it let rental chains stock far more copies of new releases. This mission formalizes the paper's single-retailer result: revenue sharing coordinates the channel, and the supplier can choose any split of the channel's maximal profit. It also includes the three further results of the paper that use the same argument.
The source is the authors' working paper of June 2000. Its results are unnumbered, so every item cites a section, a displayed equation and a printed page. The 2005 Management Science version renumbers and revises the material.
A supplier sells to one retailer, who orders units before a selling season. The retailer's expected revenue is a function of the quantity alone. Leftover units have zero salvage value, and the supplier produces each unit at cost . The paper's standing assumptions (Sec. 1, p. 5) are:
A revenue-sharing contract has two terms. The retailer pays the wholesale price per unit, and he keeps the share of the revenue and transfers to the supplier. The case is the plain wholesale-price contract. The profits of the supply chain, the retailer and the supplier are
The integrated channel quantity is the maximizer of over . In Lean these objects are RevShareCoord.Single.Model (fields R, R', c and the three assumptions) and its functions Pi, retailerProfit and supplierProfit.
Let and . Then
The statement fixes no revenue function and no share. It holds for every model and every , which is what "the supplier can take any share of the channel profit" means.
The result separates coordination from profit division. A contract family coordinates for every value of a parameter, and that parameter then moves profit between the firms without changing the quantity, so the contract terms can be settled by bargaining power alone. The heterogeneous-retailer milestone gives the practical advantage over quantity discounts: the coordinating terms do not depend on the retailer's demand, so one price list serves retailers who face different markets. The Sec. 2.3 equivalence shows that, in the fixed-price newsvendor, buy-backs are a special case of revenue sharing. The Sec. 3.1 statement shows that revenue sharing still coordinates when the retailer also sets the price, a setting in which Emmons and Gilbert (1998) showed buy-backs fail.
All of these results are proved in the paper, and none is open. The mission adds a machine-checked version of the single-retailer theory for a general strictly concave revenue function. A related newsvendor version is already formalized on the platform: SupplyChainTheory.revenue_sharing_coordinates, from Snyder and Shen, Fundamentals of Supply Chain Theory, Thm 14.6. That version has a newsvendor revenue with salvage values and goodwill costs, and it concludes the optimality of three profits, not the -split of this paper. It is a different statement, so it is not reused here.
The algebra is short. The identity under is a single line, and it is a milestone, not the goal. The work lies in the optimization claims over a half-line with only one-sided information at . The integrated optimum must be shown to exist. gives only an eventual bound on the derivative, so the existence argument needs the continuity of a concave function and its supergradient inequality. It must also be shown positive, which uses as a one-sided derivative. Its uniqueness rests on strict concavity. The retailer's first-order condition needs the same machinery for , including the observation that the boundary point is never optimal. A stationary point of is not enough. The goal asserts that is the unique maximizer over all of .
HasDerivWithinAt R (R' q) (Set.Ici 0) q for , so it is one-sided at . Strict concavity is StrictConcaveOn ℝ (Set.Ici 0) R.IsMaxOn over (over in Sec. 3.1), and "unique" means every other maximizer equals it.Many problems in optimization and numerical analysis reduce to finding a point in the intersection of finitely many closed convex sets: solving a system of linear equations or inequalities, reconstructing an image from projections, or finding a feasible point of a convex program. The classical methods for this convex feasibility problem project the current point onto one set at a time, in Euclidean distance: Kaczmarz (1937) for linear equations, Agmon and Motzkin–Schoenberg (1954) for linear inequalities, and the cyclic projection method for general convex sets studied by Gubin, Polyak and Raik (1967).
L. M. Bregman's 1967 paper replaces the Euclidean distance by a general function satisfying a short list of axioms, and shows that the projection method still works. The functions built from a strictly convex are the ones now called Bregman divergences, and the paper is the origin of Bregman projections, of the row-action methods of Censor and collaborators, and indirectly of mirror descent. Its §2 uses the abstract result to solve convex programs with linear constraints by relaxation.
This mission formalizes §1 of the paper for the cyclic control, in which the sets are visited in a fixed round-robin order. A companion mission treats the remotest-set control of Theorem 2, and two further missions treat the convex-programming results of §2.
Let be a real linear topological space and closed convex subsets of , with intersection . Let be a convex set with , and let . The paper requires:
The relaxation sequence with control starts at any and sets . Under the cyclic control , the sets are projected onto in the order . A limiting point of is the limit of a convergent subsequence .
The Lean development uses the namespace BregmanRelax.Cyclic: DConditions A S D P bundles conditions I–IV and VI together with the closedness and convexity of the sets, CondV S D Z is condition V for the points of , IsRelaxSeq S P i x is the relaxation sequence with control , and cyclicControl hm is .
Under conditions I–VI, with the cyclic control, every limiting point of every relaxation sequence lies in every set:
The statement is about every starting point and every convergent subsequence. It does not assert that the whole sequence converges.
For any control whose relaxation sequence has all its limiting points in (the cyclic control, by Theorem 1), if in addition is closed and is continuous on for all , then the relaxation sequence converges to a point of .
Theorem 1 is the abstract convergence theorem behind cyclic Bregman projections. With in a Hilbert space it gives the convergence of cyclic orthogonal projections onto finitely many closed convex sets in the weak topology (the paper's Example 1). With given by a Bregman divergence it gives the method that the paper's §2 turns into an algorithm for convex programs with linear equality and inequality constraints, including entropy maximization. Lemma 1, the generalized Pythagorean inequality, is used throughout the later literature on Bregman projections, mirror descent and online learning.
The results are proved in the paper and are classical. To our knowledge no machine-checked version exists: Mathlib has orthogonal projections onto closed convex sets in Hilbert spaces, but no Bregman projections and no convergence theorem for cyclic projection methods. A formalization supplies an axiomatic interface (conditions I–VI) that does not depend on any particular divergence, so special cases (Euclidean distance, Kullback–Leibler divergence, Bregman divergences of Legendre functions) can be obtained by checking the conditions.
There is no norm and no metric: is neither symmetric nor subject to a triangle inequality, and is only a topological vector space. The usual Fejér-monotonicity argument for Euclidean projections, which compares distances to a fixed point of , works only one way in . Convergence of a subsequence does not by itself say anything about the shifted subsequences , and these are needed to reach every set . That step requires condition VI together with compactness, and condition VI has a compactness premise that has to be supplied separately. Throughout, convergence is in a general topology where "compact" and "sequentially compact" may differ.
The formalization commits to the following readings, each recorded in the items' Formalization Notes.
IsSeqCompact. The set of elements of being compact is read as lying in a sequentially compact set.T2Space X is assumed. is a real topological vector space (IsTopologicalAddGroup, ContinuousSMul ℝ).x ∘ φ for a strictly increasing φ : ℕ → ℕ.Fin m with , and the cyclic control is , the paper's shifted by one.X → X → ℝ; every condition constrains it on only, and the standing assumption is an explicit hypothesis.A trivializing formalization is ruled out: the hypotheses are satisfiable (a sorry-free local check takes , , two overlapping closed intervals and the clamp projections), the conclusion concerns every limiting point of every cyclic run, and the goal neither assumes convergence nor restricts the control.
Contributions welcome: proofs of the milestones, a proof of the goal, and instances of DConditions for concrete divergences (squared Euclidean distance in finite dimension, Bregman divergences of strictly convex differentiable functions). These instances are reusable by the companion missions of this paper.
Every step of the dynamic programming algorithm on a general state space does three things: it takes a conditional expectation of the cost-to-go under a transition kernel, it minimizes the resulting function of state and control over the control, and, if a policy is to be produced, it picks a control for each state that attains or nearly attains that minimum. On a finite or countable state space all three are harmless. On an uncountable state space each can destroy the measurability needed to take the next expectation: the infimum over an uncountable family of measurable functions need not be measurable, and a minimizer chosen state by state need not be a measurable function of the state, so it does not define a policy at all.
Section 7.5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), settles the three operations for semicontinuous costs and continuous kernels. The results are the topological half of the book's measurability theory; the descriptive set theory half (lower semianalytic functions and analytically measurable selectors, §7.6–7.7) is a separate mission in this series. The semicontinuous results are what Propositions 8.6–8.7 and Corollaries 9.17.2–9.17.3 of the book use to obtain Borel-measurable optimal policies for finite-horizon and infinite-horizon models with lower semicontinuous costs and compact control sets.
Timeline. The exact selection theorem for lower semicontinuous functions (Proposition 7.33 below) is credited by the book's notes to Dubins and Savage, How to Gamble If You Must (1965). The Hausdorff metric on closed sets goes back to Hausdorff's Set Theory. Measurable selection in the closed-valued setting was later systematized by Kuratowski and Ryll-Nardzewski (1965), whose theorem gives a different route to results of this kind.
Throughout, is the extended real line. A function on a metrizable space is lower semicontinuous if every sublevel set , , is closed, and upper semicontinuous if every superlevel set is closed (Definition 7.13). is the space of bounded continuous real-valued functions on .
For a separable metrizable space , is the set of Borel probability measures on with the weak topology (convergence of integrals of functions in ). A stochastic kernel on given is a map from to , and it is continuous if this map is continuous (Definition 7.12). The integral of a Borel-measurable is with the convention (Eq. (43) of Chapter 7).
For a compact metric space , is the collection of closed subsets of with the topology of the Hausdorff metric (Appendix C). For , the section at is , the projection is , and a function has its graph in if for every . "Borel-measurable" refers to the Borel σ-algebras of the topologies in question; on this is the Borel σ-algebra of the subspace topology.
Let be metrizable, compact metrizable, closed, and lower semicontinuous. Put
Then is closed, is lower semicontinuous, and there is a Borel-measurable with graph in and
The results. Propositions 7.31–7.33 are the closure properties that make the dynamic programming recursion stay inside the class of lower semicontinuous functions bounded below: the expectation step preserves the class (7.31), the minimization step preserves it (7.32, 7.33), and the minimization admits a Borel-measurable exact minimizer (7.33). This is why, in semicontinuous models, the optimal cost functions are lower semicontinuous and optimal policies can be taken Borel-measurable and nonrandomized. Proposition 7.34 gives the weaker, -optimal counterpart for upper semicontinuous costs, where the infimum need not be attained.
Formalizing them. All of these results are proved in the book; none is open. As far as is known, none has a machine-checked proof: Mathlib has semicontinuity, the Hausdorff extended metric on closed and on nonempty compact sets, and the weak topology on probability measures, but no theorem combining them into a measurable selection result of this kind. A formal development would supply measurable selectors for semicontinuous minimization in Lean and the Borel-measurability of set-valued maps into the hyperspace of closed sets, both reusable well beyond dynamic programming.
The obvious attempt at the goal is to pick, for each , some minimizer of over the compact section . The minimizer exists by compactness and lower semicontinuity, but the choice is made pointwise and gives no control on measurability: a minimizer chosen by the axiom of choice need not be Borel-measurable. The argmin sets vary with only semicontinuously: they can jump from a single point to a large set, so a continuous selection generally does not exist, and continuity arguments cannot replace measurability. Lemma 7.18 isolates the hardest part: a choice of a point of each nonempty closed set that is measurable as a function of the set itself.
A second difficulty is bookkeeping at infinity. Values are allowed throughout, so sublevel sets, minima, integrals and -bounds must all be handled in ; the integral in Proposition 7.31 uses the convention , which is not Mathlib's.
EReal. The only place where values of opposite infinite sign are combined is the integral, which is the published definition DupacovaWets.Consistency.expect (reused, not restated): with an explicit case returning when , exactly the book's convention (42). The -bound of Proposition 7.34 adds a real to a value different from , which is safe in EReal.LowerSemicontinuous/UpperSemicontinuous, equivalent to Definition 7.13 for EReal-valued functions. Lemma 7.13 of the book (the sequential characterization) is Mathlib's lowerSemicontinuous_iff_le_liminf together with first countability of metrizable spaces, and is not restated here.LowerSemicontinuousOn f D (resp. UpperSemicontinuousOn); values off play no role. is Prod.fst '' D, selectors are functions on that subtype, and its σ-algebra is the Borel σ-algebra of the subspace topology.Closeds Y, and for compact is NonemptyCompacts Y, each with the Hausdorff extended metric and the Borel σ-algebra of its topology. This topology agrees with the book's (the exponential topology of Appendix C, independent of the metric).BddBelow in EReal would be vacuous and is not used.A complete development needs the Borel structure of the hyperspace (measurability of maps into Closeds Y from upper semicontinuity in the sense of Kuratowski, Proposition C.4 of the book), the construction of a measurable choice function on NonemptyCompacts Y, and approximation of semicontinuous functions by monotone sequences in . Each of these is reusable on its own; proofs of individual milestones by any route are welcome.
Many networks are built and paid for by the users they serve: multicast trees, virtual overlays, shared subnetworks of the Internet. A protocol proposes a design and a rule for splitting its cost, and each participant is free to accept the proposal or defect to a cheaper alternative. The designer therefore cannot impose the global optimum; the best it can do is propose the cheapest outcome that no participant wants to leave, a Nash equilibrium. The ratio between the cost of the best equilibrium and the optimal cost, the price of stability, measures the loss caused by requiring stability. It contrasts with the price of anarchy, which compares the worst equilibrium with the optimum and suits settings with no coordinating protocol at all.
Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 2008; preliminary version FOCS 2004) studied this question for the most common cost-sharing rule, the Shapley (equal-split) rule, under which every user of an edge pays the same share of its cost. Their first result, the subject of this mission, is that the price of stability is at most the harmonic number , where is the number of players, and that this bound is attained in the limit.
There are players and a finite set of edges. Each player has a family of feasible strategies, each a set of edges; in the network setting consists of the edge sets connecting player 's terminals in a directed graph. Each edge has a nonnegative cost . In a strategy vector , , let be the number of players whose strategy contains . Under Shapley cost sharing player pays
The cost of the designed network is
and the payments add up to exactly this amount. The profile is a (pure) Nash equilibrium if no player has a strategy with . Finally,
The game is a congestion game: the per-user cost of an edge, , depends only on the edge and its number of users. Rosenthal's potential
changes by exactly the deviating player's change in cost when a single player changes strategy. The same objects are used with load-dependent edge costs , in which case .
For every game with in which each player has a feasible strategy there is a Nash equilibrium with
and for every , the instance of Fig. 1.1 (player has its own path of cost , and all players can share a path of cost ) has a Nash equilibrium, every Nash equilibrium of it costs , and some profile costs . The ratio tends to as .
The bound shows that requiring stability under the Shapley rule costs at most a logarithmic factor, , whereas the price of anarchy of the same game is (two parallel edges of costs and already show this). It was among the first price-of-stability results and is the starting point for a line of work on network design games: the undirected case, where the bound is not tight and the correct value remained open for years, weighted players, and other cost-sharing rules. The argument (an exact potential that over- and under-estimates the social cost by bounded factors) is the standard tool for price-of-stability bounds, and Theorem 3.1 isolates it in a reusable form.
The theorem is proved in the paper; to our knowledge no machine-checked proof exists. This mission produces a formal account of Shapley cost-sharing games as congestion games, of Rosenthal's potential and the finite improvement property, of the potential-sandwich argument of Theorem 3.1, and of the matching lower-bound instance, for constant and for nondecreasing concave edge costs.
The obvious approach, bounding the cost of an arbitrary equilibrium, fails: some equilibria cost times the optimum, so any proof must select a particular equilibrium. The selection uses the finiteness of the strategy space together with the exact potential, and the bound needs the inequality , which for concave costs requires the per-user cost to be nonincreasing. On the lower-bound side, the claim that every equilibrium of Fig. 1.1 costs requires excluding all equilibria in which some players share the common path, for every at once, not only checking that the all-own profile is stable.
Games are encoded as congestion games over arbitrary finite families of edge sets, reusing the published CongestionPoA.AsymSum.Model (congestion game, loads, player costs, cost-form pure Nash equilibrium, total cost). The paper notes that its proofs do not use the graph structure; the directed-graph game is the instance in which is the family of edge sets connecting player 's terminals. Players and edges form finite types; is the number of players and is Mathlib's harmonic k cast to . The price of stability is stated as the existence of a Nash equilibrium whose cost is at most the constant times the cost of every profile, with no division by the optimum, and with the hypothesis that some profile exists. Concave costs are functions on with nonincreasing increments, nondecreasing, with ; this last condition is implicit in the paper and needed for to be nonincreasing. Theorem 3.1 carries the implicit hypothesis .
A statement that bounds every equilibrium is false, and one that asserts a cheap profile without the Nash condition is trivial; both are excluded, and the tightness part quantifies over every Nash equilibrium of the instance and asserts that one exists.
Needed infrastructure: finite improvement paths in potential games, sum manipulations over loads, and bounds on harmonic sums. The potential lemmas apply to every finite congestion game and are reusable beyond this mission. Proofs of any milestone are welcome independently.
A matching of a graph is a set of edges no two of which share a vertex. A matching with as many edges as possible is a basic object of combinatorial optimization. Assignment problems, pairing and scheduling problems, and the Chinese postman problem reduce to it, and it is the standard example of a problem with a polynomial-time algorithm that is not an instance of linear programming over a bipartite structure.
For bipartite graphs the problem was settled by the 1950s, through the theorems of König and Hall and the Hungarian method of Kuhn, whose correctness rests on linear programming duality. As Berge notes on p. 842, that duality "no longer subsists when the graph is not bipartite". C. Berge's three-page note of 1957 (doi:10.1073/pnas.43.9.842) gave the criterion that works for every graph: a matching is maximum exactly when it admits no augmenting chain.
Timeline.
Let be a finite graph without loops or multiple edges, with vertex set and edge set . A matching is a set of edges no two of which have a vertex in common. Its size is its number of edges. A matching is maximum if no matching of has more edges. This is a statement about cardinality: a matching to which no edge can be added (maximal under inclusion) need not be maximum.
Fix a matching . Its edges are strong, all other edges weak. A vertex is neutral if no strong edge contains it, and is the set of neutral points. An alternating chain is a walk in that does not use the same edge twice and in which, of any two consecutive edges, one is strong and the other weak. Vertices may repeat.
For the milestones, Berge adds a new vertex joined by strong edges to every neutral point, which gives a graph . Whenever an alternating chain of runs from to a vertex , its last edge carries an arrow from to . The non-neutral vertices then fall into four classes:
The mission's Lean development uses the same names: IsNeutral, IsAlternatingChain, IsMaximumMatching, barGraph, Arrow, IsInaccessible, IsWeakPt, IsStrongPt, IsMedium.
The statement fixes nothing beyond finiteness: the graph need not be connected, and no bound on its size is assumed.
Theorem 1 reduces the optimality of a matching, a statement about all matchings of the graph, to the absence of one kind of local structure. Its consequences include:
A matching that is not maximum can be certified by exhibiting the chain, and a maximum matching is certified by the labelling of Lemmas 1–4.
Theorem 1 has been proved since 1957 and appears in every textbook on matching theory. It is not formalized in Mathlib at the revision this mission uses. Mathlib has matchings as subgraphs, perfect matchings, alternating cycles and Tutte's theorem, but no augmenting-path characterization. This mission adds a formal statement of the theorem, together with the labelling of Berge's proof in a form that later missions on Edmonds' algorithm can reuse.
The "only if" direction is a local computation: the symmetric difference along an augmenting chain is again a matching, with one more edge. Even this needs care, because an alternating chain is only a trail and may a priori revisit vertices, while the augmentation needs a path.
The converse is the substance. In bipartite graphs, a search from the neutral points that alternates weak and strong edges labels each vertex at most one way, and its failure yields a cover of the same size as the matching. In general graphs an odd cycle lets a vertex be reached both through a strong and through a weak edge (the medium points). The bipartite labelling then fails, and no cover of size need exist: in a triangle the maximum matching has one edge and the minimum cover two. The proof has to treat these odd structures separately, and that is what Lemmas 1 and 4 do.
SimpleGraph V on a Fintype V. The paper's "unoriented graph (or 1-dimensional regular complex)" may have parallel edges, but a matching uses at most one edge of a parallel class, so nothing is lost. The matching is a subgraph M with M.IsMatching, and its size is M.edgeSet.ncard. Maximum means cardinality-maximum over all matching subgraphs. Internally stable sets and covers are Mathlib's IsIndepSet and IsVertexCover.Option V, with = none. An arrow needs an alternating chain of positive length from .IsMedium in Lean, because M names the matching.Any proof of the goal is welcome, whether it follows Berge's induction, uses the symmetric difference of two matchings, or goes through the Tutte–Berge formula. Reusable infrastructure is especially welcome: augmentation along a path, the symmetric difference of two matchings as a union of paths and cycles, and trails that alternate with respect to a matching.
Periodic-review inventory control with a fixed ordering cost is one of the oldest problems in operations research. A firm reviews its stock at the beginning of each of periods, decides whether to place an order, pays a fixed cost for every order it places, and pays holding costs on leftover stock and penalties on unmet (backlogged) demand. When demand is random and correlated across periods, and the firm's forecast evolves as information arrives, the optimal policy solves a dynamic program over the whole information state. That program is intractable in general, and in practice firms use heuristics with no performance guarantee.
Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2), 2007) gave policies with worst-case guarantees for these models, using a "marginal cost accounting" scheme that charges each unit's holding cost to the period in which it was ordered. For the model with fixed ordering costs, the stochastic lot-sizing problem, they assume that the demand of each period is known at the beginning of that period (make-to-order systems, or settings where the short-term forecast is accurate), while demand further ahead stays random and arbitrarily correlated. Under this assumption they define the triple-balancing policy and prove it costs at most three times the optimum in expectation.
Timeline:
There are periods on a probability space with a filtration : is the information available at the beginning of period . The data are a fixed ordering cost , per-unit holding costs , per-unit backlogging penalties , an initial inventory level , and nonnegative demands . The per-unit ordering cost is zero, the lead time is zero and there is no discounting. The defining assumption is that is -measurable: the demand of a period is known when the period begins. For every period there is a conditional joint distribution of the demands given , under which every conditional mean is finite.
A feasible policy is an order process with and determined by . Its inventory levels are before ordering and after ordering, and its cost is
The triple-balancing policy TB uses two rules. Let be the last period before in which TB ordered ( if none). Rule 1: TB orders in period if and only if, without an order in , the accumulated backlogging cost over would exceed . Rule 2: when it orders in , it orders
the largest quantity whose expected marginal holding cost over is at most . When it orders in period , it orders exactly enough to clear the backorders and meet . Let be the number of orders TB places.
For every instance, the triple-balancing policy TB and every feasible policy satisfy
The constant 3 is the paper's. The statement leaves the demand law, the information structure and the cost data unrestricted beyond the standing assumptions above.
Two non-milestone theorems show that the setting is not empty. A conditional demand law exists whenever demands are integrable, and a triple-balancing policy exists when .
The theorem gives a policy that can be computed online and comes with a worst-case expected-cost guarantee that does not depend on the demand distribution, the horizon or the cost data. In this setting the optimal policy is not computable in general, and the previously used heuristics have no such bound. The two lemmas separate a lower bound on every policy, in terms of TB's own number of orders, from an upper bound on TB's cost. The authors' subsequent work extends the balancing template to capacitated and multi-echelon models (§7 of the paper).
The result is proved in the paper. As far as we know, no machine-checked version exists of this theorem, of the balancing argument, or of a stochastic inventory model with correlated demand and evolving information. A formalization would check the argument, which is terse in places: the printed proof of Lemma 6.2 indexes its final sum loosely and must handle the event . It would also produce reusable infrastructure for policies adapted to a filtration, for regular conditional distributions of future demand, and for cost accounting over random intervals between orders.
The costs of TB and of an arbitrary policy cannot be compared period by period, because the two policies order at different, random times that depend on the evolving information. Any comparison has to be made over intervals whose endpoints are stopping times determined by TB, conditioned on the information at their start. At such a time the other policy may hold more or less stock than TB, and the bound must hold in both cases. Bounding each policy's cost on its own does not work: the guarantee rests on a coupling between when TB orders and what every other policy must pay over the same random stretch of time. The formal side adds a second difficulty. Rule 2 is defined through a conditional expectation viewed as a function of the order quantity, so it needs a regular conditional distribution and a measurable selection of the maximizer.
MeasureTheory.Filtration ℕ. A policy is feasible when it is nonnegative and adapted, and " known at the start of period " means is -measurable.Several trivializing formalizations are ruled out. Junk conditional expectations cannot make Rule 2 hold for every , because it uses kernel integrals in . Infinite expected costs cannot be read as . The policy class is not empty, because a separate theorem gives existence under (without some positive holding cost on the maximum in Rule 2 does not exist).
Contributions welcome: proofs of the existence theorems (measurable selection of , versions of regular conditional distributions), the stopping-time decomposition of the cost over TB's order intervals, and Lemmas 6.1 and 6.2.
Nash's theorem guarantees that every finite game has a mixed equilibrium, but says nothing about how hard one is to find. Daskalakis, Goldberg and Papadimitriou (SIAM J. Comput. 39(1), 2009) showed that computing a Nash equilibrium is complete for the class PPAD of total search problems whose solutions are guaranteed by a parity argument on a directed graph (Papadimitriou 1994). Their proof simulates an arithmetic circuit by a graphical game: a multiplayer game in which each player's payoff depends on a few neighbours only, built from small game gadgets whose equilibria compute , , , constants and comparisons on mixed-strategy probabilities.
These gadgets are the reusable core of the reduction. The PPAD-completeness results for three-player games, and the later results for two-player games and for approximate equilibria, all rest on gadget analyses of this kind.
Timeline.
A game has finitely many players; player has a finite set of pure strategies and a nonnegative payoff for each pure profile . A mixed profile gives each player a probability distribution , and denotes the product of the probabilities of the components of a partial profile . The expected payoff of a pure strategy of is .
An -Nash equilibrium (the paper's notion, an -approximately well-supported equilibrium, Eq. (2)) is a mixed profile in which no player puts weight on a pure strategy that another of its pure strategies beats by more than :
For this characterizes Nash equilibria.
A player with strategies is binary; is the probability that it plays , and is the probability that plays . The affects graph (Definition 2.2) has an edge between distinct players when the payoff of is a nonconstant function of the action of . A legal -coloring (Definition 4.8) gives each player one of colors so that the two ends of an edge differ and two distinct players with a common successor differ.
The game (Fig. 11) has inputs , output and intermediate players , all binary except , which has strategies . Its payoff tables are fixed by nonnegative integers ; the inputs' payoffs are unconstrained.
For nonnegative integers with , the affects graph of has a legal 3-coloring, and for every , at every -Nash equilibrium,
The case is exact computation at every Nash equilibrium.
The result. The paper reduces -player games to three-player games by building a graphical game from gadgets, legally coloring it with three colors, and turning each color class into one player of a normal-form game (§4.2, §4.5). Proposition 4.18 supplies a gadget that computes and can be glued into such a construction while keeping it legally 3-colorable (p. 233), at the price of an error constant instead of the constant of the elementary gadgets. The error bound is what carries the reduction over to approximate equilibria: an -Nash equilibrium of the gadget computes its function to within .
Formalizing it. All results here are proved in the paper (Proposition 4.5 is stated with the remark that its proof is similar to those of Propositions 4.2 and 4.3). None of them has a machine-checked proof, and no graphical-game or gadget infrastructure exists in Lean. The mission formalizes the known proofs and produces a library of verified gadgets with explicit error bounds, the first layer of any formal treatment of the PPAD-hardness of Nash equilibria.
Each claim is a case analysis on which strategy of an intermediate player is dominated by more than , but the cases interact. Claim 3 needs Claims 1 and 2 as inputs, and it is the step where both and are used: without them one of the regimes of cannot be excluded. The three-strategy player cannot be handled by the "binary player copies or disagrees" argument of the elementary gadgets; its weight on and on must be tracked separately. The error constants and propagate through products of approximate quantities, so a proof that is loose at any step does not reach them.
On the Lean side, the expected payoff of a pure strategy is a sum over all pure profiles of a ten-player game; every claim first has to reduce it to the few coordinates the player's payoff actually depends on.
Games, mixed profiles and expected payoffs are those of the published agt_games bundle: a finite player type, strategy types S i, payoffs u : ι → (∀ i, S i) → ℝ, AGT.IsMixedProfile, AGT.expectedPayoff. The expected payoff of a pure strategy is the expected payoff of the profile with 's strategy replaced by the point mass at . An -Nash equilibrium requires a genuine mixed profile.
Each gadget is one explicit game on its own player type, with the payoff tables of the paper. Binary strategies are Fin 2 with the paper's labels , and is the weight on 1; 's strategies are an inductive type {zero, one, star}. The input players' payoffs are unconstrained in the paper; here they are , which makes the -condition at the inputs vacuous. Since every non-input payoff depends only on gadget players, "-Nash equilibrium of the standalone gadget" quantifies over all mixed strategies of the inputs and imposes the condition exactly on the other players, which is the paper's meaning when the gadget sits inside a larger game. The affects graph is computed from the payoff functions, without self-loops, and colors are Fin k. The ranges (Proposition 4.18) and (Propositions 4.2, 4.3, 4.5) follow the paper; is added where the paper writes only .
The paper states Proposition 4.18 and Lemma 5.3 as "there is a graphical game"; an existential statement would be met by a game whose output has a dominant strategy and whose inputs are forced, so both are stated for the explicit game of the proof, with free inputs.
A complete development needs a computation lemma for the pure-strategy payoff in each gadget (reusable for any gadget on these definitions) and the case analyses of the claims. Proofs of the elementary gadgets, which are short, and of Claims 1 and 2 are good first contributions; Claim 3 is the main step.
A single machine must process a set of jobs, each with a processing time and a due date, and the cost of a schedule depends on how late the jobs finish. Total tardiness is the classical criterion, but in many applications lateness is penalised more than proportionally: a job one week late costs more than twice a job half a week late, and a quadratic or other convex penalty describes this better. Hamilton Emmons's 1969 paper in Operations Research (DOI 10.1287/opre.17.4.701) derives dominance rules for total tardiness and then asks which of them survive when total tardiness is replaced by for an arbitrary convex nondecreasing loss .
Timeline of the relevant results:
A finite set of jobs is to be sequenced on one machine. Job has a processing time and a due date . All jobs are available at time , and the machine processes them one after another without idle time. A schedule is an ordering of the jobs of . The completion time of in is the sum of the processing times of and of every job before it; its waiting (starting) time is , and its tardiness is
A loss function , convex and nondecreasing on , is fixed, the same for every job. The objective is , and a schedule is optimal if no schedule of has a smaller objective. With this is total tardiness.
Where the paper uses job indices, the jobs are indexed in SPT order: implies , or and . The notation means that some optimal schedule has before ; for a set of jobs, means that some optimal schedule has before every job of , and is the set of jobs of not in . An EDD schedule sequences the jobs in nondecreasing order of due dates.
If an EDD schedule of satisfies
then minimises over all schedules of , for every convex and nondecreasing on .
The goal fixes no constant and no particular : it is a statement about the whole class of convex nondecreasing penalties.
Two further statements of the same section are included as items: Corollary 1.3* (the SPT schedule is optimal if it coincides with the EDD schedule) and Theorem 3 for the generalised objective.
The goal says that EDD is optimal for every convex nondecreasing tardiness penalty as long as no job starts after its due date. The classical sufficient condition, that at most one job is tardy, follows from Jackson's rule; Emmons's condition allows any or all jobs to be tardy, provided each is tardy by at most its own processing time. Because the conclusion holds for the whole class of penalties at once, an instance satisfying it needs no knowledge of : total tardiness, total squared tardiness, and any other convex nondecreasing cost are minimised by the same sequence. Theorems 1* and 2* are the dominance rules that the paper's ordering procedure applies pairwise; they reduce the search space of branch-and-bound methods for convex tardiness objectives.
The results are proved in the paper (for the proofs are said to be "easily established" and omitted). None of them has, to our knowledge, a machine-checked proof. The mission produces formal statements and proofs of the generalised results, including the omitted ones, on top of a reusable single-machine model.
The total-tardiness proofs compare changes in tardiness additively: an interchange is good if the decrease in one job's tardiness is at least the increase in another's. For a convex this comparison is not enough, because a unit of tardiness costs more at higher tardiness levels; the changes must also occur at the right height on the curve, and part (b) of the proof of Theorem 1 fails for this reason. Each generalised argument therefore has to check, for every job whose tardiness changes, both the size and the location of the change, including jobs whose tardiness changes from zero to positive. Ties for the latest due date are a further obstacle: the printed proof of Corollary 2.1 cites Theorem 2, whose hypothesis is strict, so a job sharing the maximum due date is not covered by the argument as written, although the corollary is stated without excluding ties.
Jobs are elements of a type ; the job set is a Finset , processing times and due dates are real functions . Where the paper's index matters, is linearly ordered and its order is the job index, together with the SPT-indexing hypothesis. A schedule is a duplicate-free list whose elements are exactly , and completion times are the published single-machine definition MooreLateJobs.Shared.completionTime (Moore 1968), which starts the machine at time with no idle time. Optimality is against every schedule of . The relation is formalised as the existence of an optimal schedule with before (keeping the premise in the conclusion where the theorem has one); the paper's cumulative reading of the notation is not formalised.
Standing assumptions and deviations:
A trivializing formalization is ruled out: the goal requires optimality of the given EDD list against every schedule of , not of some EDD list, and a sorry-free check shows its hypotheses hold on a two-job instance in which both jobs are tardy.
A complete development needs list lemmas for moving one job to a later position, the effect of such moves on completion times, and slope inequalities for convex functions on . The schedule-manipulation lemmas are reusable for other single-machine sequencing results. Proofs of any milestone, of the two further items, and of general interchange lemmas are welcome.
In the secretary problem, items with nonnegative values arrive one at a time in a uniformly random order, and an online algorithm must decide on each arrival, irrevocably, whether to keep it. The classical version keeps one item; the rule that observes a fraction of the arrivals and then takes the first item better than everything seen picks the best item with probability at least (Ferguson 1989).
Babaioff, Immorlica and Kleinberg (SODA 2007; journal version J. ACM 2018) introduced the matroid secretary problem: the kept set must be independent in a known matroid. It models online auctions in which the feasible sets of winners have matroid structure, for example hiring along the edges of a network without closing a cycle. They gave a -competitive algorithm when the matroid is graphic, i.e. the items are the edges of a graph and a set is feasible when it contains no cycle.
Timeline for graphic matroids:
Let be a finite simple graph. Each edge has a value . A set is independent in the graphic matroid of if the graph has no cycle. The offline optimum is
The edges arrive in a uniformly random order. An algorithm sees each edge and its value on arrival and decides at once whether to select it. The selected set must be acyclic. The algorithm is -competitive if for every and every .
A partition matroid on a subset is given by a family of nonempty, pairwise disjoint parts with union : a set is independent when it lies in and meets each part at most once. Its max-weight base has value .
Definition 5.1. A random partition (a probability distribution on such families, chosen from alone) is an -partition scheme if every partition in its support has only acyclic independent sets, and for every ,
The random partition of Lemma 5.3. Pick an edge uniformly at random. With probability colour red and blue, otherwise the reverse. Colour every other vertex red or blue independently with probability . Each red vertex gets a part: the red-blue edges at . Then repeat on the edges with both endpoints blue, with fresh randomness.
The algorithm. Draw the partition, let the edges arrive, and on each part run the classical secretary rule on that part's arrivals. Output all selected edges.
For every finite simple graph and every :
Part 1 is needed for the statement to have content: an algorithm that selects every edge would otherwise satisfy part 2.
The theorem shows that the graphic matroid secretary problem admits a constant-competitive algorithm with a small explicit constant. It does so through a reduction: a random partition matroid that is feasible for the original matroid and loses only a constant factor in expectation. The reduction separates the combinatorics (Lemma 5.3) from the online part (Theorem 5.4). The same framework gives algorithms for uniform and transversal matroids and for the weighted and discounted variants on any matroid with an -partition property.
The result is proved in the paper; it has not been formalized. The mission contributes a machine-checked version of the reduction, a formal treatment of a recursively defined random partition, and the classical secretary bound in a reusable finite form. The constant is not the best known for graphic matroids (Korula–Pál improve it to ), so the formal goal is this algorithm's guarantee, not the best possible ratio.
The online half is routine once the classical bound is available: the relative order of the edges in each part is uniform, and the parts are disjoint. The difficulty is Lemma 5.3. The natural idea of using a fixed optimal forest to build the partition is ruled out because the partition must be chosen before the values are seen. The expectation bound must therefore hold for every valuation at once, for a law that depends on the graph only. The construction is recursive and random: its expected value is not a closed-form sum, and any bound has to be carried through the random sequence of blue-blue subgraphs. Feasibility needs an invariant across rounds: the parts created later live inside the blue-blue edges of every earlier round.
SimpleGraph on a Fintype vertex type with decidable adjacency. The edges are G.edgeFinset, and acyclicity of is (SimpleGraph.fromEdgeSet S).IsAcyclic. Multigraphs are not covered.v : Sym2 V → ℝ with ∀ e, 0 ≤ v e; only the values on edges matter.Finset.sup' over acyclic subsets of the edge set. A partition is a finite family of nonempty, pairwise disjoint parts inside the edge set. Its max-weight base value is the sum of the part maxima.PMF defined by well-founded recursion on the number of edges. Empty parts are dropped, and edges with two red endpoints are discarded.A complete development needs the classical secretary bound in finite form, the uniformity of induced sub-orders of a uniform permutation, expectations of PMF.bind along a well-founded recursion, and facts about forests in SimpleGraph. The first two, and a general graphic-matroid layer, are reusable beyond this mission. Proofs of any milestone, alternative proofs of Lemma 5.3, and extensions to the uniform and transversal cases of Theorem 5.2 are welcome.