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?
The bullwhip effect is the observation that the variability of orders increases as one moves up a supply chain, from the retailer towards the manufacturer and its suppliers. It was documented in industry and in classroom experiments such as the Beer Game (Sterman 1989), and analysed by Lee, Padmanabhan and Whang (1997), who named demand forecasting, lead times, batch ordering, rationing and price variations as its main causes. A remedy often proposed is to centralize demand information: give every stage of the chain the customer demand data, so that no stage forecasts from the distorted orders of its downstream neighbour.
Chen, Drezner, Ryan and Simchi-Levi (2000) quantified the effect for a retailer that forecasts with a moving average and orders with an order-up-to policy. They gave an explicit lower bound on the ratio of the order variance to the demand variance in terms of the lead time, the forecasting window and the demand autocorrelation. They then showed that in a multistage chain with fully centralized demand information this ratio still grows with the total lead time upstream of each stage. This mission formalizes that result, Theorem 3.1 of the paper, together with the single-stage analysis it rests on.
Time is indexed by the integers. The customer demands seen by the retailer follow the AR(1) model
where , , and the errors are independent and identically distributed from a symmetric distribution with mean and variance . The demand is in steady state, so that and for every .
The retailer does not know the demand process. With a window of past observations it forms the moving-average estimates
where is the lead-time parameter ( means an order placed at the end of period arrives at the start of period ) and is a constant the paper leaves unspecified. The order-up-to point is for a safety factor , and the order placed in period is . It may be negative: excess inventory is returned without cost.
In the multistage chain with centralized information, stages (stage is the retailer) all observe and use the same estimate . Stage has lead time and safety factor and uses the order-up-to point . Following the paper's sequence of events, stage orders , and stage , receiving , orders .
For every stage and every period ,
with equality when . The bound holds for every choice of the constants and of the safety factors.
with equality when .
Theorem 2.2 shows that forecasting with a positive lead time is enough to make orders more variable than demand, even for independent demands (). It also says how the effect depends on each parameter: the bound decreases in the window and increases in the lead time . Theorem 3.1 is the paper's answer to the centralization remedy. When every stage sees the true customer demand and uses the same forecast and the same policy, the variability of orders at stage is still bounded below by the single-stage expression with the cumulative lead time . Centralization reduces the bullwhip effect but does not remove it. The decentralized comparison (Theorem 3.2, where the bound becomes multiplicative across stages) is a separate mission in this series.
On the formalization side, the Gaussian special case of the single-stage results is on the platform. Snyder and Shen's Fundamentals of Supply Chain Theory states Theorem 2.2, Lemma 2.1, Eq. (4) and the AR(1) moments for normally distributed errors, as the items SupplyChainTheory.bullwhip_signal_processing, bullwhip_lemma_13_1, bullwhip_order_identity and ar1_moments. This mission states them under the paper's weaker hypothesis of a symmetric error distribution. The multistage Theorem 3.1 has no machine-checked counterpart. The paper proves only Theorem 2.2 in print. For the proofs of Lemma 2.1 and Theorem 3.1 it refers to Ryan (1997) and to a working paper, so a formalization supplies arguments the published article does not contain.
Most of the algebra is routine. The difficulty is Lemma 2.1 and the covariances like it. The estimate is a square root of a quadratic form in past demands, so its covariance with a demand cannot be computed from second moments. Under Gaussian errors one can appeal to properties of Gaussian vectors. With only a symmetric error law, every distributional fact has to come from the symmetry of the errors and from the representation of the steady-state demand as an infinite series in past errors.
The printed derivation also moves faster than a proof. Expanding from Eq. (4) produces the cross terms and , which lie outside the lags of Lemma 2.1. The display after Eq. (4) does not account for them. A complete proof of milestone 4 must show that these terms vanish too. For the chain, the stage orders are defined by a recursion across stages, and the variance of involves the estimates of all stages .
Random variables are real functions on a probability space , and time is , so that exists for every . Variance and covariance are Mathlib's ProbabilityTheory.variance and ProbabilityTheory.covariance. The demand structure ChenBullwhip.Centralized.AR1Demand records (1) for every outcome and the paper's error hypotheses: independence, identical distribution, symmetry, mean and variance . It adds four disclosed conditions:
The published Gaussian structure SupplyChainTheory.AR1Demand satisfies these conditions, so this mission generalizes the Snyder–Shen items rather than referencing them. The constants are free real parameters, and in the chain is for an arbitrary function . Lead times are natural numbers, included. Sums and run over and , and stages are numbered from . The order recursion is read from the paper's sequence of events, because the paper prints no formula for .
The orders are computed from the demands through the definitions above. They are never arbitrary random variables with assumed moments. "Tight" is formalized as equality, and orders are never truncated at zero. Without the steady-state condition, a process started from an arbitrary satisfies (1) but has time-dependent moments, and the results fail; with the ratio form would be false. Both cases are excluded by the structure, not by vacuous hypotheses. The structure is satisfiable: i.i.d. standard Gaussian demands on form an instance.
A complete development needs: the series representation of a stationary AR(1) process; distributional symmetry facts for i.i.d. sequences with a symmetric law; and covariance bookkeeping for finite linear combinations. The first two are reusable for any linear time-series model with symmetric innovations. Contributions to any milestone, and to general lemmas about stationary AR(1) processes, are welcome.
Combinatorial optimization problems are routinely solved by writing the convex hull of their feasible solutions as the feasible region of a linear program. When that convex hull has exponentially many facets, a classical trick is to add auxiliary variables: a polytope with many facets may be the linear projection of a higher-dimensional polyhedron with few. The spanning tree polytope, the permutahedron and the parity polytope all have compact descriptions of this kind. This raises the question of whether every polytope of an NP-hard problem might also have one, which would yield a polynomial-size linear program for that problem.
In the late 1980s several papers claimed polynomial-size linear programs for the traveling salesman problem (TSP). Yannakakis (STOC 1988; JCSS 1991) refuted all such claims at once by showing that every symmetric extended formulation of the TSP polytope has exponential size. He asked whether the symmetry assumption could be removed. Fiorini, Massar, Pokutta, Tiwary and de Wolf (STOC 2012; J. ACM 2015) answered the question: every extended formulation of the TSP polytope, symmetric or not, has inequalities.
Timeline.
Let be a finite index set. An extended formulation (EF) of a set is a linear system , in variables such that exactly when some satisfies it. Its size is the number of inequalities. The extension complexity is the least size of an EF of .
A polytope is the convex hull of finitely many points. A face of is itself or its intersection with a valid hyperplane, and a facet is a maximal proper face. A polytope is an extension of if for some linear map . Given , the slack matrix has entries . The nonnegative rank is the least with , where has columns and has rows.
For -bit strings , is the number of common ones, and is the matrix . A 1-monochromatic rectangle cover of its support is a family of products , each containing only entries with , that together contain all of them.
On the complete graph , is the characteristic vector of an edge set and is the cut of . The polytopes are
The constant is left unfixed, so the goal survives any improvement of it.
The theorem rules out every polynomial-size linear programming formulation of the TSP polytope, in any number of auxiliary variables, which settles Yannakakis's question. The cut polytope bound does the same for max-cut, and the stable set bound for the stable set problem on general graphs. The results do not depend on P vs NP: they concern one specific model of computation, linear programs whose feasible region projects onto the polytope. They started a line of work on extension complexity, including perfect matching (Rothvoss), approximate EFs and semidefinite lifts.
Formalizing the result would produce a machine-checked chain from a communication-complexity bound to a polyhedral one. The paper's results are proved; the input of Theorem 1, Razborov's bound, is only cited, and is posed here as a separate target. To our knowledge none of these statements has a formal proof in Lean or another proof assistant. The polyhedral layer (Yannakakis's theorem, faces and extensions) and the matrix layer (nonnegative rank, rectangle covers) can be reused for later extension-complexity results.
The obvious approach, bounding the number of facets of the TSP polytope, does not work: extended formulations exist precisely because a projection can have far more facets than the lifted polyhedron. Any lower bound must cover every lifting at once, which means working with the nonnegative rank of a slack matrix rather than with any concrete formulation. Ordinary rank is no help, because has rank . The step that carries the weight is Razborov's distributional bound for disjointness, a nontrivial piece of communication complexity. On the polyhedral side, Lemma 11 needs a reduction from 3SAT to a directed and then an undirected Hamiltonian cycle problem, realized as a face of with . Theorem 12 also needs a monotonicity of in that the paper only indicates.
Sym2 (Fin n)). is indexed by ordered pairs, and the Frobenius product is the dot product over ordered pairs. Bit strings are Fin n → Bool.sInf of the attainable sizes), never , so no lower bound can hold through an infinite value. The size of an EF counts inequalities only.The dynamic lot size model asks when, and how much, to order of a single item over a planning horizon of periods with known, time-varying demands, setup costs, unit order costs and holding costs. It is the textbook model of production planning and the building block of material requirements planning, multi-item scheduling and many decomposition schemes for larger supply-chain problems.
Wagner and Whitin (1958) showed that some optimal policy orders only when inventory is zero, which turns the problem into a shortest-path recursion with running time. For more than thirty years this was the standard algorithm. In 1991 three groups independently reduced the complexity: Federgruen and Tzur (Management Science 37(8), 1991), Wagelmans, van Hoesel and Kolen (Operations Research 40, 1992) and Aggarwal and Park (Operations Research 41, 1993). Each obtained in general and under special cost structures. The Federgruen–Tzur algorithm is a forward algorithm: at iteration it keeps a short list of periods that could still be the best last setup period for some future horizon, and updates it by local tests on neighbouring entries. This mission formalizes the theorem that justifies those tests.
For periods let be the demand, the setup cost, the variable per unit order cost and the cost of carrying a unit of inventory at the end of period . Write and , so . For let , let , and let
be the carrying cost of an order placed in period that covers the demands of periods .
The costs are given by the zero-inventory recursion (2): and, for ,
is the cost of the first periods when the last setup is in period .
For two periods the difference is affine in , with intercept given by (4) and slope . Its root is defined by (5): when the slopes differ, and or according to the sign of when they agree. It is extended symmetrically, .
At iteration the future demands are unknown, so a future horizon has a potential cumulative demand . The th Minimal Optimal Predecessors list is the set of periods that are the lowest-index optimal last setup period, among , for every potential cumulative demand in some open interval above .
Let and let with , ranked so that , with equal -values in ascending order of index. Put and for . Then
In attack order:
A supporting item potCost_spec certifies that the potential costs used to define agree with the paper's , up to a term that does not depend on .
Theorem 1 is what makes the forward algorithm correct. Part (a) reduces the minimality of a candidate list to a condition on consecutive pairs of a sorted list. Part (c) says which entry to delete when the condition fails. Part (b) says where to read off the optimal last setup period. With these, is maintained by deletions at the ends and in the interior of a list ordered by , and each period is inserted and deleted at most once; the bound, and the bound under the paper's special cost structures, follow from this bookkeeping. The same lower-envelope reasoning appears in the other 1991–1993 algorithms and in later extensions to backlogging and capacitated variants.
The result has a complete published proof. To our knowledge there is no machine-checked development of the Wagner–Whitin recursion or of any of the fast lot-sizing algorithms. This mission produces the model, the breakpoints and the Minimal Optimal Predecessors lists as reusable definitions, and a checked proof of the characterization. It also records two small corrections that a formal reading forces on the printed text (see Formalization scope).
Each piece in isolation is elementary algebra on affine functions. The difficulty is in the combinatorics of the lower envelope with ties. The natural argument "consecutive breakpoints increase, so each line owns an interval" must handle three things:
The "only if" direction needs every failure of (6) to be traced to an element that is never the unique lowest-index optimum on an interval. Ties are exactly where the printed definition of , read literally at a single demand value, breaks the theorem. A proof that ignores ties proves a statement that is false.
EReal, so are kept distinct from every real number. The final "" of (6) is part of the condition.List ℕ. Lean lists are 0-based, so the paper's and are entry and gval j L m.(r, Q) policies are the standard replenishment rule for a single item under continuous review: whenever the inventory position (stock on hand plus on order minus backorders) drops to the reorder point , an order of size is placed. They are known to be optimal in the classical models with Poisson or compound renewal demand, constant or exogenous lead times and full backlogging, and they are used widely in practice and in multi-item and multi-echelon systems where they are applied item by item.
For decades, computing an optimal pair exactly was not routine. The textbook treatment of Hadley and Whitin (1963) gives approximations; as Browne and Zipkin (1991) put it, "until recently, there was no reliable, straightforward method for computing an optimal (r, Q) policy, even in the simple case of Poisson demand processes." Many heuristics were proposed (surveyed by Lee and Nahmias, 1989); the only exact procedure in circulation was in Zipkin's classnotes, based on a result of Sahin (1982).
Federgruen and Zheng (1992) give a short exact algorithm, Algorithm OPT, whose work is linear in the optimal order quantity . It rests only on the form of the cost, not on a particular demand model.
Inventory positions are integers (demand arrives unit by unit). A fixed cost is charged per order, and is the expected holding and backlogging cost rate as a function of the inventory position . In all the models of the paper the long-run average cost of the policy, for an integer and an integer , has the form
The paper's standing assumptions on are:
The sequence . Let be an integer minimizing . Given , let and , and set
So the window grows by one point at a time towards the smaller neighbouring value, ties going left. Write for an optimal reorder point for a given , and
Algorithm OPT, Step 1. Variables start at , , , , . Each pass compares and ; on the smaller side (left on ties) it stops if is at most that value, and otherwise adds the value to and moves one step left or one step right; then and . The output is the final .
Under the standing assumptions, Step 1 of Algorithm OPT, started from any global minimizer of , stops after finitely many passes, and its output satisfies and
The goal fixes no constants and no demand model: it is a statement about every satisfying the standing assumptions.
The result turns the joint minimization of (1) over , an unbounded two-dimensional integer problem, into a single scan whose length is plus the distance to the minimizer of . Because it uses only the form (1) and the unimodality of , it applies at once to Poisson and compound Poisson demand, to stochastic lead times with an equilibrium lead-time demand, and to cost structures with stockout penalties; the paper also notes extensions to policies. Lemma 1 and Corollary 1 additionally give the structure of the optimal reorder point as a function of .
The result has been proved on paper since 1992. What this mission adds is a machine-checked proof of the algorithm's correctness for general under exactly the paper's hypotheses. The platform already has the linear-cost special case of the underlying lemmas for one discrete demand model (InventoryControl.rq_discrete_recursion, rq_discrete_joint_optimal), but with and given as hypotheses and no algorithm; nothing on the platform states the algorithm or treats general unimodal .
The obvious argument says: for fixed the sum in (1) should cover the smallest values of , and the greedy window collects exactly those. Both halves need care on the integers with flat stretches of : "the smallest values" is ambiguous under ties, and the claim that a greedy window holds them relies on being a global minimizer together with the unimodality of , not on convexity.
The stopping rule is the second point. Lemma 2 looks like a first-order condition, but need not be convex; optimality of the first stopping for all larger uses that the values are nondecreasing along the sequence, which the paper uses without stating. Termination of the algorithm is not discussed on the page; it needs , and fails for constant .
Finally, the goal is about an imperative loop. Connecting its five variables to , and is an invariant argument that has to match the tie-breaking and the non-strict stopping tests exactly.
NegUnimodal G: , antitone on and monotone on . "" is Coercive G: along atBot and atTop. Mathlib's QuasiconvexOn ℤ is not used: over -weights it holds for every function.Proofs of any milestone are welcome, as are general lemmas on windows of unimodal integer sequences, which are reusable beyond this mission.
Myerson's optimal auction (Myerson 1981) maximizes a seller's expected revenue when buyers have independent private values, but it is a sealed-bid mechanism: every buyer reports a value, and the allocation and payments are computed from all reports at once. Real sellers more often post prices: buyers arrive, each sees a take-it-or-leave-it price, and buys or leaves. Chawla, Hartline, Malec and Sivan (arXiv:0907.2435) ask how much revenue such simple mechanisms lose. Their strongest notion is the order-oblivious posted-price mechanism (OPM): the prices are fixed in advance, and the guarantee must hold whatever order the buyers arrive in, even an adversarial one.
The tool behind the guarantee for sellers of identical units is a prophet inequality. In the single-choice version, a gambler inspects independent random rewards one at a time and must accept or reject each on the spot; Krengel and Sucheston, and Samuel-Cahn (Ann. Probab. 1984), showed that a single fixed threshold earns at least half of what a prophet who sees all rewards earns. The paper extends Samuel-Cahn's threshold rule to choices (Appendix D.2) and turns it into a revenue guarantee (Theorem 10).
There are agents . Agent 's value for being served is drawn independently from a distribution with density ; the virtual valuation is (Definition 1), and is regular if is non-decreasing (Definition 2). The seller may serve any set of agents in a downward-closed set system ; this mission uses the -uniform matroid, where a set is feasible exactly when it has at most members.
A mechanism maps reported values to an allocation and payments . It is truthful if reporting the true value is a dominant strategy and no agent ever gets negative utility. Its expected revenue is , and denotes the revenue of Myerson's mechanism, the largest over truthful mechanisms (Theorem 19).
Given prices and values , agent desires service if . Let be the class of maximal feasible sets of desiring agents. When agents arrive in an arbitrary order and each buys if it desires service and can still be feasibly served, the set of buyers lies in . The paper's pessimistic revenue estimate is
For the prophet inequality, are independent nonnegative random variables with order statistics , and . The threshold rule with threshold picks indices , where is the lesser of and the -th smallest index with (or if there is none). The numbers and are the unique solutions of
for every instance with regular distributions and a -uniform matroid constraint. The prices are chosen once, before the mechanism it is compared with; this is the paper's " 2-approximates ".
The theorem says that a seller of identical units can fix one price per buyer, ignore the arrival order entirely, and still collect half of the optimal revenue. The factor 2 is tight: Appendix D.2 gives a single-item example with two buyers where no order-oblivious pricing does better. Corollary 11 extends the result to partition matroids, and Theorem 24 is reused for the graphical-matroid result (Theorem 12, App. D.3). Theorem 24 is a statement in optimal stopping independent of mechanism design, and -choice prophet inequalities are now a standard tool for online allocation.
The results are proved in the paper (preprint arXiv:0907.2435v2; a conference version appeared at STOC 2010). To our knowledge none of them, nor any prophet inequality, has a machine-checked proof; Mathlib has independence of random variables but no order statistics, stopping-rule prophet inequalities, or Myerson's revenue characterization in this multi-agent dominant-strategy form. A related single-unit, Bayesian-incentive-compatible form of Proposition 1 exists on the platform (MechanismDesign.Auctions.revenue_eq_virtual_surplus), in a different model.
The threshold rule picks the first values above , not the largest, and its picks are dependent random indices; the expectation does not factor. The obvious comparison of the gambler with the prophet term by term fails, because the gambler can exhaust its picks on early, small values. The bound has to balance two events: either at least values reach , or a value is picked whenever it exceeds ; independence enters exactly in the second. The rule also has forced picks at the end of the sequence, which must be handled as stated.
On the mechanism side, is a minimum over an adversarially chosen family, not the revenue of one run, so it cannot be read off from a single sequential mechanism. Proposition 1 needs the full revenue-equivalence argument: monotone allocations, the payment identity, and an integration by parts against the density.
Useful reusable infrastructure: order statistics and their measurability, Samuel-Cahn-type threshold rules, and Myerson's payment identity for dominant-strategy mechanisms. Proofs of any milestone, and supporting lemmas on these objects, are welcome.
A seller who knows the distributions of buyers' values can maximise expected revenue with Myerson's optimal mechanism (Myerson 1981): collect bids, compute virtual values, serve a feasible set of maximum virtual surplus, and charge threshold payments. Real sellers seldom run such auctions. They post prices: a buyer is offered a take-it-or-leave-it price and either accepts or walks away. Posted prices need no bidding, involve no competition between buyers, and are trivially truthful. The question is how much revenue they give up.
Chawla, Hartline, Malec and Sivan (arXiv:0907.2435, STOC 2010) answer this for a range of feasibility constraints with a single construction, the sequential posted-price mechanism (SPM) . For general matroids it loses at most a factor (Theorem 5). For uniform and partition matroids, that is, multi-unit sales and unions of multi-unit sales, it loses at most a factor (Theorem 6), and the paper shows this factor is tight for its mechanism. This mission targets Theorem 6.
Timeline. Myerson (1981) characterised the optimal single-parameter mechanism. Blumrosen and Holenstein (2008) showed that the best single-unit SPM can be a factor below Myerson's revenue even with i.i.d. buyers. Chawla, Hartline and Kleinberg (EC 2007) used posted prices to approximate multi-parameter unit-demand pricing. Chawla, Hartline, Malec and Sivan (2010) gave the matroid, partition-matroid and matroid-intersection bounds. Yan (SODA 2011) explained the factor through the correlation gap of submodular functions and sharpened it for units to .
There are agents. Agent has a private value for being served, drawn independently from a distribution with density . The virtual value is , and is regular if is non-decreasing. The seller may serve any set in a downward-closed family .
A partition matroid assigns each agent to a part and each part a capacity . A set is feasible iff it contains at most agents of every part . With one part of capacity this is the -uniform matroid: at most agents are served.
A truthful mechanism maps a value vector to a feasible set and payments . It is dominant-strategy incentive compatible and individually rational. Its expected revenue is , and is its service probability for agent .
The sequential posted-price mechanism built from sets the price for agent , so that agent accepts with probability exactly . It approaches the agents one at a time in decreasing order of price ( is the ordering). It offers agent the price if adding to the agents already served keeps the set feasible. The agent accepts iff . Its expected revenue is .
For every partition matroid, every truthful , and built from as above,
Taking to be Myerson's mechanism gives the paper's statement.
The theorem shows that a mechanism with no bidding loses at most about of the optimal revenue when the constraint is a union of multi-unit supplies. That covers selling several kinds of goods, each in limited stock, to single-minded buyers. The prices are computed once from the distributions. The order is fixed before any value is seen. No agent's payment depends on another agent's report. The factor is tight for this mechanism (App. C.2), and the same template (prices from service probabilities, decreasing order) gives factor for all matroids and for intersections of matroids.
On the formal side, the paper's results are proved but none is machine-checked as far as we know. The platform has Myerson-type results for a single unit with Bayesian incentive compatibility and a common support (Börgers), and for i.i.d. buyers with a fixed number of units (Talluri and van Ryzin). Neither covers independent, non-identical buyers under a set-system constraint with dominant-strategy truthfulness. A complete development would include the ex-ante revenue bound of Lemma 2 for regular distributions, which is reusable for any posted-price or prophet-inequality argument, and the correlation-gap inequality.
The obvious argument compares with Myerson's mechanism one agent at a time. That fails, because may stop offering to an agent once the units of its part are gone, and the agents blocked this way can be the ones Myerson's mechanism serves. The loss has to be bounded in aggregate, using only the ex-ante constraint . The single-unit case reduces to an inequality about products . For units, the printed proof (pp. 15–16) is an induction that compares the run with a hypothetical single-unit instance with probabilities . Its second case is informal, so a formal proof needs its own argument for the -unit bound. Passing from uniform to partition matroids needs the observation that with a global order the run inside each part depends only on that part's agents. Lemma 2 needs the revenue-curve concavity that regularity gives, stated through densities rather than derivatives.
Welcome contributions: proofs of the algebraic milestones (Lemma 20, display (3)), the revenue formula, Lemma 2 (reusable payment-identity infrastructure for dominant-strategy mechanisms), and a correlation-gap argument for units.
A seller who must decide whom to serve among several buyers with private values can, in principle, run Myerson's revenue-optimal mechanism: collect bids, compute virtual values, serve the feasible set of largest virtual surplus, and charge threshold payments (Myerson 1981). In practice sellers rarely do this. Retail, ticketing and online platforms mostly use posted prices: each buyer is offered a take-it-or-leave-it price and accepts if and only if the price does not exceed the buyer's value. Posted prices are simple to explain, are trivially truthful, and do not require buyers to reveal their values.
Chawla, Hartline, Malec and Sivan (arXiv:0907.2435, STOC 2010) asked how much revenue is lost by this simplification, and showed that for a wide range of feasibility constraints a sequential posted-price mechanism recovers a constant fraction of the optimal revenue. The matroid case, a factor of 2, is the first and most widely cited of their results. It is a revenue analogue of the prophet inequality and was one of the starting points of the literature on "simple versus optimal" mechanisms.
There are single-parameter agents, indexed by , and one seller. Agent has a private value for being served, drawn independently from a distribution with density . The virtual valuation of agent is
and is regular if is non-decreasing.
The seller faces a feasibility constraint: a downward-closed family of subsets of , the sets of agents that can be served together. The rank of a set is . The constraint is a matroid if it satisfies the augmentation axiom: whenever and , some has . Examples are identical units (-uniform matroids) and disjoint markets with separate capacities (partition matroids).
A mechanism maps reported values to a feasible set of served agents and a payment for each agent. It is truthful if reporting the true value is a dominant strategy and no agent ends with negative utility. Its expected revenue is , and is the probability that it serves agent .
A sequential posted-price mechanism (SPM) with ordering and prices approaches the agents in the order . When agent 's turn comes, if adding to the set of agents served so far keeps feasible, is offered price and is served (and pays ) if ; otherwise is blocked. Its expected revenue is .
The mechanism of the paper sets , so that agent accepts an offer with probability exactly , and approaches the agents in decreasing order of price.
For regular, independent values and a matroid constraint, for every truthful mechanism and the SPM built from its service probabilities,
Taking to be Myerson's optimal mechanism gives the paper's statement that 2-approximates the optimal revenue.
The theorem shows that under a matroid constraint the optimal mechanism's advantage over a single round of posted prices is at most a factor of 2, uniformly over all regular distributions. Prices, rather than an auction, then suffice up to a constant, which justifies posted pricing in settings where an auction is impractical. The same argument, with the matroid replaced by an intersection of matroids, gives the paper's Theorems 7 and 8, and the bound underlies the analysis of VCG with reserve prices (Theorem 32). Lemma 2's benchmark became a standard tool for "ex ante relaxation" arguments.
The results are proved in the paper; none of them has a machine-checked proof. Formalizing them requires Myerson's revenue characterization in a multi-agent, dominant-strategy setting with a general feasibility constraint, which Lean's libraries do not have, and a probabilistic analysis of a sequential process over a product measure. Related formalizations exist for narrower models: the single-unit, Bayesian incentive compatible revenue identity MechanismDesign.Auctions.revenue_eq_virtual_surplus (Börgers' textbook, common support) and the i.i.d. multi-unit RevenueManagement.revenue_equivalence. Neither covers per-agent supports, set-system constraints or dominant-strategy truthfulness.
The obvious argument compares the SPM with the hypothetical mechanism that ignores the feasibility constraint, whose revenue is exactly . The SPM loses the revenue of agents who would have accepted but are blocked. The difficulty is that blocking is correlated with the values of earlier agents, and the lost revenue must be bounded by revenue actually collected. A naive per-agent charge fails in a general matroid, because one served agent can block many others; the bound has to use the matroid's rank structure together with the decreasing price order.
On the mechanism side, Lemma 2 needs the full Myerson theory: monotonicity of truthful allocations, the payment identity, and an optimization over interim allocation rules with a fixed service probability, where regularity is used.
All objects live in the namespace CHMSPricing.SpmMatroid. Agents are Fin n. The following conventions are fixed.
The goal cannot be trivialized by a free choice of prices: the prices are tied to the mechanism's service probabilities, and the SPM uses the same matroid as the mechanism. Individual rationality is essential, since without it a "truthful" mechanism can extract unbounded revenue.
A complete development needs Myerson's lemma for dominant-strategy single-parameter mechanisms, a quantile/revenue-curve argument under regularity, matroid span and rank facts for the paper's finite set systems, and independence arguments for a sequential process on a product measure. The rank bound and the deterministic lost-revenue inequality are independent of the probabilistic parts and are good first contributions; the Myerson-side lemmas are reusable for the other missions of this series.
A shop that promises delivery dates is judged by how late its orders are, not by how early. For a single machine processing jobs that are all available at time , the total tardiness of a processing order,
charges each job the amount by which its completion time exceeds its due date , and nothing for finishing early. It is one of the basic criteria of deterministic scheduling (Conway, Maxwell and Miller, Theory of Scheduling, 1967), and the single-machine problem of minimizing it is the core subproblem of many dispatching and decomposition methods.
Two contrasting rules are classical. Sequencing in order of shortest processing time (SPT) minimizes total lateness and total completion time (Smith, 1956), and it minimizes total tardiness when every job is tardy under it. Sequencing by earliest due date (EDD) minimizes total tardiness when at most one job is tardy under it. Between these extremes no simple rule is optimal, and before 1969 the proposed exact methods (Held and Karp, 1962; Lawler, 1964; Elmaghraby, 1968) searched subsets of schedules.
Timeline.
This mission formalizes Emmons's SPT side: the pairwise dominance theorem for a shorter job before a longer one, and its corollary that the SPT schedule is optimal under a condition far weaker than "every job is tardy".
A finite set of jobs is processed on one machine. Job has a processing time and a due date . A schedule of is an ordering of the jobs of ; the machine starts at time , never idles, and processes the jobs in that order, so a job's completion time is the sum of the processing times of the jobs up to and including it. Its tardiness is , and the schedule's total tardiness is . A schedule is optimal if no schedule of has smaller total tardiness.
Following Emmons, jobs are SPT-indexed: are numbered so that implies , or and . The SPT schedule processes in this order.
Emmons's notation (" precedes in an optimal schedule") means that there exists an optimal schedule having all properties already established and in which comes before . The set collects the jobs already known to precede .
The condition can be read as with the SPT completion time of , so it allows jobs to be early. It is the paper's sufficient condition for SPT optimality, and the conclusion is optimality against every schedule of .
Two further results are included as supporting statements: Corollary 1.2 (p. 705, last) and Corollary 2.3 (p. 707, the adjacent-pair rule iff after a waiting time ).
Corollary 1.4 turns an NP-hard problem into a closed-form answer on a recognizable class of instances: one pass over the SPT order checks the condition, and if it holds no search is needed. Theorem 1 is the more general tool. It orders pairs of jobs in an optimal schedule, and together with Emmons's companion theorems it underlies later exact methods for total tardiness, including Lawler's decomposition and the branch-and-bound algorithms that use Emmons's dominance rules for pruning.
The results are proved in the paper. What a formalization adds is a checked account of the step that the paper treats informally: dominance statements are existential ("some optimal schedule has before "), and the paper argues on p. 702 that such statements can be accumulated. Each statement here makes explicit which previously established properties the new optimal schedule keeps. No machine-checked proof of these results was found on Prove2Me or in Mathlib at the time of drafting.
The obvious argument is a pairwise interchange, but the interchanged jobs are not adjacent. Moving from before to 's position shifts every job in between, changes two tardiness terms in different directions, and the comparison depends on where the due dates fall relative to the start of and the end of . The hypothesis involving only controls the start time of through the information that precedes it, so the existence statement must carry that information along.
The goal is not a direct consequence of Theorem 1 applied pairwise: existential conclusions for different pairs need not hold in a common optimal schedule. Optimality of one fixed order requires all the pairwise decisions to be realized simultaneously, and the problem changes (due dates shift) once a job is fixed in place.
Jobs are elements of a type with a linear order that plays the role of the paper's index, and the job set is a Finset ι; this lets the reduction remove a job and keep the remaining labels. Schedules and completion times are the published definitions MooreLateJobs.Shared.IsSchedule and MooreLateJobs.Shared.completionTime (duplicate-free lists containing exactly the jobs of ; prefix sums of processing times from time ). Tardiness, total tardiness, optimality (against every schedule of ), "precedes" (comparison of positions), the SPT indexing convention and the SPT schedule (the jobs sorted by index) are defined in EmmonsTardiness.SPT.Model. Processing times and due dates are real.
Conventions and deviations from the page:
A formalization of the goal as "some optimal schedule starts with ", or of Theorem 1 with an arbitrary set unrelated to optimal schedules, would be a different and weaker (or false) statement; the targets above state optimality of the SPT schedule itself and tie to an optimal schedule.
Needed infrastructure: lemmas on prefix sums of lists, on the effect of a transposition on positions in a duplicate-free list, on removing the head of a schedule, and existence of an optimal schedule among the finitely many permutations of . These list-scheduling lemmas are reusable for other single-machine results (Moore 1968, and the EDD mission of this series). Proofs of the milestones, alternative arguments, and general interchange lemmas are all welcome.
A function that is bounded below need not attain its infimum: on has infimum and no minimizer. The classical "variational principle" says that at a minimizer of a differentiable functional, . Without compactness there may be no minimizer, and the principle has nothing to say. In 1974 Ivar Ekeland showed that a weaker statement survives in every complete metric space: next to any approximate minimizer lies a point that is the exact, strict minimizer of a slightly perturbed function (Ekeland 1974).
The result is now a standard tool in nonlinear analysis, optimization and the calculus of variations. It yields approximate first-order conditions () without existence of minimizers, approximate Lagrange multiplier rules, and approximate maximum principles in optimal control; Ekeland's survey (Ekeland 1979) collects many of these uses.
Timeline. Bishop and Phelps introduced the partial order on a Banach space times that underlies the proof, in their study of support functionals of convex sets (Bishop–Phelps, The support functional of a convex set, Proc. Symp. Pure Math. 7, AMS, 1963). Brøndsted and Rockafellar used it in 1965 to obtain subdifferentiability properties of convex functions on Banach spaces (Brøndsted–Rockafellar 1965), and Browder applied it to nonconvex subsets of Banach spaces (Bull. AMS 79, 1973). Ekeland's 1974 article, formalized here, isolates the device as a principle valid in every complete metric space for lower semicontinuous functions with values in , and applies it to Gâteaux-differentiable functions, constrained optimization, Plateau's problem, geodesics and optimal control.
Let be a complete metric space. Let be lower semicontinuous (for every the set is closed), not identically , and bounded from below:
For , a point is an -minimizer if
For , the Bishop–Phelps order on is
In Lean it is EkelandVP.General.bpLE α p q, read . The epigraph of is (1.15).
In §2, is a real Banach space with dual , and is Gâteaux-differentiable with derivative (EkelandVP.General.IsGateauxDiff F F'): at every with , for every (2.1).
For every satisfying (1.2) and every there is with
The parameters and are free; the trade-off between closeness to and the size of the perturbation is the content of the theorem.
The result. Theorem 1.1 replaces "a minimizer exists" by "a strict minimizer of a Lipschitz perturbation exists nearby", with explicit control of both the distance and the perturbation. With this gives a point that is -optimal, -close to , and -stationary in the metric sense. Corollary 2.3 is the form announced in the paper's abstract: a differentiable function with a finite lower bound has points where is almost minimal and is arbitrarily small. Later sections of the same paper use Theorem 1.1 for approximate Lagrange multiplier rules (§3) and an approximate Pontryagin maximum principle (§7), which are the subjects of missions II and III of this series.
Formalizing it. The theorem is proved; this mission formalizes the paper's own route (the order (1.6), Lemma 1.2, then Theorem 1.1) and its first applications in §2. The pinned Mathlib has no statement of Ekeland's principle, of the Caristi fixed point theorem, or of the Bishop–Phelps order, and the platform has none either. A machine-checked Theorem 1.1 for extended-real-valued functions would be directly reusable by every later mission that needs approximate optimality without compactness.
The obvious argument — take a minimizing sequence and pass to a limit — fails because nothing makes a minimizing sequence converge: is not compact, and a minimizing sequence of escapes to . Completeness only helps for Cauchy sequences, so one must construct a sequence that is Cauchy. The limit must moreover be maximal for the order (1.6), not merely a limit point, and that maximality is what produces the strict inequality (1.5). Lemma 1.2 is where this difficulty sits. In §2, the passage from the metric statement (1.5) to a bound on requires to be finite near along every line, which the Gâteaux hypothesis supplies.
MetricSpace with CompleteSpace; is dist u v. carries the product topology; only closedness of subsets of it is used.EReal. "Bounded from below" (1.1) is ; it also excludes the value , which the paper's codomain does not contain. "Not identically " is . Lower semicontinuity is Mathlib's LowerSemicontinuous.lam.EReal subtraction is ordinary.NormedSpace with CompleteSpace, is a function , and Gâteaux differentiability requires to be finite near before taking a real derivative; without this, EReal.toReal would let an infinite function have a junk derivative. Density of is stated for derivatives taken at points where .Contributions welcome: proofs of the milestones (the first two are short; Lemma 1.2 is the core), of Theorem 1.1, and of the §2 corollaries; a reusable Caristi fixed point theorem built on the same order would be a natural addition.
A call center with agents facing Poisson arrivals at rate and exponential service at rate is the M/M/N (Erlang-C) queue. Choosing trades the cost of agents against the cost of customers waiting, and in practice it is done with the square-root safety-staffing rule , where is the offered load. Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; published in Operations Research 52(1), 2004, doi:10.1287/opre.1030.0081) turned that rule of thumb into an optimization result: for a general convex staffing cost and a general waiting-cost function, they identify the safety factor that makes the rule asymptotically optimal as the arrival rate grows.
Timeline of the asymptotic regime the paper builds on:
This mission is the first of a series of four on that paper and covers the rationalized regime (Section 5), where staffing and waiting costs are of the same order.
The service rate is fixed and the arrival rate grows. A staffing cost , defined on , is convex and strictly increasing; it does not depend on . For each a waiting-cost function satisfies , is strictly increasing on , and makes
finite for every . With the Erlang-C formula
the expected total cost of staffing agents is , and is any integer minimizing it (7).
In normalized units the paper defines , , the continuous delay probability with
and , minimized at (8). A surrogate approximates it. Rounding is measured by
The Halfin–Whitt delay function is , with the standard normal hazard rate (11). Asymptotic equality means as .
Assume the rationalized condition (18): for some , . Let minimize over (19). Then
The goal fixes no constant and no rate: it asserts only that the excess cost of the explicit rule is asymptotically the optimal excess cost.
The theorem justifies the square-root staffing rule from first principles for a broad cost class. In Example 5.3 of the paper (linear staffing cost per agent, linear waiting cost per unit time) it gives , with the minimizer of , a one-dimensional rule computable once for all loads. Corollary 3.3 is reused verbatim by the efficiency-driven and quality-driven theorems of the paper (missions II and III of this series), and Lemma 4.1 is the analytic input of all three.
The result has been proved since 2000; no machine-checked proof of it, or of the Halfin–Whitt limit for the continuous extension , is known to exist. The mission produces a formal proof of the regime theorem together with reusable formal statements of the Erlang-C function, its integral representation, and the Halfin–Whitt limit.
The reduction from discrete to continuous staffing (Lemmas 3.1–3.2) is elementary once unimodality of is available, but unimodality rests on convexity of , which the paper cites rather than proves, and on Lemma C.1, which needs differentiation under an improper integral. The central difficulty is Lemma 4.1: the paper derives it from Halfin and Whitt's limit theorem, which is stated for integer server counts, while is evaluated at non-integer ; a proof needs a uniform Laplace-type asymptotic for the integral defining . A further obstacle is bounding : the obvious route through continuity of the optimizer fails because nothing converges, and the paper instead argues by contradiction via (14).
All objects live in DimCallCenters.Rationalized. The arrival rate is a real lam, and every limit is Filter.atTop on with fixed. The queue itself is not modelled; the paper's theorems are statements about the closed-form cost , and so are these. Committed conventions:
WaitModel (; ; strictly increasing on ; integrable on for every , which is the paper's finiteness of ). is convex and strictly increasing on .∃ᶠ/∀ᶠ, not Filter.limsup on .The hypotheses are met by linear staffing and waiting costs (, ), for which (18) holds with , so the goal is not vacuous. It is not trivialized by junk values either: the ratio's denominator is positive at every , and never evaluates at an unstable level.
Needed infrastructure: Laplace asymptotics for , differentiation under the integral sign for , and convexity of . All of these are reusable for missions II–IV. Proofs of the milestones in any order are welcome, as are proofs of the convexity facts the paper cites from its references [9], [10].
The single-server queue with general independent interarrival and service times, the G/G/1 queue, is the basic model of a congested resource: a machine, a link, a checkout. For Markovian arrivals or services the mean wait has a closed form (the Pollaczek–Khintchine formula for M/G/1, the geometric law for G/M/1). For general distributions it has none, and the mean wait depends on the whole distributions of the interarrival and service times, not only on their moments. Capacity planning still needs numbers. Bounds that use only the first two moments are therefore the practical tool. They say how bad congestion can be for any queue with a given arrival rate, service rate and variabilities, and they become exact as the traffic intensity approaches one.
This mission formalizes Chapter 7, §7.1 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651), together with the heavy-traffic Theorem 7.1 of §7.2.3.
Timeline. Lindley (Proc. Cambridge Philos. Soc., 1952) derived the recursion for successive waiting times and characterized the stationary law. Kingman (Proc. Cambridge Philos. Soc., 1961, 1962) proved the heavy-traffic exponential limit. In "Some inequalities for the queue GI/G/1" (Biometrika, 1962) he proved the two-moment upper bound. Marshall (1968) derived further moment relations and bounds (Operations Research, 1968). Marchal (Operations Research, 1978) gave the lower bound (7.14).
A G/G/1 queue is specified by two probability laws on : the law of an interarrival time and the law of a service time . Both have finite second moments, and
The pairs are independent and identically distributed, and is independent of . Customers are served first come, first served. The line delay of the th customer obeys Lindley's recursion
and is independent of . The idle gap is the time between the th departure and the next start of service.
The queue is stationary when the law of does not depend on , that is, when one step of (7.1) maps to itself. The mean stationary line delay is . In the Lean development these objects are IsGG1Input A B lam mu, lindley, idleX, IsStationaryWaitLaw A B ν and meanWait ν, in the namespace QueueingFundamentals.Bounds.
For every stationary G/G/1 queue with , is finite and
The goal is (7.13) rather than the stronger (7.17) because it depends only on the first two moments of the input.
Kingman's bound is the most widely used performance estimate for single-server queues. It needs no distributional form, only two means and two variances. It yields the "Kingman formula" approximation used across manufacturing and service operations, and it is asymptotically exact as (Theorem 7.1). The departure variance (7.12) drives the decomposition approximations for networks of §7.3. The heavy-traffic theorem is the entry point to diffusion approximations of queues.
All results here are proved in the literature (Theorem 7.1 is stated in the book without proof). This mission produces the first machine-checked versions. As far as a search of the platform shows, none of these statements, and no stationary Lindley recursion, has been formalized. The substrate it needs is reusable for any mission on G/G/1, G/G/c or random walks: stationary laws of a recursion on distributions, moment identities for , and convergence in distribution.
The book's derivation squares (7.3) and takes expectations, using . That step is valid only if the stationary wait has a finite second moment. It is not assumed here and fails in general: with finite second moments of and the stationary wait has a finite mean, but its second moment is finite only if . So the moment identity (7.7) cannot be obtained by cancelling second moments. A truncation or limiting argument is needed, and even the finiteness of has to be proved rather than assumed. The lower bound further needs a Jensen argument for the conditional mean of one Lindley step. Theorem 7.1 needs a uniform-integrability argument across a sequence of queues.
Conventions committed to in Lean:
Measure ℝ; independence of (and for ) is the product measure;MemLp id 2), , , , ;variance) and are Lebesgue integrals. Every theorem therefore asserts, as part of its conclusion, that has a finite mean, and none assumes a finite second moment of ;cdf of the law of ;expMeasure 1.Closed forms carried by the statements: (7.4), (7.7), (7.12), (7.13), (7.14) and (7.17) exactly as printed, and the scaling of Theorem 7.1.
Stating (7.13) with , or the idle probability as free real numbers constrained by (7.7) would reduce it to algebra. Here is always the mean of a stationary law of the queue.
Not formalized: (7.5) and (7.8), which need the idle-period law and the arrival-point probability as separate objects, and the multiserver bounds of §7.1.3. Proofs of any milestone are welcome, as are reusable lemmas on stationary laws of Lindley's recursion (existence, uniqueness, and finiteness of the mean under ).
Two-stage stochastic linear programs model decisions taken before uncertainty is resolved (first stage) and corrected afterwards at a cost (second stage, the recourse). The standard solution method for problems with finitely many scenarios is the L-shaped method of Van Slyke and Wets (1969), an outer linearization in the style of Benders decomposition: a master program approximates the expected recourse function by cutting planes, one cut per iteration. Birge and Louveaux (1988) proposed the multicut variant, which approximates the recourse function of each realization separately and can add several cuts per iteration, and compared the two methods by worst-case counts of major iterations.
The paper's §5 treats the special case of simple recourse, where the second stage only penalizes shortage and surplus of each component of the first-stage output against a random target. Simple recourse arises in production planning, inventory and capacity models, and is the case in which the recourse function separates into one-dimensional pieces. There the paper derives an explicit LP (25) equivalent to the problem, a dedicated multicut algorithm for it, and the bound of iterations quoted below. This mission formalizes that section.
First-stage data are , , , and the first-stage feasible set is . A deterministic technology matrix , with rows , maps to the tender . Problem (3) of the paper is
For each row the random vector takes values with probabilities . The simple recourse cost (20) of row is the optimal value of a one-row LP,
and by separability (19) the expected recourse function is with . Write .
The multicut algorithm for simple recourse problems (p. 389) keeps a set of identified pairs , initially empty. Step 1 solves the master program (26),
with and . Step 2 adds to every pair for which the constraint (27) is violated at the master's solution , and returns to Step 1; when no pair is added the algorithm stops.
The paper states (p. 389): "The initial problem (26) involves constraints and variables. For this problem, the worst-case situation is when at each iteration, only one constraint (27) is violated in Step 2. Then, the maximal number of iterations is ." The goal asserts, for every run of the algorithm (any optimal solution of (26) may be used at each Step 1):
and, when the algorithm stops at , and for all .
The bound is linear in and , while the L-shaped method may need as many iterations as has facets, up to (milestone 4). This is the paper's clearest instance of the multicut method's worst-case advantage, and the equivalence (25) shows that simple recourse problems are LPs of size linear in , a fact used throughout the later literature on simple and integrated recourse.
The results are proved in the paper, briefly. To our knowledge none has a machine-checked proof. Formalizing them produces a checked reduction of simple recourse to an explicit LP, a checked correctness proof of a constraint-generation algorithm with an explicit iteration bound, and the piece count of a sum of one-dimensional convex piecewise linear functions.
The counting argument is short once the algorithm is pinned down; the difficulty lies in the rest. Correctness at stopping requires relating three optimization problems (3), (25) and (26) whose objectives differ by a constant and by slack variables that are only present for identified pairs, and doing so for an arbitrary optimal solution of the master. The step from (20) to (22)–(23) requires solving an LP in closed form, as an infimum that must first be shown finite. The facet count requires showing that a sum of convex functions, each with one breakpoint, is a maximum of exactly affine functions, which is not a consequence of convexity alone.
All vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, realizations are indexed by Fin J, and pairs by Fin m2 × Fin J. The second-stage value is the EReal infimum of the LP (20), not its closed form; expectations are finite sums weighted by with .
Readings pinned down, each recorded in the item statements:
A formalization in which the master step could fire without a violated, unidentified pair, or in which the algorithm's optimal solutions were fixed in advance, would make the bound either false or empty; the definitions exclude both. The goal includes optimality at stopping so that it is not only a statement about a set growing inside a finite set.
Needed infrastructure: elementary LP feasibility and optimality, finite sums in EReal, and piecewise linear convex functions on . Contributions of any of the milestones, in any order, are welcome; milestone 1 is the natural first step.
The price of anarchy measures how much a system of selfish agents loses compared with a centrally optimized one: it is the worst ratio, over all Nash equilibria, between the social cost of the equilibrium and the optimal social cost. Koutsoupias and Papadimitriou introduced it in 1999 (Worst-case equilibria, STACS 1999), and bounding it for routing and congestion games became a central topic of algorithmic game theory. Congestion games model routing in networks, load balancing on machines and any setting where agents choose sets of shared resources whose cost grows with their usage.
Christodoulou and Koutsoupias (The price of anarchy of finite congestion games, STOC 2005) determined the pure price of anarchy of finite (atomic, unweighted) congestion games with linear latencies for two social costs — the sum of the players' costs and the maximum cost of a player — and for asymmetric and symmetric games. Awerbuch, Azar and Epstein obtained the bound for the sum independently in the same proceedings (The price of routing unsplittable flow, STOC 2005). This mission is the fourth of a series that formalizes the paper: the symmetric games with the maximum social cost (Sect. 3.4). For asymmetric games the maximum social cost has price of anarchy (mission III); symmetry brings it down to a constant.
A congestion game has a finite set of players , a finite set of facilities, for each player a collection of pure strategies (each a subset of ), and for each facility a latency function . A pure strategy profile picks for every player. The load is the number of players whose strategy contains , and the cost of player is
A profile is a pure Nash equilibrium if no player can lower its cost by changing only its own strategy: for every and every , where replaces by .
The maximum social cost is and the sum social cost is . Latencies are linear when with . The game is symmetric when all players share one strategy set, . The pure price of anarchy for the maximum social cost is
For every symmetric linear congestion game with at least one player, every pure Nash equilibrium and every pure strategy profile ,
and for every there is a symmetric linear congestion game with players, a pure Nash equilibrium and a profile that minimizes the maximum social cost, with and
The second part shows that the constant of the first is tight as .
The result says that in symmetric congestion games with linear costs no player at an equilibrium is ever more than times worse off than the worst-off player under the best allocation, regardless of the number of players. This contrasts with the asymmetric case, where the ratio grows like (Theorems 5 and 6 of the paper), and it fills the symmetric–maximum entry of the paper's Table 1. Together with the sum bounds it completes the picture of pure equilibria under linear latencies that later work on smoothness and robust price of anarchy (Roughgarden, Intrinsic robustness of the price of anarchy, STOC 2009) generalized.
The results are proved in the paper, which only displays the identity-latency case and states that the arguments extend to affine latencies. No machine-checked version of any of the paper's bounds is known to exist; the mission produces a formal proof of the affine statement, a checked construction for the lower bound (the paper verifies its Nash condition only partly), and a congestion-game layer shared with the rest of the series.
The obvious attempt bounds the worst player's cost by its deviation to its own optimal strategy only, as in the proof for the sum; that gives one inequality per player and loses the factor needed to compare with . Without symmetry the factor cannot be recovered at all (Theorem 6 of the paper). For the lower bound, the difficulty is that the construction must be a Nash equilibrium against all strategies in the common set — including the other players' equilibrium strategies and the isolated strategy of the maximum-cost player — while the paper only writes out the deviation to the optimal strategies; its parameters are left as the solution of a linear equation, which must be chosen integral for every .
Players form a finite type (Fin N in the lower bound) and facilities a finite type; profiles are maps from players to Finsets of facilities, with feasibility as a separate predicate IsProfile. Latencies are real-valued functions on natural-number loads; "linear" means affine with nonnegative coefficients. MAX is the maximum over a nonempty player set. Upper bounds are stated for every Nash equilibrium and every feasible profile, never dividing by the optimum. The lower bound asserts that minimizes MAX over all profiles and that : without positivity the equality would be satisfied by a game with all costs , and without symmetry or the full common strategy set the instance would not be the paper's. The lower bound gives for the instance, which is what the paper's proof shows.
The development needs sums over facilities exchanged with sums over players (), monotonicity of affine latencies, and an explicit finite instance. The congestion-game definitions are shared with the other missions of the series and will be merged with them; Lemma 1 and Theorem 1 are also milestones of mission I. Proofs of any milestone, and alternative constructions for Theorem 8, are welcome.
When many independent users share a resource whose cost grows with use (links of a network, servers, machines), each user chooses for itself, and the outcome is a Nash equilibrium rather than a socially optimal allocation. The price of anarchy, introduced by Koutsoupias and Papadimitriou (STACS 1999), measures the cost of this decentralisation: the worst ratio between the social cost of an equilibrium and the optimal social cost. It has become a standard yardstick in algorithmic game theory, network routing and the design of distributed protocols.
Christodoulou and Koutsoupias (STOC 2005) determined the price of anarchy of finite congestion games with linear latencies, the atomic, unweighted counterpart of selfish routing. This mission formalizes the central entry of their table: pure equilibria, general (asymmetric) strategy sets, and the average social cost.
Timeline:
A congestion game has a finite set of players, a finite set of facilities, for every player a set of pure strategies (each a set of facilities), and for every facility a latency function giving the cost of to each of its users as a function of how many users it has. A pure strategy profile picks for each player. The load is the number of players with , and player pays
The profile is a pure Nash equilibrium if no player can lower its cost by switching alone: for all and all , where replaces by . The social cost is , which is times the average cost of a player. Latencies are linear: with . The game is asymmetric in the sense that each player has its own strategy set (symmetric games, where all coincide, are a special case).
The pure price of anarchy of the average social cost is
the minimum taken over pure strategy profiles. In Lean these objects are CongestionGame, load, cost, IsProfile, IsPureNash, sumCost and IsLinear in the namespace CongestionPoA.AsymSum.
The goal theorem pure_poa_sum_eq_five_halves is the conjunction of Theorems 1 and 2 of the paper:
The first part is the upper bound; the second shows that it is attained for every number of players from three on.
The value is the benchmark for atomic congestion with affine costs. It is the reference point for the later results of the paper (the symmetric case , the maximum social cost , mixed equilibria ) and for a large literature on coordination mechanisms, taxes and the price of stability, which compare their guarantees against it. The bound is also the standard example of what later became the smoothness framework, through which the same constant governs mixed and coarse correlated equilibria and hence no-regret learning outcomes.
Both theorems are proved in the paper; nothing here is open. The proofs for affine latencies, however, are only indicated: the paper displays the identity case and states that the arguments extend. The mission states the affine case and asks for complete machine-checked proofs, including the lower-bound construction, which the paper describes and declares "not hard to verify". No machine-checked proof of these results is on the platform.
The Nash conditions give one inequality per player, each mixing the equilibrium loads with the strategies of the comparison profile. Bounding the loads crudely, for instance by the number of players, gives a ratio that grows with ; the constant requires comparing the cross term with both social costs simultaneously and with the right weights. The integrality of the loads matters at that point: the natural pointwise inequality is false for real arguments, so a proof that treats loads as real numbers cannot reach .
For the lower bound, a Nash equilibrium must be verified against every unilateral deviation of every player, for all at once, in a construction with cyclic indices. The case is genuinely different (the paper states that its price of anarchy is ), so the argument has to use .
Players and facilities are finite types; a profile is a map from players to finite sets of facilities, and feasibility () is a separate predicate. Latencies are real-valued functions of the natural-number load, and "linear" means affine with nonnegative coefficients. The upper bound is stated multiplicatively, for every Nash and every feasible , which is equivalent to and avoids dividing by . The lower bound quantifies over players Fin N, , and existentially over a finite facility type, a linear game, a Nash equilibrium and an optimal feasible profile of positive social cost. The positivity rules out the trivializing witness: in the all-zero latency game every profile is a Nash equilibrium and . The Nash condition is the paper's cost form; it agrees with the payoff-form AGT.IsPureNash of agt_games for payoffs .
Trivializing formalizations are ruled out: the comparison profile must be feasible (otherwise could be by letting players use no facility), the upper bound covers all affine latencies rather than only , and the lower-bound instance must have linear latencies with nonnegative coefficients.
A complete development needs finite double counting (regrouping by facilities), monotonicity of affine latencies, and a decidable or explicit check of the lower-bound game. The congestion-game layer is reused by the other missions of this series. Proofs of individual milestones, and alternative proofs of the upper bound, are welcome.
In many statistical applications the number of unknown parameters is far larger than the number of observations : gene-expression studies with tens of samples and thousands of genes, imaging problems with fewer measurements than pixels, and nonparametric curve estimation from finitely many noisy samples. Least squares is useless in this regime, since the system is underdetermined. If the parameter is sparse (only a few of its entries are nonzero), estimation becomes possible, and the question is how accurate a computationally tractable estimator can be.
Candès and Tao (arXiv:math/0506081; Ann. Statist. 35(6), 2007, doi:10.1214/009053606000001523) introduced the Dantzig selector, an estimator computed by a linear program, and proved that its squared error is within a factor of order of the error of an oracle that knows where the nonzero entries are. The paper, with its discussion in the same issue, is one of the founding results of high-dimensional sparse regression, alongside the Lasso analysis of Bickel, Ritov and Tsybakov (arXiv:0801.1095).
Timeline. Candès and Tao (2005, arXiv:math/0502327) showed that minimization recovers a sparse vector exactly from noiseless data when the restricted isometry constants of the design satisfy . The Dantzig selector paper (first posted 2005, published 2007) carried this to Gaussian noise, with the error bound formalized here (Theorem 1.1) and an oracle inequality (Theorem 1.2). Bickel, Ritov and Tsybakov (2009) replaced the restricted isometry hypothesis by weaker restricted eigenvalue conditions and showed that the Lasso and the Dantzig selector behave alike.
Observe from the linear model
where is a deterministic design matrix with columns , each of Euclidean norm ; is an unknown deterministic parameter; and is a vector of independent random variables with . The vector is -sparse if at most of its entries are nonzero.
For let be the submatrix of the columns indexed by . The restricted isometry constant is the smallest with
for all and all coefficient vectors ; the restricted orthogonality constant (for ) is the smallest with for all disjoint with , .
Given a tuning parameter , the Dantzig selector is any solution of
Let , , -sparse, and . For every , with , with probability exceeding the program has a solution and every solution satisfies
For this is , display (1.10) of the paper. The constant is the one the paper's proof establishes (see Formalization scope).
The result. Theorem 1.1 shows that an estimator computable by linear programming reaches, up to the factor and the constant , the squared error that least squares would attain if the support of were known in advance, even when . The factor is the price of not knowing the support; the paper argues (p. 5) that, apart from this factor, (1.10) is unimprovable in general. The bound is non-asymptotic, with an explicit constant and an explicit failure probability, and it holds for every -sparse simultaneously in the sense that the good event (the noise being nearly orthogonal to every column) does not depend on . Its deterministic part, Lemma 3.1, is reused verbatim in the proof of the paper's oracle inequality (Theorem 1.2) and became a standard tool in compressed sensing.
Formalizing it. The result is proved, and to our knowledge no machine-checked proof exists. A formalization produces a checked version of the cone-and-tube argument behind most -recovery guarantees, a Lean statement of the restricted isometry machinery for noisy data, and a checked Gaussian maximal inequality usable for other high-dimensional estimators. It also settles the exact constant: the paper prints , while its proof gives in place of .
Lemma 3.1 is the main obstacle. The obvious approach bounds directly through restricted isometry, and it fails because the error is not sparse: it spreads over all coordinates, and restricted isometry controls only on vectors with at most nonzero entries. The two constraints (3.2) and (3.3) only say that is concentrated in on the coordinates of and that is small coordinatewise, and turning that into an bound on all of is where the work lies. In Lean this requires bookkeeping that is routine on paper: ordering the coordinates of off by magnitude, with ties and a possibly incomplete last group of coordinates, and working with the span of a selected set of columns. On the probabilistic side, the tail bound needs the law of (a weighted sum of independent Gaussians), a sharp Gaussian tail estimate of Mills-ratio type, and a union over events. A cruder sub-Gaussian bound would not give the stated failure probability.
Indices are Fin n and Fin p; vectors are functions into ℝ. The norms, the column and the constants , are the published definitions CandesTao_Decoding_Norms and CandesTao_Decoding_RestrictedIsometry (the smallest admissible constants, via sInf), from the formalization of Candès and Tao's Decoding by Linear Programming. The noise is a family z : Fin n → Ω → ℝ on a probability space, mutually independent (iIndepFun), each coordinate with law gaussianReal 0 σ². The constraint is coordinatewise. A Dantzig selector is any minimizer; uniqueness is not assumed. Section 3 works with ; the goal is stated for general .
Committed conventions and corrections:
A trivializing formalization is excluded: the hypothesis is on the actual least constants of , not on free parameters, and it is satisfiable (for instance by , where both constants vanish).
Needed infrastructure: sums of independent real Gaussians (Mathlib has gaussianReal and its convolution), a Mills-ratio tail bound, a sorting-based block decomposition of a Finset, and orthogonal projection onto the span of finitely many columns. The block decomposition and the tail bound are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 3.1.
Policy gradient methods learn a parameterized policy directly, by stochastic gradient ascent on a scalar performance measure , instead of deriving the policy from learned action values. They are how reinforcement learning handles continuous action spaces, stochastic optimal policies and prior knowledge built into the policy's form, and they underlie REINFORCE (Williams, 1992) and the actor–critic family. Every such method needs an estimate of . The difficulty is that depends on in two ways: through the action choices in each state, and through the distribution of states those choices produce. The second effect depends on the unknown environment dynamics.
The policy gradient theorem (Sutton, McAllester, Singh and Mansour, 2000; Marbach and Tsitsiklis, 2001) gives as an expectation over the on-policy state distribution that involves no derivative of that distribution. Chapter 13 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., 2018) states it as Eq. (13.5), proves it in a box for the episodic case (p. 325) and in a second box for the continuing case (pp. 334–335), and builds REINFORCE, REINFORCE with baseline and actor–critic methods on it. This mission formalizes that chapter's theorem and the identities around it, in the book's own model.
A finite episodic MDP has a finite set of nonterminal states, a terminal state, a finite action set , a finite reward set and dynamics : for each nonterminal and action , a probability distribution over next state and reward . The terminal state is absorbing and pays nothing. Write and for the expected reward.
A differentiable policy parameterization assigns to every and state a distribution over actions, with differentiable. Under the nonterminal states form a substochastic chain with matrix ; . Episodes terminate when for all .
There is no discounting (, p. 324). The state value is the expected total reward from , with ; the action value is the expected total reward after taking in . The episode starts in a fixed state , and the performance is (13.4). The expected number of visits to in an episode is , and the on-policy distribution is (9.3).
In the continuing case there is no terminal state, is the average reward per step (13.15), is the steady-state distribution, and , are differential values, defined from the return (13.17).
If episodes terminate under , then is differentiable at and
with . The book writes and names the constant, the average length of an episode, in words (p. 326). The goal states it.
The theorem turns into a quantity that can be sampled by following the policy: weighting states by is what visiting them under does, and the log form makes the action sum an expectation over . REINFORCE (13.8), REINFORCE with baseline (13.11) and one-step and eligibility-trace actor–critic methods all rest on it, and so does their claim that the expected update is in the direction of the performance gradient (p. 329). The baseline identity is why a learned state value can reduce variance without introducing bias.
The results are proved, in the book and in the literature. What this mission adds is a machine-checked version in the book's model: random episode lengths with , vector parameters , four-argument dynamics, and values defined from expected returns. The platform already has a proved finite-horizon policy gradient theorem (policy_gradient_finite_horizon, with a baseline and log-form companion) for a fixed horizon , a scalar parameter and an expected-reward kernel; it does not cover the book's statement. The mission also makes explicit two points the text leaves informal: that episodes terminate, and what exact constant hides behind "".
The book's proof is a formal manipulation: differentiate the Bellman equation, substitute it into itself, and "unroll" infinitely often. Two steps are not justified on the page. First, it presupposes that exists; with the value is an infinite series whose convergence depends on through termination, so differentiability of at has to be established, and termination is assumed only at . Second, "repeated unrolling" is a limit: after unrollings a remainder is left over, and it vanishes only because . Differentiating the series for term by term is not an alternative shortcut without a uniform bound on the derivatives of .
In the continuing case the corresponding obstacle is the differentiability of the steady-state distribution and of the differential values, which the book's proof uses without comment; here they are part of what is to be proved, from ergodicity at alone.
Option S, with none the single terminal state (several terminal states can be merged, all having value 0). One action type for all states. lives in EuclideanSpace ℝ (Fin d), and is Mathlib's gradient; conclusions are HasGradientAt, so differentiability is asserted, not assumed.Reusable infrastructure: the episodic value layer (substochastic chains, expected visits, termination) is needed by any undiscounted episodic RL result; the soft-max and Gaussian eligibility computations are needed by every policy-gradient algorithm. Proofs of any milestone, and general lemmas on the differentiability of values and stationary distributions of parameterized finite Markov chains, are welcome.
Two-stage stochastic linear programs with recourse are a standard model for planning under uncertainty: a first-stage decision is taken before a random outcome is observed, and a second-stage (recourse) decision corrects for it afterwards at a cost. When has finitely many realizations, the problem is a large but structured linear program, and the classical way to solve it is the L-shaped method of Van Slyke and Wets (1969), a Benders-type outer linearization of the expected recourse cost.
Birge and Louveaux (1988) proposed the multicut L-shaped algorithm: instead of one cut on the expected recourse function per iteration, it adds one cut per realization. They compared the two methods by worst-case counts of major iterations (the operations between two returns to the master problem), and showed that the multicut count grows linearly in the number of realizations, while their bound for the single-cut method grows like . The multicut idea is now part of every textbook treatment of decomposition for stochastic programming (Birge and Louveaux, Introduction to Stochastic Programming, Ch. 5) and of most production implementations of Benders decomposition.
The data are a matrix , vectors , , a fixed recourse matrix , and realizations , each with a cost , a right-hand side , a technology matrix and a probability . Row vectors are written without transposes, as in the paper. The second-stage value of realization is
the expected recourse is , and the deterministic equivalent (2) minimizes over , where and is the set of for which every second-stage problem is feasible.
The multicut algorithm keeps feasibility cuts and, for each , optimality cuts . Step 1 solves the master
ignoring when scenario has no cut. Step 2 tests feasibility of each scenario at the master solution and, at the first infeasible one, adds a feasibility cut from the simplex multiplier of a phase-one LP. Step 3 solves each second-stage problem at with simplex multiplier ; for every with (condition (14)) it adds the optimality cut . If no satisfies (14) the algorithm stops.
The cut set is the finite set of all optimality cuts that Step 3 can produce for scenario : the cuts of simplex-optimal bases of the scenario- problem at points of .
The paper states (Theorem, p. 388):
Let b be the slope number of the second stage of (2). Then, the maximum number of iterations for the multicut algorithm is 1 + K(b^{m₂} − 1) (17) while the maximum number of iterations for the L-shaped algorithm is [1 + K(b − 1)]^{m₂} (18) where K is the number of the different realizations of ξ.
The goal is (17) with the number of facets replaced by the number of distinct cuts: if for every and , then in every run of the algorithm, for every choice of optimal master solutions and optimal bases,
The bound explains why the multicut method needs few major iterations: the information sent to the master grows additively over scenarios, while the facets of are combinations of facets of the and their number can grow multiplicatively. The paper itself notes the trade-off this creates against master size ( rows instead of ), which is the basis of later work on partial aggregation of cuts.
The mission produces a formal model of the multicut algorithm as a transition system over all admissible choices, valid-cut lemmas for both cut types with dual feasibility made explicit, the correctness of the stopping rule, and the counting argument. These results are proved on paper but, to our knowledge, no machine-checked version of the multicut L-shaped algorithm or its iteration bound exists. The model is reusable for other results on Benders-type methods for stochastic programs.
The counting argument is short once the right invariants are in place; the difficulty is the invariants. A cut recorded earlier must still be satisfied by the current master solution, while the cut added for a scenario satisfying (14) is violated by it, so the new cut differs from every recorded one. This uses that every recorded cut comes from a basis whose multiplier is dual feasible: a basis that merely attains the optimal value under degeneracy can produce a cut that is not valid. The stopping rule needs strong duality at the final bases and weak duality at all earlier ones, together with extended-real bookkeeping of on points where a scenario is infeasible.
The model is the published StochasticProg_Recourse_Instance ( in EReal, when infeasible) with simplex bases and multipliers from StochasticProg_LShaped_Bases. Vectors are Fin n → ℝ, scenarios Fin K. A simplex-optimal basis is defined locally: invertible basic submatrix, nonnegative basic solution, and dual-feasible multiplier (; for the phase-one LP, and ). The algorithm is an inductive step relation on states (feasibility cuts, per-scenario cut lists, return counter); a run is any finite sequence of steps from the empty state. Master optima are attained optimal solutions, not infima.
Pinned-down readings:
The transition relation allows every choice the paper allows; a relation that fixed, say, a particular basis or a particular master solution would prove a bound for fewer runs, and one that required the cut set to be smaller than the paper's would make the bound easy. Neither is done here.
Contributions welcome: proofs of the milestones, a sorry-free proof of the goal from them, and a worked check that the definitions admit the run of Appendix A.
Competitive analysis compares an online algorithm, which must answer each request before seeing the next, with the optimal off-line solution of the same request sequence. Ben-David, Borodin, Karp, Tardos and Wigderson (Algorithmica 11, 1994) set up a general framework, request-answer games, in which paging, the -server problem and metrical task systems are all instances, and used it to compare the power of randomized algorithms against several kinds of adversaries.
One of their results (Theorem 2.1) says that if a randomized algorithm is -competitive against every adaptive off-line adversary, then some deterministic algorithm is already -competitive. The argument is a game-theoretic existence proof: it says nothing about how to compute the deterministic algorithm. Section 4 of the paper, "A Constructive Version of Theorem 2.1", answers the natural follow-up question for a large class of games: under monotonicity, locality and a finite diameter, a deterministic algorithm that loses only a factor can be assembled from a finite object.
A request-answer game has a request set , a finite answer set , and cost functions , ; is the cost of the empty play. The off-line optimum of a request sequence of length is . A deterministic online algorithm answers the -th request by a function of the requests so far; its cost on is . It is -competitive if for every .
The game is monotone if always, and local if for every only finitely many request sequences have . The discrepancy of two request-answer sequences is
and the diameter is the supremum of over all pairs.
For a real , the set consists of the request sequences all of whose proper prefixes have off-line optimum at most . Given a deterministic algorithm , the restart algorithm simulates and, as soon as the request sequence leaves , starts over as if it had received no previous requests. This cuts every request sequence into segments , each a longest prefix in of what remains.
Let be monotone and local, with finite nonempty and , , and diameter at most . Let with , , and
Then is finite; the restart algorithm depends on only through its values on ; and for every with on ,
Theorem 2.1 shows that, against adaptive off-line adversaries, randomization gives no advantage, but only as an existence statement. Theorem 4.1 turns it into a recipe: a deterministic algorithm need only be good on the finite set , which can be prepared in advance, and restarting extends it to all inputs at a loss of . The paper illustrates this with -server problems on finite graphs, where is a finite table and each step of the resulting algorithm costs one dynamic-programming evaluation of an off-line optimum.
The restart construction is of independent use: it is a general way to turn a guarantee on bounded-cost inputs into a guarantee on all inputs when the cost is nearly additive over concatenation.
To our knowledge neither the abstract request-answer game model nor this theorem has a machine-checked proof. The mission produces a formal model of request-answer games with the monotonicity, locality and diameter conditions, the restart algorithm as an explicit definition, and the full chain of inequalities of the proof.
The individual inequalities are elementary; the work lies in the bookkeeping of the construction. The algorithm is defined online, one request at a time, while the analysis is phrased through the decomposition of the whole sequence. Relating the two requires showing that the online rule produces exactly the decomposition into longest prefixes in , and that the answers produced on each segment are those of run from scratch, so that the cost of the whole play can be compared with the costs on the segments. The constants must close exactly: with the additive losses at the cuts, on both the algorithm's side and the optimum's side, must be absorbed by the factor , and they do so only for ratios .
A tempting shortcut is to conclude Theorem 4.1 from Theorem 2.1 directly: a deterministic -competitive algorithm is trivially -competitive when costs are nonnegative. This proves the sentence of the theorem without its point, and is ruled out below.
Lists, oldest first; is F.cost r a with r.length = a.length. Costs are real-valued (the paper allows ; real costs are a special case).Fintype and nonempty; in the goal the request set is a Fintype and nonempty.List R → A. Competitiveness of a deterministic algorithm against adaptive off-line adversaries is stated as competitiveness on every request sequence, which is equivalent for deterministic algorithms (p. 8).Contributions welcome: proofs of the milestones, and a connection to the other missions of this series, where the randomized model and Theorem 2.1 are formalized.
Competitive analysis measures an online algorithm, which must answer each request before seeing the next, against the best off-line answer to the whole request sequence. Randomized online algorithms are often much better than deterministic ones against an oblivious adversary, who fixes the requests in advance; the paging problem is the standard example. Against an adaptive adversary, who sees the algorithm's answers before choosing the next request, the advantage can disappear.
Ben-David, Borodin, Karp, Tardos and Wigderson (Algorithmica 11, 1994; preliminary version STOC 1990) made this precise in an abstract framework of request-answer games. Their Corollary 2.1 says: if a game has a randomized algorithm that is -competitive against adaptive on-line adversaries and one that is -competitive against oblivious adversaries, then it has a deterministic -competitive algorithm. That proof is non-constructive: it goes through a game-theoretic determinacy argument. Section 3 of the paper gives a constructive version. Most competitive analyses of randomized algorithms against adaptive adversaries are carried out with a potential function, in the style of Manasse, McGeoch and Sleator (J. Algorithms 11, 1990). The paper shows that such a potential function, together with any oblivious-competitive algorithm , determines an explicit deterministic algorithm , answer by answer. This mission formalizes that construction and its guarantee.
A request-answer game has a request set , a finite answer set and cost functions . The off-line optimum of is . A deterministic online algorithm is a sequence of maps ; on it answers , at cost . It is -competitive if for all . Throughout, and are affine maps (the paper's "linear functions").
A randomized online algorithm is a probability distribution over deterministic algorithms ; it is -competitive against any oblivious adversary if for all . The algorithm analysed by the potential function is described by its next-answer laws on , given the requests so far, the new request and its own past answers. An adaptive on-line adversary chooses each request from the algorithm's past answers and answers it itself, before the algorithm does, for at most rounds; a configuration after rounds is : requests, algorithm's answers, adversary's answers.
An augmented potential function for and (Definition 3.1) is a family with (1) ; (2) for every configuration; (3) for every configuration, every and every .
Let be an augmented potential function for and , and a -competitive algorithm against oblivious adversaries. Say that obeys the potential rule if for every and ,
Then such an exists, and every such satisfies
Both parts are part of the goal: the rule can be followed, and following it guarantees -competitiveness.
The theorem turns two separate analyses into one deterministic algorithm with an explicit description. The potential function certifies against the strongest on-line adversary; the oblivious algorithm need not be related to , and the paper remarks that may be itself. The next answer of is computable whenever the expected potential under is (Corollary 3.1, stated informally in the paper), and the paper notes that for the potential functions used in the -server literature this expectation is computable in time polynomial in the number of nodes and . Read in this light, a potential-function proof for a randomized algorithm doubles as a deterministic algorithm.
The result is proved in the paper. As far as is known, neither this theorem nor the abstract framework of request-answer games with adaptive adversaries has a machine-checked formalization. The mission produces that framework and a checked derandomization principle that applies to every request-answer game with real costs, not to one problem.
The obvious argument for the existence of averages property (3) of ; the work is in seeing which configuration to apply it to. The rule compares 's configuration against 's answers, not against an adversary playing , and the paper argues through an auxiliary on-line adversary that asks and serves it with . Making this rigorous requires interchanging the expectation over 's coins with the finite expectation over 's next answer, and checking that the needed expectations are finite.
The second difficulty is the two kinds of randomness. enters only through its next-answer laws, while must be a single distribution over deterministic algorithms: the rule evaluates and with the same coins . Replacing by a behavioural description breaks the coupling between consecutive rounds.
Requests and answers are Lean lists, oldest first, and is F.cost r a on lists of common length; values on lists of different lengths are never used. Costs are real: the paper allows , so every statement here is about the real-valued games. The answer type is finite and nonempty, so the minimum exists. Affine maps are written . The goal additionally assumes nondecreasing: the last step of the paper's proof applies to an inequality, which needs it, and the paper's examples are positive ratios. In Lemma 3.1 and milestone 5 linearity of is kept as the paper's standing convention, although with inside the expectation the argument does not use it.
is a map from (requests, own answers) to a probability mass function on (behavioural form); its play against an adaptive on-line adversary is a probability mass function on final configurations, with finite support, and its expectations are finite sums. is a probability measure on a coin space with a deterministic algorithm per coin, each answer measurable in the coins; expectations over are Bochner integrals of functions with finitely many values. stays inside expectations, as in the paper's definition of competitiveness against adaptive adversaries. Adversaries stop by returning none and have a uniform depth bound.
The goal cannot be satisfied vacuously: it states the existence of an algorithm obeying the rule alongside the guarantee for every such algorithm, and Definition 3.1 is required at every configuration, not only at reachable ones.
Not formalized: the "only if" direction of Lemma 3.1, which the paper only sketches, and Corollary 3.1, whose notion of computability the paper leaves unspecified. The definitions of request-answer games, online algorithms, adversaries and competitiveness are reusable for the other missions of this paper and for any problem-specific competitive analysis. Contributions welcome: proofs of the milestones, and a lemma relating the mixed and behavioural forms of a randomized algorithm.
A single server shared by several classes of customers is the basic model of scheduling under uncertainty: jobs of different types arrive at random, need random amounts of work, and a scheduler decides at every moment which type to serve. A classical way to optimize such a system, the achievable region approach, describes the set of all performance vectors that some scheduling policy can attain, and optimizes a linear cost over that set with linear programming. For the multiclass M/M/1 queue under preemptive, work-conserving scheduling, this set is a polyhedron described by conservation laws (Coffman and Mitrani, 1980; Gelenbe and Mitrani, 1980; Shanthikumar and Yao, 1992): it is the base of a polymatroid, its vertices are the performance vectors of the strict priority rules, and minimizing a linear cost over it is solved greedily, which recovers the rule.
That description uses one inequality for every nonempty set of classes, constraints in all. Bertsimas, Paschalidis and Tsitsiklis (working paper 1992, Annals of Applied Probability 1994) derived performance bounds for general multiclass networks from quadratic potential functions. Specialized to one station, their nonparametric method produces a different polyhedron, in variables with constraints, and they show that its projection is exactly the conservation-law polyhedron (Theorem 8.4). The paper remarks that this confirms, for this polymatroid, the belief that problems solvable in polynomial time admit polynomial-size formulations.
There are customer classes . Class has arrival rate and service rate ; its traffic intensity is , and the queue is stable: . For define
In the queue, is the steady-state mean number of class customers and their mean remaining work; is the mean work of the classes in when those classes have preemptive priority over the rest.
The performance polymatroid P1 (Theorem 8.3) is the set of with
For a permutation of , the vector is the solution of the triangular system , (Eq. (58) with ).
The extended formulation P2 (Theorem 8.4) is the set of nonnegative and satisfying
In the queue, is the steady-state mean of the number of class customers on the event that the server is busy with class . The projection of P2 is the set of for which some makes a point of P2.
Both inclusions are part of the goal. The statement fixes no constants and holds for every , every positive rate vector and every stable load.
The result. Theorem 8.4 replaces constraints by constraints in variables without changing the projected set. Any linear program over the M/M/1 performance region, including problems with side constraints where the greedy rule no longer applies, can then be solved with a polynomial-size LP. It also identifies the paper's nonparametric method as exact at a single station: the method loses nothing there, which is the baseline against which its gaps in networks are measured.
Formalizing it. The result is proved in the paper, but the reverse inclusion is argued through achievability: every point of P1 is the performance of some (randomized) policy, and every policy's performance satisfies the equations of P2. That argument rests on stochastic objects (invariant distributions under arbitrary policies, and time-0 randomizations over priority rules) that the paper does not define precisely. The paper points to a purely combinatorial derivation in Paschalidis' thesis, which we have not seen. A machine-checked proof of the polyhedral identity is therefore new content: it supplies the deterministic argument the paper delegates. The polymatroid structure of P1 (Milestone 1) is classical for supermodular set functions; this mission requires it for this specific . We know of no formalization of either result.
The inclusion only combines the equations of P2 with nonnegativity. The reverse inclusion is the hard half: for each point of P1 one must exhibit a nonnegative matrix satisfying linear equations, and the inequalities of P1 say nothing directly about the off-diagonal entries . The paper's own argument does not help here, since it produces as a steady-state expectation under a scheduling policy, an object defined through a Markov chain and given in no closed form. The sign constraints are where the inequalities of P1 are encoded, and a proof has to explain how sign conditions on auxiliary variables carry exactly the information of exponentially many inequalities in the original ones.
Classes are Fin n; rates are real functions lam mu : Fin n → ℝ with 0 < lam i, 0 < mu i and ∑ i, lam i / mu i < 1. The paper's is written x i, because n is the number of classes. A point of P2 is a pair (x, I) with I i j , including the diagonal entries. P1 is the platform definition AllocationIndices.achievablePolytope with the matrix : inequality for every , equality at , nonnegativity. The paper writes for the class set in (65) and (71); every such sum runs over all classes. The constraints (64)–(65) bound , not . is given by its closed form, , which solves (58). The standing hypothesis is presupposed by the model (Poisson arrivals at rate ); the load condition is the paper's stability condition and keeps every denominator of positive.
No statement involves a policy, a Markov chain or an expectation; the queueing meaning above is motivation only. In particular, neither "P1 is the achievable region" nor "the performance vector of each priority rule is achievable" is formalized. The goal is the full set identity: stating only , or assuming as a hypothesis of the goal, would not be Theorem 8.4.
A complete development needs: supermodularity of under the load condition; the greedy (Edmonds) description of base polytopes of supermodular functions, which is reusable well beyond this mission; and a nonnegative solution of the P2 system at each . Contributions of any of these as separate lemmas are welcome.
Unconstrained submodular maximization (USM) asks for a subset of a finite ground set maximizing a nonnegative submodular function . It contains Max-Cut, Max-DiCut and maximum facility location as special cases, and it is the basic subproblem of many constrained submodular maximization algorithms. Because is given only through a value oracle, the question is how close to the optimum a polynomial number of queries can get.
Timeline of the approximation ratio for USM in the value oracle model:
This is the third mission on the FOCS 2012 paper; the first two treat the deterministic and the randomized double greedy on sets.
Let be a finite ground set with elements and . The function is submodular if
Write and let be a maximizing set.
The multilinear extension of is the function on vectors
where the random set contains each element independently with probability . A set is identified with its characteristic vector, so agrees with on , and also denotes the unit vector at . For vectors, and are the coordinate-wise maximum and minimum.
Algorithm 4 (MultilinearUSM). Fix an arbitrary order of and start from and (the vectors and ). In iteration compute
set , , and update
with the convention that the two fractions are and when . The output is the random set . Every choice before the output is deterministic; the algorithm queries at four points per element.
For the analysis, .
For every nonnegative submodular and every order of the ground set,
The result. Theorem A.1 shows that the double greedy analysis survives a change of domain: the factor is obtained by a procedure that never flips a coin until the end, and whose state is a pair of fractional points. The ratio matches the Feige–Mirrokni–Vondrák hardness bound, so it cannot be improved in the value oracle model. Its output is a fractional point together with an independent rounding, which separates the optimization from the rounding step.
Formalizing it. The result is proved on paper; no machine-checked proof of a double greedy guarantee is known. A complete development yields reusable facts about the multilinear extension of a submodular function on a finite type: is affine in each coordinate, its coordinate increments are antitone in the other coordinates on , and restricted to characteristic vectors is . These are the standard tools of every continuous-relaxation argument for submodular maximization.
The proof on the page is short, but it relies on two facts it does not prove. First, the page justifies "by Lemma II.1", which is a statement about sets; for vectors it requires that the increment of along a coordinate decreases as the other coordinates increase, a property of the multilinear extension of a submodular function that must be derived from the sum defining . Second, inequality (6) is written out only for , and Case 2 of Lemma A.2 is omitted as analogous; the formal statements cover all cases. The main technical work is the bookkeeping of the run: that each coordinate is touched once, that and when it is touched, that , and that every state stays in , where the antitonicity applies.
Fintype with decidable equality; sets are Finset X; is real-valued, with nonnegativity a hypothesis ∀ S, 0 ≤ f S wherever the page uses it (the goal and the telescoped display). Submodularity is the published NonmonotoneSubmod.Shared.Submodular, the lattice form ; is the published NonmonotoneSubmod.Shared.OPT; is the published NonmonotoneSubmod.Shared.F, the sum above, defined for every .An online algorithm must answer each request before it sees the next one. Its performance is compared with an optimum that may choose all its answers after seeing the complete request string. Randomization can improve an online algorithm's guarantee when the request string is fixed in advance. The comparison changes when an adversary chooses later requests after seeing the algorithm's earlier answers. Ben-David, Borodin, Karp, Tardos and Wigderson studied these choices of adversary in a common request-answer model and proved a general relation between their competitive guarantees (Ben-David et al., 1994, manuscript §§2–3).
The paper distinguishes three adversaries. An oblivious adversary fixes the request string before the algorithm's random choices affect any answer. An adaptive off-line adversary chooses the next request from previous answers but serves the resulting request string optimally after the play. An adaptive on-line adversary also chooses its own answer as each request arrives. The ability to react to answers makes the latter two adversaries materially different from the oblivious one for randomized algorithms (Ben-David et al., 1994, manuscript pp. 7–9).
A request-answer game has a request set , a finite nonempty answer set , and a real cost for a request string and an answer string . The off-line optimum for is . A deterministic online algorithm returns its th answer from the first requests alone; it has no access to the rest of or to the eventual stopping time. Its cost on is .
A randomized online algorithm is a distribution over deterministic online algorithms. With coins , write for the resulting deterministic algorithm. For a fixed request string , is -competitive against oblivious adversaries when . The paper calls a transformation “linear” when it has the affine form (Ben-David et al., 1994, manuscript p. 7).
An adaptive off-line adversary has a rule from prior answer strings to either the next request or a stop signal, together with a common finite upper bound on play length. Let denote its request string and . Its competitiveness condition places the transformation inside the expectation: . An adaptive on-line adversary has the same request rule and an additional answer rule; its own cost is , and the corresponding condition uses on the right (Ben-David et al., 1994, manuscript pp. 8–9).
The first target is Theorem 2.1: if some randomized algorithm is -competitive against every adaptive off-line adversary, a deterministic algorithm has that same guarantee on every request string:
Theorem 2.2 takes an guarantee for against adaptive on-line adversaries and a guarantee for another randomized algorithm against oblivious adversaries. It concludes that has the composed guarantee against adaptive off-line adversaries:
The mission goal is Corollary 2.1, the deterministic consequence of these two results:
The milestones follow the paper's two theorems and the stated claims in their proofs, including the finite-horizon winning-position formulation and the adversary that simulates a fixed online algorithm (Ben-David et al., 1994, manuscript pp. 9–13).
The corollary turns the existence of two randomized guarantees under different information rules into the existence of a deterministic online strategy with an explicit composed cost transformation. It is an existence result: it does not say that the deterministic strategy can be computed efficiently from the randomized algorithms. The paper itself notes that such a construction is unavailable in full generality and then examines settings where constructive versions are possible (Ben-David et al., 1994, manuscript p. 13).
The mathematical results were proved in the 1994 paper; this mission asks for machine-checked Lean proofs of the abstract model, the intermediate claims, and Corollary 2.1. The local draft currently contains compiled statements with proof placeholders, so it does not yet provide checked proofs. A completed development would make the adversary distinctions and the exact placement of expectations available for reuse in later online-algorithm formalizations.
The apparent shortcut is to treat an adaptive request sequence as fixed and apply a guarantee against oblivious adversaries directly. That loses the dependence of later requests on the algorithm's earlier answers. For Theorem 2.1, a winning request strategy must have one finite horizon that works for every answer path; separate finite horizons for each branch do not suffice when the answer set is infinite. For Theorem 2.2, the simulated adversary must make its own answers before the algorithm answers the current request, while still matching a fixed online benchmark along every resulting play. The expectation inequalities must remain valid when the request string itself depends on the algorithm's coins (Ben-David et al., 1994, manuscript pp. 9–11).
Lean represents requests and answers as oldest-first lists. List index zero is request one in the paper. The general game is a separate definition; the algorithm, adversary, and competitiveness definitions build on it. An off-line adversary's rule returns Option R, where none is the stop signal, and has a uniform finite depth bound. A randomized algorithm consists of a coin probability space and a deterministic prefix algorithm for each coin; its answer events are measurable. Finiteness of and bounded play depth make the cost of each fixed adversarial play take finitely many values, so its real expectation is an ordinary integrable expectation.
The formal game uses real-valued costs, a deliberate restriction of the paper's costs. The answer set is finite and nonempty, while the request set may be infinite. The transformations and are affine. Theorem 2.2 and the goal assume is monotone: the paper applies to an inequality in its proof, and its competitive-ratio examples have positive slope. Theorem 2.1 does not need this added assumption. The two randomized algorithms may have different coin spaces, each an arbitrary Lean type at the declaration's universe level. The off-line and on-line adaptive comparisons retain inside the expectation.
The target ranges over every equal-length request and answer play generated by these rules, including an adversary that stops without a request. It does not allow the deterministic algorithm to see future requests or choose a different policy for each adversary. Reusable contributions include the game interface, bounded adaptive plays, measurable randomized algorithms, and finite-horizon winning positions. The statements of all three principal results, their intervening claims, and proofs of those statements are within scope.
An on-line algorithm must answer each request as it arrives, without knowing the requests to come; paging, caching, the -server problem and metrical task systems are standard examples. Its quality is measured by competitive analysis: its cost is compared with the cost of an optimal off-line solution that knows the whole request sequence. For randomized on-line algorithms the comparison depends on how much the adversary producing the requests is allowed to see. Ben-David, Borodin, Karp, Tardos and Wigderson (Algorithmica 11, 1994; conference version STOC 1990) introduced the three standard adversaries — oblivious, adaptive on-line and adaptive off-line — and related the competitive ratios achievable against each.
Their Theorem 2.2 (manuscript p. 10) shows that if a randomized algorithm is -competitive against adaptive on-line adversaries and some randomized algorithm is -competitive against oblivious adversaries, then the first algorithm is -competitive against adaptive off-line adversaries. This mission formalizes the paper's claim (manuscript p. 11) that this product bound cannot be improved in general, together with the explicit construction on pp. 12–13 that proves it.
A request-answer game consists of a request set , a finite answer set , and cost functions . For a request sequence , the off-line optimum is . A deterministic on-line algorithm answers the -th request with ; a randomized one is a probability distribution over deterministic algorithms , being the coin tosses.
An adaptive off-line adversary chooses each request from the answers given so far, stops after at most requests, and pays the off-line optimum of the requests it made; the algorithm pays . An adaptive on-line adversary must in addition answer each request itself, before the algorithm does, with , and pays . An oblivious adversary fixes in advance and pays . A randomized is -competitive against oblivious adversaries if for all , and against adaptive on-line adversaries if for all .
The construction uses the mates game: is a set of elements split into pairs of mates, and for the cost depends only on the first answer and the second request : it is if , if is the mate of , and otherwise. The algorithm draws uniformly at random. The parameters solve
For (or ) and every , there are a game and a randomized algorithm such that
and for every randomized algorithm some adaptive off-line adversary achieves
The result. Together with Theorem 2.2, the claim pins down exactly how much the adaptive off-line adversary can gain over the other two: the product is an upper bound for every game and is approached by a single game for every admissible pair . It shows that no general argument relating the three adversary models can give a bound better than the product, so any improvement for a specific problem (paging, -server) must use the structure of that problem. The paging example cited on p. 11 (RANDOM against the three adversaries) gives one instance of tightness; the mates game gives tightness for every admissible pair.
Formalizing it. The result is proved in the paper, in about one page, with two steps left to the reader ("by inspection of the equations", "a simple case analysis"). No machine-checked proof of this or of any statement about adaptive adversaries is known to us. The formalization makes the model of §2 precise (sequences, stopping, the order in which adversary and algorithm commit, expectations over coins), checks the asymptotics of the parameters, and verifies the case analysis, which on inspection needs an inequality the page does not state. Two printed formulas on p. 12 contain typos; the formal statements carry the correct values.
The construction is explicit, but each competitiveness claim quantifies over all adversaries, which may adapt their requests to the algorithm's random answers, stop at any time, and (for the on-line adversary) commit to their own answers in advance. The algebra of -competitiveness is tight: the adversary's best expected advantage is exactly zero, so every case of its best reply must be checked with no slack. The page's condition does not suffice for this: when is neither the adversary's first answer nor its mate, the reply "mate of " beats the reply "the adversary's own answer" only when , which holds for the solved parameters but is not implied by . At the solved parameter is below for every , and the oblivious bound fails.
All declarations live in OnlineRandomization.Tightness. The conventions:
cost r a is on lists of equal length .none for "stop" and carry a depth bound ; an on-line adversary's answer depends only on .Type.Fin t × Bool, with mate . The paper leaves the costs of plays with fewer than two requests undefined; the formalization sets and (with the algorithm would not be -competitive).The positivity requirement in the goal is essential: without it the adversary that asks nothing satisfies for every , and the third clause would hold vacuously.
A complete development needs: finite expectations over a uniform coin, the evaluation of the play of an adversary against a constant algorithm, and limit and eventual-inequality arguments for rational functions of . The model of §2 is shared with the other missions of this series and is reusable for any request-answer formulation of an on-line problem. Proofs of individual milestones are welcome.
Stochastic gradient methods minimize a function when only noisy estimates of its gradient are available: each step moves along a descent direction corrupted by random noise. They are the standard training algorithm for neural networks and the basic tool of stochastic approximation, and the question every user faces is what can be guaranteed when is nonconvex, possibly unbounded below, and the noise is allowed to grow with the gradient.
D. P. Bertsekas and J. N. Tsitsiklis, Gradient Convergence in Gradient Methods with Errors, SIAM J. Optim. 10(3):627–642, 2000 (DOI), answer this under minimal assumptions. Noise with variance growing in had been handled for related methods (Poljak and Tsypkin 1973), but typically together with a lower bound on , under which is approximately a supermartingale and the supermartingale convergence theorem applies (see the monographs of Kushner and Clark 1978; Benveniste, Métivier and Priouret 1990; Kushner and Yin 1996). Section 4 of the paper (p. 635) removes the lower bound: it proves that, with probability 1, either or converges and , without assuming bounded iterates. Section 5 shows that the randomized incremental gradient method for a finite-sum objective is a special case. This mission formalizes Section 4 and the Section 5 application. A companion mission covers the deterministic counterpart (Proposition 1 of the same paper).
Let be continuously differentiable with a Lipschitz gradient: there is with
Let be a probability space and an increasing sequence of -fields (a filtration; is the history of the algorithm just before the noise is drawn). The stochastic gradient method generates random vectors by
where is a deterministic stepsize, is a descent direction and is a noise term. The assumptions of Proposition 3 are:
The noise variance in (c) may grow quadratically with and is therefore unbounded in general. A point is stationary if .
Under (2.1) and (a)–(d), with probability 1,
and every limit point of is a stationary point of . The dichotomy is per sample path: different paths may take different branches.
For with Lipschitz gradients satisfying (5.2), the randomized incremental gradient method , with independent uniform indices , satisfies the conclusion of Proposition 3.
Proposition 3 is a convergence guarantee for stochastic gradient descent on smooth nonconvex objectives that needs neither a lower bound on , nor bounded iterates, nor bounded noise variance. It contains, as special cases, stochastic gradient descent with unbiased gradient estimates whose variance grows with the gradient, the randomized incremental (single-sample) gradient method for finite sums of Section 5, and scaled or approximate gradient directions through condition (4.1). Its conclusion is the strongest one available at this generality: if stays bounded below along a path, then the gradient vanishes along that path and every limit point is stationary.
The result is proved in the paper; to our knowledge it has not been machine-checked. Its formalization requires a working theory of generalized conditional expectations of non-integrable noise, square-integrable martingales in and pathwise arguments over random interval partitions, which is reusable for other stochastic approximation results (Robbins–Monro type schemes, TD-learning, stochastic subgradient methods).
The natural first idea is to view as a supermartingale up to summable errors and apply the supermartingale convergence theorem (Robbins–Siegmund). This fails here: the theorem needs bounded below, and is not assumed bounded below; in addition the noise term in (4.4) has conditional mean of order , which is not summable when the gradient is unbounded. Any argument must therefore extract a decrease of that dominates noise of the same order as the gradient itself, without a lower bound to anchor a supermartingale, and must do so along every sample path while the hypotheses are only conditional-expectation statements about non-integrable noise.
EuclideanSpace ℝ (Fin n), is Mathlib's gradient f, is ContDiff ℝ 1, and the Lipschitz constant is L : ℝ≥0 with LipschitzWith L (gradient f) (the standing assumption (2.1), equivalent to the page's form).Measure Ω with IsProbabilityMeasure, the -fields are a Mathlib Filtration ℕ, and measurability in (a) is StronglyMeasurable[ℱ t]. The recursion and (4.1) hold on every sample path. Stepsizes are deterministic.condExp is for non-integrable functions, so stating (4.2)–(4.3) with it would make them hold vacuously for any non-integrable noise; that encoding is ruled out. Instead (4.3) says that for every -measurable set , (in ), and (4.2) says that for every -measurable on which is integrable. These are exactly the generalized conditional-expectation statements of the page.condExp is used there, with integrability of stated explicitly; the page's hypothesis implies it. Lemma 2 is stated over any finite-dimensional real inner-product space, since the paper applies it to real and to vector-valued sequences.Summable. Convergent random series (Lemma 2) are convergence of partial sums, not Summable, which would mean unconditional convergence. "" is "for every , eventually ". Limit points are MapClusterPt.Contributions welcome: a proof of Lemma 2 from Mathlib's martingale convergence theorems (Submartingale.exists_ae_tendsto_of_bdd), a proof of (4.4) from the descent lemma, a general bridge between the set-integral encoding of conditional expectations and Mathlib's condExp on localizing sets, and the interval construction behind Lemmas 3–6.
Temporal-difference (TD) learning estimates the value of a policy by moving a current estimate toward a target built from observed rewards and from the estimate itself. Chapter 7 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) interpolates between the two extreme targets of the preceding chapters: the one-step TD target, which uses one reward and then bootstraps, and the Monte Carlo target, which uses every reward until the end of the episode. The intermediate target, the -step return, uses rewards and then bootstraps from the current estimate. The family underlies -step TD, -step Sarsa, the off-policy per-decision methods and the tree-backup algorithm, and it is the introduction to eligibility traces (Chapter 12).
The book justifies the whole family with one inequality, the error reduction property (7.3), p. 144: the expected -step return is closer to the true value than the estimate it bootstraps from, by a factor in the worst state. It is the reason given for calling -step TD methods "sound". The same chapter states, mostly as exercises without solutions, a series of exact identities that rewrite each kind of -step return as a sum of one-step TD errors.
A finite Markov decision process has finite state and action sets , , a finite reward set , and dynamics , the probability of next state and reward after action in state (Eqs. (3.2)–(3.3)). A policy is a probability distribution over actions for each state. Following from produces a random trajectory For a discount factor the state-value function is the expected discounted return (3.12),
Given any function (an estimate of ), the -step return (7.1) is
In an episode that terminates at time it is replaced by the complete return when . The TD error (6.5) is . Off-policy variants use a behavior policy that generates the data, the per-decision ratio , and the return with control variate (7.13), , . The tree-backup return (7.15)–(7.16) uses action values and the expected approximate value (7.8).
For a finite MDP, a policy , , any and every ,
The result. The error reduction property makes the expected -step target a -contraction toward in the sup norm, uniformly over the estimate it starts from. It is the one-line reason the book offers for the soundness of every -step TD method, and the same contraction is what the -return of Chapter 12 averages over . The TD-error identities are the algebra behind implementations that accumulate TD errors instead of storing returns, and behind the forward/backward-view equivalences of Chapter 12. Exercise 7.6 is the unbiasedness of the control-variate return, which is what allows (7.13) to replace plain importance weighting without changing the expected update.
Formalizing it. All results are elementary and well known, but the book gives no proofs: (7.3) is asserted, and the identities are exercises without published solutions. None is formalized on Prove2Me. The mission produces machine-checked versions with every hypothesis explicit (discounting, the fixed estimate, terminal values, coverage), and a trajectory-level expectation for finite MDPs that other chapters of the series can reuse.
The obvious proof of (7.3) is a matrix computation: , and a stochastic matrix does not increase the sup norm. The difficulty lies in the step before it. The left side is an expectation over trajectories, and is an infinite discounted series; neither is a matrix power by definition. Connecting them requires a Chapman–Kolmogorov identity for the finite-trajectory distribution induced by and , the splitting of at time , and summability of the discounted series. Defining the expected -step return as the matrix expression would reduce the goal to the last line and remove its content; that shortcut is ruled out below.
The TD-error identities are telescoping sums, but each has its own boundary: termination inside the steps, the convention that terminal states have value zero, the index at in (7.6), the special case of the tree backup, and ratios with vanishing denominators in (7.13).
Needed infrastructure: finite sums over function types, Chapman–Kolmogorov for the segment distribution, summability of . The trajectory layer is reusable for the importance-sampling and eligibility-trace chapters. Alternative proofs of the goal, and proofs of the undiscounted episodic version as a separate theorem, are welcome.