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?
An online matching algorithm must commit to each assignment when a request arrives, before it sees later requests. This limitation arises whenever waiting for the full instance is impossible: an available resource can be assigned to a current request or saved for an unknown future request. The quality of the assignment is measured by how many requests can be matched. The central question is how much the lack of future information costs, even when an algorithm uses randomness. Karp, U. Vazirani, and V. Vazirani studied this question for bipartite graphs and proved an asymptotic ceiling of for the expected fraction matched by any randomized online rule on graphs with a perfect matching (Karp, Vazirani, and Vazirani, 1990).
The paper also analyzes RANKING and gives a matching asymptotic guarantee from below. This mission concerns the separate upper-bound result: the existence of hard instances for every algorithm. The upper bound matters independently of any particular proposed rule. It says that improving an algorithm's decisions cannot remove the worst-case loss due to decisions made before all columns are revealed. Its quantifiers make the adversarial model precise: the graph is selected with knowledge of the algorithm, before that algorithm's random choices are made.
There are boys, represented by rows, and girls, represented by columns. A bipartite graph records which boy and girl pairs may be matched. The graph is assumed to contain a perfect matching: some bijection between the two sides uses only edges of . This assumption supplies an offline benchmark of matches. Without it, a graph with no edges would make every upper bound on matching size empty of content.
Girls arrive one at a time. On arrival, the algorithm learns the edges incident to that girl, chooses an as-yet-unmatched adjacent boy, or declines to match her. A choice cannot later be changed. The paper labels columns so that they arrive in the order . A deterministic algorithm can base its action on the neighborhoods revealed so far. A randomized algorithm can additionally use internal random choices. Its performance is the minimum, over a graph with a perfect matching and a preselected arrival order, of its expected number of matches; the expectation is over its own randomness (Karp, Vazirani, and Vazirani, 1990, p. 352).
The paper's hard family begins with the complete upper-triangular graph , where row is adjacent to column exactly when . Its columns arrive from largest to smallest. Relabeling the rows by a permutation gives an instance that still contains a perfect matching. The algorithm RANDOM takes an eligible boy uniformly whenever at least one is available. Write for RANDOM's expected number of matches on , beginning with no matched rows (Karp, Vazirani, and Vazirani, 1990, p. 357).
For every , there is one threshold such that, for every and every randomized online algorithm on rows and columns, a graph with a perfect matching satisfies
The threshold is uniform over algorithms. The graph may depend on . This is the quantified upper-bound reading of Theorem 2's (Karp, Vazirani, and Vazirani, 1990, Theorem 2).
Lemma 13 identifies the average size produced by any deterministic greedy algorithm on a uniformly permuted with RANDOM's expected size on . Lemma 14 bounds the worst-case performance of every randomized algorithm, including non-greedy algorithms, by that value. Lemma 16 identifies the value itself by the two-sided limit
Together these statements give the finite-instance comparison and the asymptotic value named in the goal (Karp, Vazirani, and Vazirani, 1990, Lemmas 13, 14, 16).
Theorem 2 limits what any randomized online matching rule can guarantee under the paper's oblivious-adversary performance measure. Since the hard graph always admits a perfect matching, the gap from is caused by the order of information and the required irrevocable decisions. The statement applies to the entire algorithm class, rather than comparing two selected procedures. It therefore provides the ceiling against which the paper's lower guarantee for RANKING is measured.
Formalizing the result requires a reusable description of finite online algorithms, their visible histories, and expected matching size. It also requires a definition of uniform random choice from currently eligible rows with an explicit empty-choice case. The 1990 result is proved in the paper; the statements in this mission are targets for machine-checked proofs, not claims of an existing formal proof. The model can support later statements about other matching rules and hard-input distributions without changing the meaning of an online decision.
For a fixed graph, an algorithm can be designed around the graph's particular perfect matching, so one hard graph cannot simply be announced in advance for all deterministic algorithms. The theorem instead has to bound each randomized algorithm against a graph selected for that algorithm. Even then, checking the triangular graph against one rule does not establish a universal bound: different rules can respond differently to the same revealed neighborhoods. The crucial mathematical obstacle is a comparison across all such rules while preserving the restriction that future columns remain unseen. A further asymptotic step is needed to determine RANDOM's value on the triangular family, including both sides of the claim in Lemma 16.
Both sides are Fin n. An edge set is a subset of row-column pairs. The published perfect-matching predicate is reused: it asks for a bijection whose every selected pair is an edge. The paper's one-based column order is represented by zero-based order ; arrival number zero is the largest column. A deterministic rule receives only the neighborhoods of columns that have arrived, including the current column. A randomized rule is a probability mass function on the finite set of deterministic rules, allowing arbitrary correlations among its choices. The expected size is a finite sum over that mass function.
RANDOM is represented by the conditional-expectation recursion for uniform choice among eligible rows. If none is eligible, the column remains unmatched and there is no division by zero. For , the matching and RANDOM value are zero; the main theorem is eventual in and Lemma 16's value at zero does not affect the limit. Lemma 16 uses a two-sided limit. The paper's in Theorem 2 is stated as with before the algorithm, so the error is uniform across algorithms. A hard graph must contain a perfect matching; dropping this condition would let the empty graph satisfy the inequality trivially.
Useful contributions include finite probabilistic averaging, the greedy comparison, analysis of the recursive RANDOM value, and a proof joining Lemmas 14 and 16 into the uniform goal. The history and matching-run definitions are reusable for other finite online bipartite matching statements. The two numbered claims inside the paper's proof of Lemma 13 and its later remarks are outside the mission's curated milestone list.
A newsvendor retailer who may order twice faces a tradeoff. Ordering late lets the retailer use a better demand forecast. Ordering early lets the supplier produce more cheaply, with longer procurement lead times and no overtime labor. Fisher and Raman (1996) document such forecast improvements between ordering epochs in fashion apparel. A decentralized supply chain must balance cheap early production against well-informed late production, and it is not obvious that a simple contract can induce both firms to strike the balance an integrated firm would choose.
This mission formalizes §6.6 of G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003), read in the author's January 2003 draft. The section builds on Donohue (2000), who studied the same two-mode production problem under forced compliance. The chapter's model lets the supplier operate under voluntary compliance: she may deliver less than the retailer orders, and she may produce more in period 1 than was ordered. The question is whether a buy back contract with one wholesale price per ordering epoch still coordinates the supply chain.
A demand signal with density and distribution function is observed once before the selling season. Given , demand has distribution function , continuous and strictly increasing on . Demand is stochastically increasing in the signal: for . Expected sales are . Period 1 is before the signal and period 2 is after it. The retailer's total order is after period 1 and after period 2. The supplier's unit production cost is in period , with , where is the retail price. Salvage values and goodwill costs are zero.
The supply chain's period-2 objective is
and maximizes it over . The supply chain's expected profit is .
Under the buy back contract the retailer pays per unit ordered in period , and the supplier refunds per unsold unit. The retailer's period-2 profit is , and his period-1 profit is . The supplier's period-2 profit and her period-1 profit , as functions of the stock she holds, are given in the mission's Profits definition.
For with
the identities
hold, so the supply chain's optima in both periods are the retailer's optima (with equivalence for ). In addition,
The result shows that the buy back contract, which coordinates the single-period newsvendor, extends to a setting with a forecast update and two production modes, even when the supplier is free to under-deliver or to stockpile. Profit can be divided arbitrarily through . Coordination also forces the supplier's margin on expensive late production below her margin on cheap early production, which contradicts the intuition that the better-informed late order should command a premium. Milestone 7 rules out stranded inventory: under the coordinating terms the supplier never stocks more than the retailer ordered in period 1.
These results are established on paper in Cachon's chapter. No machine-checked version is known. The identities are algebraic. The supplier's production result needs differentiation of an expectation over the signal across the moving threshold .
The retailer's identities reduce to algebra once the contract terms are substituted, and the margin comparison is one line. The substantive steps are the derivative formulas (27) and . The obvious move, differentiating inside the expectation term by term, fails because the period-2 optimum has a kink at . The integrand switches between two regimes, and the switch point moves with . The supplier's period-1 profit is not differentiable at ; only its right derivative is negative at . Turning the page's derivative statements into the global claim that is her unique optimum needs a monotonicity argument on both sides of .
The conditional law is a measurable family of probability measures on supported on , each with a finite mean, a continuous distribution function, and a distribution function strictly increasing on . The signal has a measurable density with , and demand has a finite unconditional mean. These standing assumptions follow the chapter's p. 7 newsvendor model, together with the measurability needed for expectations over the signal. makes the critical ratio lie in . Expected sales reuse the platform definition SupplyChainTheory.expSales (from SupplyChainTheory_contracts).
The optimum is a hypothesis-carried selection maximizing over . It is never an arbitrary function: a formalization that let be unconstrained would make a statement about meaningless orders. The thresholds enter as solutions of (26) whose existence is assumed where the page assumes it. Optimal order quantities are taken over and . Derivatives are stated with HasDerivAt (or HasDerivWithinAt for the right derivative at a kink).
Three corrections of the print are disclosed in the item notes:
Contributions are welcome on all milestones. A lemma that differentiates with a density-driven threshold would be reusable beyond this mission.
The integer linear programming feasibility problem asks, for an integer matrix and , whether some satisfies . It is NP-complete, so no algorithm polynomial in the length of the data is expected. H. W. Lenstra, Jr. (Math. Oper. Res. 8 (1983) 538–548) showed that the picture changes when the number of variables is fixed: the problem is then solvable in polynomial time. The proof is a short argument from the geometry of numbers, and it became the starting point of lattice methods in integer programming, including Kannan's improved algorithm and the later flatness-based branching schemes.
Lenstra's introduction (p. 538) describes the idea as transforming the problem into an equivalent one in which "either the existence of a vector satisfying is obvious; or it is known that the last coordinate of any such belongs to an interval whose length is bounded by a constant only depending on ." This mission formalizes the geometric statement behind that dichotomy, §1 of the paper.
Timeline. For , Hirschberg and Wong and Kannan gave polynomial algorithms in special cases, and Scarf treated the case completely; the case of general fixed was conjectured by Hirschberg–Wong and Scarf (as recounted on p. 538). Lenstra's paper (received 1981, published 1983) settled the conjecture. Its lattice reduction step uses the algorithm of Lenstra, Lenstra and Lovász (1982). Kannan (1987) later reduced the dependence on to .
Work in with the Euclidean length , and write for the closed ball with centre and radius .
A lattice is for a basis of . Its determinant (the as columns) is the volume of the parallelepiped and does not depend on the basis. Hadamard's inequality (6) says . A basis is reduced in Lenstra's sense if, for a constant depending only on ,
Singling out , let be the hyperplane spanned by the other vectors, the lattice inside it, and the distance of to . Then : the lattice lies on a family of parallel hyperplanes at successive distance .
In the paper, is bounded with positive volume, and a linear map makes it "round":
with depending only on . Then if and only if for , a lattice with basis .
Let be a basis with (7), numbered so that , and let satisfy (3) and (4). Then
where is the number of hyperplanes , , that meet (finiteness included).
The goal leaves and free, so it remains valid for any reduction algorithm and any rounding procedure; the companion mission (Integer Programming with a Fixed Number of Variables 2) supplies , and the LLL algorithm supplies .
The result. The goal is the branching step of Lenstra's algorithm. It says that a lattice-point-free convex body that is well rounded is "flat" in the lattice direction dual to : only boundedly many lattice hyperplanes meet it. The search for a lattice point in dimension therefore reduces to fewer than searches in dimension , which with fixed gives polynomial running time. Sharper forms of the same dichotomy, such as Kannan's bounds, are the basis of later lattice-based integer programming algorithms.
Formalizing it. The results are classical and proved on paper; to our knowledge none of the statements of §1 is machine-checked. Hadamard's inequality (6) is in Mathlib (Orientation.abs_volumeForm_apply_le). The published platform theorem KannanLattice.Core.exists_lattice_point_near_projection (Kannan 1987, Proposition 4.2) proves a stronger form of (8) and (10), with Gram–Schmidt lengths in place of ; for , (10) is the published QFS.exists_lattice_mem_closedBall. What remains is the "base times height" identity (11) relating a full-rank determinant to the distance of a vector from a hyperplane, the spacing bound (12), the count of hyperplanes meeting a ball, and their assembly. This is one of the two geometric ingredients of Lenstra's polynomial algorithm; the algorithm itself and its running time are not formalized.
The argument is short on paper, and each step is "clear" there. The work lies in connecting three descriptions of the same geometry that Mathlib keeps apart: the determinant of a coordinate matrix (), the metric distance of a point to a subspace (), and the -dimensional volume of . Identity (11) needs exactly this bridge, and (12) needs Hadamard's inequality for the lower-dimensional lattice inside a hyperplane of , not for a full-rank matrix. Bounding the number of hyperplanes meeting a ball needs the normal direction of and the fact that the hyperplanes are apart along it. A tempting shortcut is to define as the length of the last Gram–Schmidt vector and as the product of Gram–Schmidt lengths: that turns (11) into a tautology and is ruled out below.
EuclideanSpace ℝ (Fin n), so norms are Euclidean and balls round; is Metric.closedBall p z with as a hypothesis where the paper writes a ball.b : Fin (k+1) → ℝⁿ, = b (Fin.last k) and = b ∘ Fin.castSucc. "Basis for " is linear independence of the vectors over , and is the published KannanLattice.Core.lattice b, the -span.latDet). is Metric.infDist from to the span . , for which the paper writes no formula, is the published KannanLattice.Core.latticeDet (the product of Gram–Schmidt lengths of , the -volume of their parallelepiped).hitIndices b p R; is its cardinality, its finiteness is part of every conclusion (the cardinality of an infinite set is in Lean), and is computed in .Welcome contributions: the bridge between Matrix.det of a basis and products of Gram–Schmidt lengths (reusable for any lattice development), Hadamard's inequality for a family of fewer than vectors, and the count of lattice hyperplanes meeting a ball.
A retailer can keep too little inventory even when its own stocking decision is optimal. In the single-location model of Cachon, Supply Chain Coordination with Contracts (2003), the supplier suffers a cost when the retailer has backorders, but the retailer does not bear that part of the cost. The supplier and retailer therefore prefer different base-stock levels. Section 6.7 asks whether payments tied to expected inventory and backorders can make the retailer choose the level that minimizes their combined cost. The result also describes how the contract divides that cost between the firms.
The model concerns a continuing operation with repeated replenishment opportunities and backordered demand. A base-stock policy keeps the retailer's inventory position at a chosen level by replacing units as demand occurs. Cachon reduces the cost calculation for such a policy to the distribution of demand over one replenishment lead time. That reduction allows the coordination question to be stated with one real stock-level decision rather than a full inventory trajectory. The chapter presents this model as a building block for its two-location system in §6.8 Cachon (2003).
Let denote lead-time demand, the amount demanded while the retailer waits for replenishment. It is nonnegative and has a finite mean , distribution function , and density . At inventory level , expected inventory is and expected backorders are , where . The section assumes and a strictly increasing differentiable on nonnegative levels. These assumptions place the optimum above zero.
The retailer pays holding cost and its own backorder cost . The supplier pays a further backorder cost . All three cost rates are positive. Thus and are the firms' costs, while is the channel cost. Write . Because demand is backordered rather than lost, the section treats the sales rate as constant across the stock decisions and compares costs alone Cachon (2003), §6.7.1.
The proposed contract pays the retailer from the supplier, where and are transfer rates. A positive rate is a subsidy; a negative rate charges the retailer. For a parameter , the contract sets and . The retailer's contracted cost is its original cost minus this transfer; the supplier's contracted cost is its original cost plus it. The parameter describes a family of printed contract rates and is not itself a payment term Cachon (2003), p. 74.
The milestones establish the two expectation identities, the channel's cost formula and strict convexity, the channel's critical ratio, the retailer's lower uncontracted stock level, and the retailer's cost after the printed transfer. In the notation above, the channel optimum is unique and satisfies
the uncontracted retailer has its own unique optimum with . Three further statements of §6.7.1 complete the section: the signs of the transfer rates over the family (, with exactly for , and ); the decomposition
and the equivalence with the newsvendor model: with lead-time demand as newsvendor demand, retail price and wholesale price , the newsvendor retailer's profit , with expected sales , equals . The mission goal is the coordinating identity of Eq. (33), together with the unique optimality it implies:
Consequently, the retailer's contracted cost has the same unique minimizer as the channel cost. At each stock level the retailer's contracted cost is strictly increasing in , which is the page's statement that the retailer's share of the cost increases with . The result does not prescribe one fixed allocation of cost: each in the stated interval gives a contract with the same coordinated stock level and a different retailer share Cachon (2003), Eq. (33), p. 74.
The theorem identifies an explicit transfer that corrects an incentive gap created by the supplier's backorder cost. Without it, the retailer sets stock according to , while the channel's stock decision uses . Under the contract, the retailer bears the fraction of total cost at every stock level, so its decision agrees with the integrated channel's decision. This conclusion connects a decentralized cost objective to the base-stock target used in the next section's two-location analysis Cachon (2003), §§6.7–6.8.
The chapter proves these claims informally; this mission asks for machine-checked Lean proofs of the expectation identities, convexity and optimality claims, and the contract identity. Its reusable output is the precise treatment of expected positive-part inventory and backorders under a demand law with finite mean. The local definitions may also support later formalizations of inventory contracts. Expected sales in the newsvendor comparison is the published SupplyChainTheory.expSales (definition SupplyChainTheory_contracts), referenced rather than redefined. The existing proved SupplyChainTheory.chain_optimal_fractile concerns a single-period newsvendor profit objective; its critical ratio is related mathematically but belongs to a different model and is not substituted for Eq. (31).
The algebra of the transfer rates is short, but the unique-optimum claim depends on more than algebra. It requires expected inventory and backorders to match the distribution formulas, the cost to have the required curvature at nonnegative levels, and the optimum to occur at a positive level. A formal statement that defines the retailer's contracted cost directly as would erase the coordinating claim. The negative-stock region also matters: since demand is nonnegative, expected inventory vanishes there and cost is affine rather than strictly convex. The formulation must keep strict convexity on the range where it holds while still identifying the unique optimum among all real stock levels.
Lean represents by a probability measure on supported on , with an explicit integrable first moment. The density is a measurable nonnegative function whose induced measure is the demand law; the cdf is continuous, strictly increasing on , equals zero at zero, and has that density as its derivative at positive levels. These are the section's distribution assumptions. The positive rates are fields of one model, and are defined by expectations. This rules out accidental zero values from nonintegrable real integrals. The cost functions are constructed from the expected inventory and backorders; the transfer is constructed from the two printed rates. The identities in Eqs. (28)–(33) are theorem targets, not definitions.
Stock levels are real, including negative levels, because the section does not explicitly restrict the decision set. The formal result states strict convexity on nonnegative levels and uniqueness of the cost minimizers over all real levels. The page's sentence that for all fails at , where ; the formal statement asserts with strict positivity exactly for . The contract range is exactly ; would make every retailer stock level cost-equivalent. The transfer sign is positive from supplier to retailer, as on p. 73. Risk neutrality and full information are the chapter's standing conventions. The continuous-review state process, supplier capacity, and proof that a base-stock policy attains the displayed long-run average are not modeled; the mission formalizes the section's explicit lead-time-demand cost reduction. Contributions that establish integrability, distribution identities, strict convexity, and critical-ratio optimality are all needed for closure.
In airline and hotel revenue management a firm sells a fixed stock of a perishable resource (seats on a flight leg, rooms on a night) over a finite selling horizon, and in each period decides which fare classes to open. Customers do not buy a fixed fare: they choose among the fares on offer, or leave. Talluri and van Ryzin (Management Science, 2004) formulated this single-leg, choice-based problem as a dynamic program over the time remaining and the units remaining.
Practical revenue management systems rarely offer arbitrary sets of fares. They use nested controls: fares are opened from the most expensive downwards, so the open set is always "every fare above some threshold". Whether restricting to such revenue-ordered offer sets is natural depends on how the optimal threshold moves as the state changes. For mixtures of multinomial logit models, Rusmevichientong, Shmoys, Tong and Topaloglu (Production and Operations Management, 2014, Theorem 6) showed that the best revenue-ordered threshold moves monotonically in both the remaining capacity and the remaining time.
Berbeglia and Joret (arXiv:1606.01371v3, §5, Theorem 5.1) extend these two monotonicity properties to every regular discrete choice model, the class that contains essentially every model used in revenue management, including all random utility models. This mission formalizes that result.
A finite nonempty set of products is sold. For a choice set and a product , is the probability that a customer offered buys ; the no-purchase probability is . The system is regular when (i) all these probabilities are nonnegative, (ii) for , (iii) , and (iv) whenever , for every and for the no-purchase option .
Each product has a revenue . Let be the distinct revenues. For the revenue-ordered assortment is ; a larger index gives a smaller set, .
In the multi-period model one customer arrives per period. With periods remaining and units left, the firm offers some . The values of the revenue-ordered dynamic program are
when or , and . The optimal revenue-ordered index is the smallest maximiser,
and is the marginal value of capacity.
For every and ,
More units left give a weakly larger optimal offer set; more periods left give a weakly smaller one. The paper states the theorem for , ; the horizon and the capacity only bound and , so the goal is stated for all .
Milestones 5–7 are asserted or cited in the paper, not proved there; milestones 6–7 are stated for this restricted dynamic program, which is the one the paper applies them to.
The theorem says that a firm restricted to revenue-ordered offer sets can implement its policy as a nested booking control: as seats sell out, the threshold fare can only rise, and as departure approaches with seats in hand, it can only fall. This is the structure that standard revenue management systems already assume, and Rusmevichientong et al. point out that such monotonicity can be used to implement them. The paper's contribution is that the property depends only on regularity of the choice model, not on its multinomial-logit form.
Formalizing it adds a machine-checked statement of the single-leg choice-based dynamic program over a general choice model, a precise account of the tie-breaking rule (the smallest maximiser), and machine-checked versions of the two marginal-value monotonicity facts that the paper cites from Talluri and van Ryzin rather than proves. To our knowledge none of these statements has been formalized in any proof assistant; the paper's proofs are informal.
The paper's proof is short, but two of its steps are not proved there. The marginal-value inequalities are imported from Talluri and van Ryzin, whose dynamic program optimises over all offer sets; here only the revenue-ordered sets are available and the empty set is not, so those proofs have to be redone for this program, and the bound is needed to keep each stage's shifted problem well behaved. The claim itself is justified on the page only by an informal sentence.
The second subtlety is tie-breaking. The monotonicity is about the smallest optimal index. Several indices can be optimal at once, and the comparison of Lemma .1 transfers optimality of one index from one shift to another only through Lemma 2.1, that is, through the no-purchase case of the regularity axiom. Without that case the statement fails.
C; choice probabilities are P : C → Finset C → ℝ, defined on all pairs. The no-purchase option is not a product: its probability is the derived quantity noPurchase P S = 1 − ∑_{x∈S} P x S.IsChoiceSystem P is axioms (i)–(iii); IsRegular P adds axiom (iv) for products and for the no-purchase option. Milestones 5–7 assume only axioms (i)–(iii), as the paper says suffices; Lemma .1, (16), (18) and the goal assume regularity and .level r ℓ is for , topRevenue r is , and roSet r ℓ is as a Finset. The paper's sorting of products () is notation only and is not used.Finset.sup', and the minima defining and are Finset.min' over sets proved nonempty.Formalizations that would trivialize the statement are ruled out: the dynamic program maximises over the revenue-ordered sets only, never over all subsets (that is Talluri and van Ryzin's program); is the smallest maximiser, never the largest; and , , and the choice model are arbitrary, never fixed.
The definitions (regular choice model, revenue-ordered assortments, the restricted dynamic program) are reusable for other results on nested policies. Proofs of the cited Talluri–van Ryzin lemmas for this program are especially welcome, as they are the part the paper leaves to the literature.
A retailer who controls both inventory and price can respond to a supply contract in two ways. A contract that induces the right order quantity at a fixed price may change the retailer's incentive to raise or lower that price. For a one-season supply chain, Cachon's chapter compares familiar contracts under price-dependent demand and identifies a price-contingent buy-back, also called a price-discount contract, that aligns both decisions. The mission concerns §6.3 of the author's January 2003 third draft, on printed pages 33–38. Those page and equation numbers belong to the draft and may differ from the typeset chapter.
One risk-neutral supplier and one risk-neutral retailer have full information before a single selling season. The retailer chooses a nonnegative stocking quantity and a retail price from an admissible price set ; the price stays fixed during the season. Demand has a probability law that depends on . Write for its distribution function, for expected sales, and for mean demand. Demand is nonnegative, has a finite mean and, in the chapter's regular setting, its distribution function increases with demand level and has a positive price derivative at positive demand levels. Higher prices thus lower demand in the stochastic order used by the chapter. The price set is nonempty and open so an admissible price optimum has an interior first-order condition.
The supplier's unit cost is , the retailer's unit procurement cost is , and is total unit cost. Their goodwill penalties for unmet demand are and , with . An unsold unit has salvage value at the retailer. The integrated channel's expected profit is
A buy-back contract charges a wholesale price for each ordered unit and pays the retailer for each unsold unit. A revenue-sharing contract charges a wholesale price and gives the retailer a fraction of sales and salvage revenue. In this section the supplier offers the terms and the retailer chooses . The profit formulas use the chapter's convention that a positive transfer goes from retailer to supplier.
The goal is the price-contingent buy-back on p. 35, with :
In the chapter's zero-goodwill case, , every feasible then gives the retailer and the supplier . The same retailer profit is obtained from revenue sharing with and . Thus every existing maximizer of the integrated profit maximizes each firm's profit under the contingent buy-back. At the retailer is indifferent; at the supplier is indifferent.
The milestones follow the chapter's printed claims in attack order:
The result identifies a contract schedule under which the same quantity-price pair is best for the integrated channel and for the two firms' reported profit functions. It also explains the relation between a buy-back whose terms vary with the chosen price and a revenue-sharing arrangement. In the zero-goodwill setting, both allocate every realized choice's expected channel profit in fixed shares. The general-goodwill identity shows the additional mean-demand terms that matter when the retailer controls price.
The source presents these results analytically; this mission asks for Lean proofs of the stated price and profit relationships. A published Prove2Me definition already supplies expected sales and mean demand for a single demand law, and the model here applies those functions to each price's law. The earlier open theorem RevShareCoord.Single.price_quantity_coordination (from Cachon and Lariviere's revenue-sharing paper) treats deterministic revenue and a simpler cost convention. It is an overlap in theme, but its statement does not include price-indexed demand, salvage value, retailer cost or the contingent buy-back terms, so it is not posed again here. The new model can support further price-dependent contract comparisons in the chapter.
The obstacle is that matching the retailer's quantity incentive at a fixed price can change the retailer's price incentive. The buy-back rate required by the fixed-price coordination equations depends on ; a fixed buy-back contract therefore does not generally align both choices. Revenue sharing with goodwill penalties has a similar price dependence. The integrated profit need not be concave or unimodal in , so a price first-order condition by itself does not establish coordination. The chapter assumes a finite integrated optimum exists and treats the price condition as necessary, not sufficient.
Lean represents price-dependent demand as a family of probability measures on , one for each price in . Each admissible law is supported on nonnegative demand, has no atom at zero and has an integrable identity function, so is a genuine finite expectation. Sales are defined by , using the published SupplyChainTheory_contracts definition; they are not defined by the equivalent CDF integral. The admissible decisions are exactly and . Unit costs and goodwill penalties are nonnegative, each admissible price exceeds , and , as in the model of §6.2. The chapter's standing risk-neutrality and full-information conventions appear in the use of expected profit with the same demand laws available to both firms.
There is a material qualification. With price-dependent demand, may change with . The printed first-order condition (14) and the p. 36 inference from to a joint optimum omit that effect when goodwill penalties are positive. Price first-order and optimality statements here therefore use , a case explicitly discussed in the chapter; general-goodwill claims are limited to algebraic identities. The printed p. 36 equality of price derivatives under revenue sharing also misses its factor , which the formal statement restores. The contingent buy-back terms are defined by the chapter's linear formulas, not by a property that hard-codes coordination. The algebraic statement permits parameter values that may violate economic buy-back bounds such as ; those bounds need separate checks when selecting a contract.
Two first-order statements, (15) and (16), compare price derivatives; they take the derivative of expected sales in price as a hypothesis, and (15) also takes differentiation under the integral sign of as a disclosed regularity hypothesis. For the quantity discount, the statement claims what the page shows, undistorted prices for each and optimality of given , not joint optimality of for the retailer. The page's claim that revenue sharing with goodwill coordinates only with is not stated, for the mean-demand reason above.
A trivializing formalization is ruled out: no contract term is defined by the profit identity it should satisfy, the demand family cannot be replaced by a single law, and the optimal pair is a hypothesis about the integrated profit, not a chosen witness.
Reusable contributions include the price-indexed demand family, the expected-profit model with five contract types, and the price-maximizer statements. Proofs of the first-order milestones need Fermat's interior-extremum theorem on the open price set and, for (15), positivity of an interval integral; the identities need the expectation algebra of and , including .
A minimum-cost circulation is a way to send flow around a directed network while respecting capacities and paying a cost per unit on each arc. It is a basic form of network optimization: a minimum-cost flow with prescribed supplies and demands can be reduced to a circulation problem, and the circulation formulation exposes the residual arcs on which a flow can be improved. Goldberg and Tarjan's successive-approximation method relaxes exact optimality by an error parameter and repeatedly reduces that error. Its ordinary stopping rule for integer costs depends on the largest cost. For arbitrary real costs, including irrational costs, a decreasing positive error need never cross a fixed numerical cutoff. The strongly polynomial loop in their 1987 technical report, later published in Mathematics of Operations Research instead tests the smallest error parameter appropriate to the current circulation and stops when it is zero.
This mission formalizes the number of refinement calls made by that loop. It builds on the related Goldberg–Tarjan 1988 max-flow and 1989 minimum-mean cycle-canceling series: those develop different algorithms for network flow, while the published 1989 circulation and approximate-optimality definitions provide this mission's common network model. The result here concerns successive approximation and its fixed-arc progress measure.
The vertex set is finite, with , and is a symmetric set of directed arcs, with . Symmetry means that brings too. Each arc has a real capacity and a real cost ; costs obey . A circulation obeys , , and conservation of flow at every vertex. Its total cost is half the sum of over directed arcs, since each unordered edge appears twice. A minimum-cost circulation costs no more than any other circulation of the network.
The residual capacity is . For a price function , the report writes the reduced cost as . A circulation is -optimal with respect to when every residual arc has reduced cost at least . It is -optimal if some price function works, where . The tight error is the least such error. A circulation is -tight when it is -optimal but fails to be -optimal at every . This includes attainment at .
An arc is -fixed if all -optimal circulations carry the same flow through it. Write for the set of these arcs. Theorem 4.2 supplies an arc-fixing criterion from a large absolute reduced cost. Lemma 4.4 says that when a positive tight error falls by a factor of , becomes strictly larger. Both are numbered results on printed pages 16–17 of the source report's journal counterpart.
The goal is the circulation-level form of Theorem 4.5. Begin with a circulation and a sequence whose positive-error steps satisfy the contract of Figure 3: if , the next circulation is -optimal. With the report's standing and , the target is
The milestone list contains the already proved complementary-slackness characterization of minimum cost (Theorem 2.2), the cross-parameter arc-fixing result (Theorem 4.2), and strict growth of fixed arcs (Lemma 4.4). The report states Theorem 4.5 as iterations when each refinement decreases error by a constant factor. The target makes explicit the factor two used by the paper's refinements and the resulting finite count.
The theorem gives a bound on the number of refinement calls that depends on the number of vertices and arcs, not on the magnitude, precision, or integrality of the costs. It gives an exact minimum-cost circulation rather than an arbitrary small-error approximation. This distinguishes the real-cost loop from an integer-cost stopping rule based on . The bound counts refinement calls only; the report analyzes the work within particular implementations separately.
The published 1989 definitions and the complementary-slackness theorem already have machine-checked status on the platform. Theorem 4.2, Lemma 4.4, and this iteration theorem are the open formalization targets. A complete development will connect the tight error to residual-cycle structure, establish that its infimum is attained for circulations, and prove that zero tight error implies minimum cost. The mission thereby makes the fixed-arc argument reusable for other circulation algorithms that lower an approximate-optimality parameter.
Repeatedly dividing a positive real error by two gives errors approaching zero, but it does not by itself produce a finite step with zero error. The missing finite progress is structural: an arc must become fixed after enough reductions, and only finitely many arcs exist. Proving that fixedness is strict is delicate because it compares all circulations at two different error levels, not just two consecutive flows. Theorem 4.2 is the quantitative bridge between a price certificate for one flow and agreement of an arc across every sufficiently accurate flow. At the boundary , the printed wording of Lemma 4.4 would require to be a proper subset of itself, so its positive-error regime must be made explicit.
The Lean network uses CycleCanceling.MinMean.CircNetwork with a finite vertex type, a finite symmetric arc set, and real-valued capacities, costs, and flows. Off-arc values of these functions are irrelevant. The report assumes on printed page 5; the theorem binders express it as and . The arc count is for ordered arcs, exactly as the report defines . No integrality, rounding, or bounded-cost hypothesis is imposed. A feasible initial circulation is required because Figure 3 starts from one; infeasibility detection is outside this target.
The reused 1989 definitions write reduced cost as . Substituting for gives the report's , so existential price certificates, -optimality, and absolute reduced-cost conditions agree. The tight error is represented by a real infimum; proving that it is attained is part of the work. The set is filtered from and includes only arcs whose flow is shared by all -optimal circulations. The halving run computes its error from the current circulation; it does not take an unrelated error sequence. Once that error is zero, the loop has returned and later sequence entries are unconstrained. These choices exclude a vacuous or artificially fixed error parameter and a preselected optimal flow.
The explicit reading of the report's asymptotic count is halvings per factor- reduction and at most such blocks, giving refinements. This is a statement about refinement count, not a RAM-operation bound. Contributions on Theorem 4.2, the residual-cycle characterization of positive tight error, the fixed-arc strictness lemma, and the final finite counting argument all support the goal. The circulation, price, and fixed-arc infrastructure can be reused beyond this particular implementation.
Online bipartite matching asks an algorithm to assign arriving requests to resources it cannot reassign later. In display advertising, the requests are page views (impressions) and the resources are advertisers who have bought a fixed number of impressions in advance; each impression must be served immediately or lost. In the adversarial model, Karp, Vazirani and Vazirani (STOC 1990) showed that the RANKING algorithm achieves a fraction of the optimum in expectation, and that no online algorithm does better. Advertising systems, however, have historical traffic data, which motivates the i.i.d. model: the impression types are drawn independently from a distribution that is known in advance.
Feldman, Mehta, Mirrokni and Muthukrishnan (arXiv:0905.4100, FOCS 2009) were the first to beat in this model, with an algorithm that achieves with high probability. Their Section 3 asks the complementary question: how close to can any online algorithm get when the distribution is known? Their Theorem 3 answers that the expected approximation factor of every online algorithm is bounded strictly away from , already on a graph with six vertices. Later work in the same model (Manshadi, Oveis Gharan and Saberi, SODA 2011, arXiv:1007.1673) sharpened both the algorithmic and the hardness side.
An instance consists of a bipartite graph between a finite set of advertisers and a finite set of impression types, a distribution on , and a number of arrivals. In this mission is the uniform distribution on . Online, impressions arrive one at a time; their types are independent draws from . When impression arrives, the algorithm must immediately either assign it to an advertiser with that has not yet been used, or leave it unassigned. Each advertiser can be used at most once, and decisions are final.
A deterministic online algorithm decides what to do with arrival from the types seen so far; it knows , and , but not the future. A randomized online algorithm is a probability distribution over deterministic ones. is the number of impressions the algorithm assigns on the arrival sequence . is the size of a maximum matching of the realization graph, which has one node per arrival , joined to every advertiser adjacent to : the most impressions that could have been assigned with hindsight. The expected approximation factor of an algorithm is
the expectation taken over the algorithm's randomness and the arrivals.
The 6-cycle instance has , and , with the uniform distribution and . The family consists of disjoint copies of the 6-cycle, with the uniform distribution on its impression types and arrivals.
On the 6-cycle, every randomized online algorithm satisfies
and there are a constant and a threshold such that for every and every randomized online algorithm on ,
The second part is the paper's "there exists a family of instances with for which no algorithm can achieve an expected approximation of ", stated on the paper's own family. It leaves unspecified: Appendix B estimates through approximate counts, and a sharper constant would not invalidate the goal.
Theorem 3 sets the ceiling against which algorithms in the i.i.d. model are measured. It rules out an online algorithm with expected factor arbitrarily close to , even though the distribution is known and the instance is tiny, so a constant-factor gap between online and offline matching is intrinsic to the model and not an artefact of adversarial arrivals. The paper's positive results ( for the Suggested Matching algorithm, for Two Suggested Matchings) sit between and this ceiling.
The single-instance bound has a short counting proof. The family statement is argued in the paper only in outline: Appendix B approximates the fractions of copies receiving , , or more impressions, assumes the most favourable outcome on each, and reports the resulting ratio as approximately . A machine-checked proof of the family statement would turn that sketch into a theorem with an explicit constant. To our knowledge neither part has been formalized before.
The single-cycle bound reduces to a finite check, but the paper's "without loss of generality (from the symmetry of the 6-cycle)" hides the cases the algorithm can choose: assigning the first impression to either neighbour, or not assigning it at all. Each case needs its own bad continuation. The passage from deterministic to randomized algorithms is an averaging step.
The family bound is harder. On the algorithm sees all arrivals in all copies and may coordinate its decisions across copies, so the per-copy loss of the single cycle does not transfer by independence. Moreover the target is the expectation of a ratio, , not a ratio of expectations: a bound on the expected loss must be combined with concentration of the number of copies that receive exactly three impressions, and with a lower bound on that holds with high probability. The approximations ", , " of Appendix B have unquantified errors and cannot be used as they stand.
The model is formalized for general finite and with uniform arrivals. Arrival sequences are functions Fin n → I. A deterministic online algorithm is a function that receives the time , the prefix of the first types (Fin t → I) and the current type, and returns an advertiser or none; it cannot read later arrivals. A proposal of a non-adjacent or already used advertiser leaves the impression unassigned, so the encoding covers all online algorithms, including ones that skip an impression while a neighbour is free. A randomized online algorithm is a probability distribution (PMF) on the finite type of deterministic algorithms; by Kuhn's theorem this is equivalent to fresh random choices at each step. is the maximum size of an injective, edge-respecting partial assignment of arrivals to advertisers. The expected approximation factor is a finite average over all arrival sequences, weighted by the algorithm distribution.
The explicit instantiations of the paper's asymptotic wording are as follows:
Lean's division sets . A formalization of the form "there is an instance on which every algorithm has expected factor at most " would be satisfied trivially by a graph without edges, where ; the statements here are on the paper's explicit instances, where every impression type has an adjacent advertiser and on every arrival sequence.
A complete development needs finite case analysis on runs of online algorithms, averaging over mixed strategies, and, for the family, concentration inequalities for occupancy counts (Azuma or McDiarmid, both available on the platform) together with bounds on maximum matchings of disjoint unions. The online-algorithm model and the averaging lemmas are reusable for other lower bounds in the i.i.d. model. Proofs of either milestone, and independent proofs of the family statement with any explicit , are welcome.
Policy gradient methods optimize a decision rule by changing the parameters that determine its action probabilities. In reinforcement learning, the objective is the expected total reward collected over time. Once a policy is restricted to a feature-based class, the best policy may be less effective than the unrestricted optimum. A useful guarantee must therefore compare the computed policy with a chosen comparator and account for both the limits of the features and the error in estimating an update direction. Agarwal, Kakade, Lee and Mahajan give such a guarantee for a version of the natural policy gradient method that fits action values with linear features, called Q-NPG (Agarwal et al., §6.2).
The result matters when a policy has far fewer parameters than there are state-action pairs. A bound phrased only for exact action values or an unrestricted policy class would leave out the errors introduced by fitting from samples and by moving the fitting distribution from the states of a comparator to the states visited by the current policy. Theorem 6.1 keeps those effects visible as separate terms. It also avoids assuming that the comparator is an optimal policy; the comparator can be a policy selected for an application or a benchmark within a restricted class.
A discounted Markov decision process has a finite state set S, a finite nonempty action set A, transition probabilities P(s'|s,a), immediate rewards r(s,a) in [0,1], and a discount factor γ in [0,1). A policy π assigns a probability distribution over A to every state. The value V^π(s) is the expected sum of discounted rewards from s, and V^π(ρ) averages this value over an initial state distribution ρ. The action value Q^π(s,a) starts by choosing a in s and then follows π. Its advantage is A^π(s,a)=Q^π(s,a)−V^π(s). These are the unnormalized value conventions of §3, pp. 9–12.
For each state-action pair, fix a feature vector φ(s,a) in Euclidean d-space. The log-linear policy with parameter θ assigns probability proportional to exp(θ·φ(s,a)):
The Q-NPG fitting loss is the mean squared error of predicting by under a state-action distribution . Q-NPG uses an approximate minimizer w of this loss under its current on-policy measure and updates θ by ηw. The distribution ν specifies the initial state-action pair for that measure. At time zero, the pair is drawn directly from ν; the given initial action is executed before later actions follow the current policy. These definitions are (19)–(20) of §6.2, pp. 27–28.
The comparison policy π⋆ has discounted state visitation distribution . The paper's transfer measure pairs those states with a uniform action from A. The excess risk measures how much worse an approximate fitting direction is than an exact constrained minimizer under the current on-policy measure. The transfer error measures the exact minimizer's loss under . A relative condition number κ bounds, in every feature direction, the covariance quadratic form under by κ times that under ν (Assumptions 6.1–6.2, pp. 28–29).
The goal is Theorem 6.1, p. 29. Starting with θ⁽⁰⁾=0, taking T positive updates with step size , bounding feature norms by B and update norms by W, and assuming the expected excess and transfer errors are at most and , respectively, it asserts
The expectation encloses the minimum: each random run may have a different best iterate. The claim gives a finite-horizon comparison with π⋆ even when π⋆ is not globally optimal.
The milestones are the paper's performance-difference identity (Lemma 3.2), smoothness of bounded-feature log-linear policies (Remark 6.7), the deterministic NPG regret lemma (Lemma 6.2), and the two displayed bounds that control transfer and estimation terms ((25) and (26)). Together they connect the MDP's value comparison with the two statistical errors in the goal. Each milestone states a source result rather than a weakened surrogate.
The theorem separates three quantities that can vary independently in an application: the number of iterations, the statistical quality of the update direction, and the mismatch between the comparator's visited states and the fitting distribution. If both errors vanish, the displayed bound decreases with T at a square-root rate. With imperfect features, the transfer term shows the remaining performance limit. With finite-sample fitting, the excess-risk term shows how estimation quality affects the policy value. This is an agnostic statement because the comparator need not belong to a globally complete policy class (Agarwal et al., Theorem 6.1 and discussion, pp. 29–30).
The paper proves these claims mathematically. This mission asks for machine-checked proofs of the same statements in Lean, including the probabilistic expectation and the exact constants. The reusable parts are the state-action visitation distribution with a prescribed initial action, the log-linear policy and its smoothness property, the least-squares loss, and the deterministic regret lemma. Those objects can support other policy-gradient analyses with different fitting guarantees.
The update direction minimizes a loss under the distribution generated by the current policy, while the value comparison uses states visited by a different policy. The two distributions need not agree, and prediction error under one cannot simply be substituted for error under the other. The relative condition number controls the feature geometry of this shift, while the transfer error separately measures how well an exact on-policy fit predicts under the comparator's measure. Random approximate minimizers add a further layer: the bound concerns the expectation of the best iterate in each run, rather than a deterministic iterate chosen in advance. These are the obstacles identified around Assumptions 6.1–6.2 and the proof of Theorem 6.1.
The Lean development uses finite state and action types, as in the paper's §3 standing setting. It imports published definitions of transition kernels, policies, occupation probabilities, value and Q-functions, and defines this paper's advantage, discounted visitation, log-linear class and fitting loss on top of them. Parameters and features lie in EuclideanSpace ℝ (Fin d), so the norm is the Euclidean norm used by the paper. A general probability space carries the random update directions and exact constrained minimizers; their measurability and boundedness make the displayed loss expectations integrable.
The action type is nonempty so that the uniform action distribution exists. B and W are positive and T is positive, because the prescribed step size divides by and the result minimizes over . The comparator is assumed to be a policy, with no optimality hypothesis. The nonnegative condition number is represented by its quadratic-form upper-bound property for every direction. This avoids undefined real ratios when a covariance form vanishes and includes the finite coefficient in Assumption 6.2. The value and loss expressions are calculated from P, r, π and φ; they are not free variables. The Q-NPG parameter sequence is defined by the update rule from θ⁽⁰⁾=0. In particular, the goal does not assume the regret lemma or either of the two statistical inequalities that the proof must establish.
The paper notes that some §6 results extend beyond finite state or action spaces. This mission fixes the finite case inherited from §3. Contributions that prove the source milestones, establish the required summability and integrability facts, or generalize the development to larger measurable spaces are useful; a generalization must keep the same statistical and comparator conventions.
Policy gradient methods adjust a policy by following derivatives of its expected reward. A common expectation is that a small gradient indicates a policy close to optimal. For discounted Markov decision processes, that interpretation can fail when a policy rarely reaches the states where reward is available. Agarwal, Kakade, Lee, and Mahajan study this obstruction as part of their analysis of optimality and distribution shift in policy gradient methods. Their chain example makes the obstruction quantitative: even derivatives of several orders can be exponentially small while the value gap grows with the chain length. Agarwal et al., §4.3 and Proposition 4.1.
The example isolates a specific issue for local optimization. A parameter change at an early state affects reward only after the agent has passed through many intermediate decisions. A local derivative therefore measures the behavior of a policy under its own visitation pattern, which can be very different from the visitation pattern of an optimal policy. This mission states the resulting separation with explicit constants rather than treating “vanishing gradients” as a qualitative description.
A discounted Markov decision process has a finite set of states, a finite set of actions, a transition probability for each state and action, a reward in , and a discount . The value of a policy is the expected sum of discounted rewards when the process starts in state and follows . An optimal policy has value at least as large as every other policy at every state. These conventions are those of §3 of the paper and its unnormalized infinite-horizon value definition. Agarwal et al., §3, pp. 9–12.
The central model is a deterministic chain with states and four actions. At the process moves to . At each interior state , action moves forward to , while move backward to . State is absorbing. The only positive reward is , and . This is Figure 2 and the transition matrix in equation (27). Agarwal et al., Figure 2, p. 11, and (27), p. 50.
The direct policy parameter has three free coordinates at each interior state: the probabilities assigned to . The probability of is their complement. Write for this policy expression and for its value from the starting state. The paper studies parameters whose free coordinates lie strictly between zero and one and whose forward-action coordinates satisfy .
The goal is Proposition 4.1. For , every such , and every nonnegative integer satisfying , it asserts the multilinear operator-norm bound
The same statement compares this policy with an optimal policy:
Both clauses and their constants are part of the target. The derivative order includes whenever the displayed threshold admits it. Agarwal et al., Proposition 4.1, p. 16.
Three supporting targets follow the appendix's attack path. First, equals the entry of the resolvent , where . Second, equation (32) gives the derivative of any entry of in one forward probability. Third, the appendix separately bounds the optimal value below by and above by . A companion theorem records Lemma 3.1: a five-state deterministic example has a value function that is nonconcave in both the direct and softmax parameterizations. Agarwal et al., Appendix B.2, pp. 51, 54, 59; Lemma 3.1, p. 11.
The proposition supplies an explicit family in which local derivative information, even at orders growing with , is small at policies with a large value gap. It limits what a guarantee based only on finding a point with small low-order derivatives can imply about global policy quality. The paper uses this example to motivate attention to state visitation and distribution mismatch in its positive results. Agarwal et al., §4.3, pp. 16–17.
The mathematical result is proved in the cited paper. The remaining work is a machine-checked development of the chain model, its value and resolvent identities, the higher derivative estimates, and the value-gap inequality. The reusable parts include finite-state discounted value calculations, differentiation of a matrix inverse, and operator-norm estimates for multilinear derivatives. The statements in this proposal are proof targets; they do not themselves claim that those proofs have been formalized.
A policy can have a small gradient simply because it almost never reaches the rewarding state. The obvious inference from a near-zero gradient to near-optimal value therefore fails in this model. The technical difficulty is quantitative: each differentiation of a resolvent entry produces terms involving several entries, and the operator norm combines all mixed partial derivatives. The bound must remain exponentially small after that combination, uniformly over every derivative order allowed by the threshold. The second clause must simultaneously show that a policy taking the forward action reaches the reward often enough to create a large value gap. Agarwal et al., Appendix B.2, pp. 54–59.
States are Fin (H + 2) and actions are Fin 4; the parameter space is EuclideanSpace ℝ (Fin H × Fin 3). Its norm is the Euclidean norm, so the norm of the iterated Fréchet derivative is the paper's multilinear operator norm. The first and last states have no free policy parameters. All four actions at induce the same transition to , and the parameterized policy chooses at both boundary states. The resolvent is the matrix inverse of ; its milestone statements are restricted to interior probabilities , where that inverse is nonsingular.
The displayed coordinate assumptions of Proposition 4.1 do not require the three free probabilities at a state to sum to at most one. The Lean goal retains exactly those assumptions. Its value expression is still determined by the forward probabilities, because every other action has the same backward transition and only the absorbing state yields reward. This prevents an added simplex constraint from silently narrowing the proposition. A constant function or a free value variable cannot replace the chain value: is computed from the concrete transition and reward arrays.
The development uses the published finite-state transition-kernel, policy, occupation, value, and optimal-policy definitions. Contributions needed for a proof include stochasticity of the chain, geometric-series evaluation of its absorbing reward, nonsingularity and differentiation of its resolvent, and estimates that pass from mixed partial derivatives to the Euclidean operator norm. For the companion example, direct parameters lie in the product of action simplices, with positive discount; at zero discount its value is constant and the nonconcavity claim would be false.
A stochastic dominance constraint asks a random outcome of a decision to be at least as good as a benchmark outcome for every risk-averse decision maker: in the second-order version, for every concave nondecreasing utility . Dentcheva and Ruszczyński introduced optimization problems with such constraints in Optimization with stochastic dominance constraints (SIAM J. Optim. 2003), where the outcome itself is the decision variable, and extended the theory in the paper this mission formalizes, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints (Math. Program. 2004, DOI 10.1007/s10107-003-0453-z), to outcomes that depend nonlinearly on a decision .
The paper's §4 builds a Lagrangian dual of these problems. The multipliers of the -th dominance constraint are a utility function and an almost-sure multiplier for the coupling . The dual functional splits into a part that involves only the decision and one part per dominance constraint. This mission is about the second kind of part: Theorem 4 computes in closed form as a concave conjugate, and Theorem 5 gives its subgradients. Those two facts are what make the dual problem amenable to nonsmooth optimization and decomposition methods, which is the purpose the paper states for them.
The underlying shortfall function and its dual characterization are due to Ogryczak and Ruszczyński (Dual stochastic dominance and related mean–risk models, SIAM J. Optim. 2002). The pure-dominance case of the optimality theory is the 2003 paper above.
Let be a probability space, the integrable and the essentially bounded random variables. Fix a bounded interval () and a reference outcome .
The utility class consists of the functions that are concave and nondecreasing, vanish on , and are affine on : for , with a constant . For such , the left derivative at is that slope .
The concave conjugate of is
For a random variable , is the extended-real random variable .
The dual functional of one dominance constraint, eq. (34), is
The functional of eq. (35) is , considered on , where is the space of Lipschitz functions with norm .
For every and every ,
The formal statement has two cases. If almost surely, then is a.s. finite and integrable and the identity holds between real numbers. Otherwise .
Theorem 4 reduces an optimization over the infinite-dimensional space to one scalar maximization per scenario: the dual functional is an expected conjugate. It identifies the effective domain of the dual in the multiplier (bounded between and the slope of the utility at the left end of the interval), and it makes evaluating as cheap as evaluating . Theorem 5 supplies explicit subgradients, the law of a maximizer and the maximizer itself, which is what bundle and cutting-plane methods for the dual problem (31) consume. The paper's §5–§6 build their finite-scenario theory and numerical method on this decomposition.
Both theorems are proved in the paper. Neither has a machine-checked proof; no concave conjugate on with values in , no dual functional of this kind, and no measurable-selection theorem for argmax correspondences of this shape exist on the platform. A complete formalization would provide reusable infrastructure: an extended-real concave conjugate, interchange of supremum and expectation for a scalar integrand with a bounded maximizer, and a concrete measurable-selection argument.
The hard step is the interchange . The inequality "" is pointwise, but "" needs a random variable that attains the pointwise maximum, is measurable, and is integrable. The paper cites Rockafellar–Wets for both the interchange and the selection. The maximizers are not unique: where or the argmax is an unbounded half-line, so an arbitrary measurable selection need not be integrable, and the bounded one must be constructed. The unbounded cases need care because is only essentially bounded and the test outcomes must be shown integrable.
This chunk's objects are in NonlinSSD.DualFunctional; it imports the already moderated utility class NonlinSSD.Optimality.U1. Random variables are functions on a probability space with IsProbabilityMeasure P; is Integrable, is MemLp ζ ⊤ P. The conventions and explicit readings:
derivWithin v (Set.Iic a) a, never deriv v a, which is at a kink.EReal-valued, so an infimum equal to and a supremum equal to are represented, not replaced by . The supremum in is over integrable only.A trivializing formalization is ruled out: a real-valued conjugate or dual functional (junk at ), a supremum over all measurable (junk integrals), or a one-sided case split would each make the goal easier than the paper's theorem, and a sorry-free check confirms that both cases of Theorem 4 are inhabited (, and ).
Contributions are welcome at every level: proofs of the milestones in order, general lemmas on extended-real conjugates on , and a measurable argmax selection for continuous integrands over a compact interval, which is reusable well beyond this paper.
Boundary feedback is the standard way to stabilize vibrating structures governed by wave equations: a sensor measures the velocity at the boundary and an actuator applies a force proportional to it. For the one-dimensional damped wave equation with such feedback, the closed loop is uniformly exponentially stable (Chen, 1979). In practice the measured velocity reaches the actuator only after a computation time, so the feedback acts with a time delay . The question addressed by Datko, Lagnese and Polis (1986) is whether arbitrarily small delays can destroy the stability of a system that is stable without them.
Their note answers it with an explicit example and a sharp threshold on the feedback gain. It is the founding example of delay-induced instability in boundary stabilization, cited by most later work on robustness of boundary control to delays.
Timeline.
Fix real numbers (damping), (feedback gain) and (delay), and put . The delayed system is
A classical solution is a function with complex values satisfying (1), (2), (8).
Separated solutions lead to the eigenvalue problem
The spectrum is the set of for which this problem has a solution not identically zero on . The paper encodes it through the entire functions
and the critical gain . In Lean these are K a, f a k ε ω, h a k ε ω, delaySpectrum a k ε, IsClassicalSolution a k ε u and IsExpUnstableSolution a k ε u in the namespace DatkoDelayWave.BoundaryDelay.
In attack order: the characteristic equation (16) ( for ); separated solutions; Lemma 1 (one zero of forces infinitely many zeros of and in every vertical strip around it); (17)–(18) (no zeros of in the right half-plane below or at the critical gain); the half-plane bound below the critical gain; (19) (no purely imaginary zeros at the critical gain); the explicit zero ; density of the delays ; the root family (12)–(15) above the critical gain; Lemma 2 (an open dense set of delays with zeros of in ); the three parts of the THEOREM separately; and, off the goal's path, the undelayed formula for .
The result shows that exponential stability obtained by boundary velocity feedback is not robust to delays when the gain is above : delays from a dense set of lengths, including arbitrarily small ones, produce exponentially growing modes. When the critical gain is , so every positive gain is fragile. Below the critical gain the spectral gap survives every delay. This identifies a quantitative robustness margin and motivated the later analysis of delayed boundary control, including the Nicaise–Pignotti theorems already posed on the platform for a different, multidimensional model (NicaiseDelayWave.*).
The result is proved in the paper, partly by citation: Lemma 1 is quoted from Datko (1978) without proof, and the open-mapping step of Lemma 2 is sketched. No machine-checked version exists. A formalization would check the threshold computations, supply the strip-zero lemma for this exponential polynomial, and give a rigorous version of the open-mapping step.
The algebraic parts, (16)–(19) and the explicit zeros, are calculations with complex exponentials. The difficulty is in Lemma 1 and Lemma 2. Lemma 1 needs the almost-periodic structure of exponential polynomials in vertical strips together with a Hurwitz or Rouché type argument, and neither is in Mathlib. Lemma 2 needs zeros of to persist under small changes of the real parameter . The paper's route through the logarithmic map (11) does not work as printed, because it is stated with the principal branch exactly on the branch cut. In part (i), the delicate step is excluding accumulation of zeros at the imaginary axis as , which the half-plane estimate alone does not give.
Parameters are real, , eigenfunctions are maps and solutions are maps (space first). Partial derivatives are deriv of the sections. Solutions and eigenfunctions are required to be on all of , resp. ; this loses no eigenvalue, since solutions of (5) are combinations of . Committed readings of the paper's loose phrases:
Trivializing encodings are ruled out: defining the spectrum as the zero set of would make a spurious spectral point, and reading "exponentially unstable" as "the spectrum meets " would delete the solution-level content of part (iii).
A complete development needs zero-counting tools for exponential polynomials in strips (almost periodicity, Hurwitz's theorem), which would be reusable for other delay equations. Contributions to any milestone, and to that general infrastructure, are welcome.
Online set cover is the basic covering problem in which the requests arrive over time. A ground set of elements and a family of sets are known in advance, but which elements must be covered is revealed one element at a time, and each arriving element has to be covered at once by a set chosen irrevocably. The problem models resource placement under unknown demand (facilities, servers, sensors that must serve clients as they appear) and is the prototype for a family of online covering problems.
Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 2009) gave the first deterministic algorithm, with competitive ratio for elements and sets, and showed that no deterministic algorithm does better than on some instances. Buchbinder and Naor (Math. Oper. Res. 2009) recast the fractional part of that algorithm as an instance of a general online primal-dual scheme for covering and packing linear programs, and turned an offline pessimistic estimator of Srinivasan into an online potential function. The result, in their Section 5.1, is a deterministic algorithm whose ratio depends on the maximum element frequency instead of the number of sets , and on the ratio instead of .
Timeline:
A set-cover instance consists of a finite ground set of elements and a finite family of sets. For an element , is the collection of sets containing , and bounds its size: for every (the frequency). In the unweighted problem every set costs .
Elements arrive in a list . The algorithm maintains:
gives ; here is a parameter;
With , the potential is with
where is the optimum number of sets covering the arrived elements, assumed known, and . The rounding rule: each time the weight of a set is augmented, is added to if this does not increase .
Every arriving element is covered by , and at every time
This is the paper's with the constant its proof gives.
The bound improves Alon et al.'s whenever sets are many but each element lies in few of them (), and whenever the optimum is large compared with . It also shows that the fractional part and the rounding part of an online covering algorithm can be designed separately: any online fractional solution with a competitive guarantee can be rounded deterministically by an online potential function. The same method gives the routing result of Section 5.2 of the paper.
As far as is known, none of these results is machine-checked. Related formal work on the platform covers Alon et al.'s algorithm and its bound (a different potential and a different fractional update), and the general covering scheme of Buchbinder and Naor's monograph; neither states Lemma 5.1 or Lemma 5.2, nor Theorem 3.2 for the scheme with in place of . A complete development here would give a verified derandomized rounding argument, reusable for other online covering problems.
The difficulty is not in the final inequality, which follows from in one line, but in keeping throughout. The decision to take a set must be made with no knowledge of future elements, and the potential has to account for elements that may never arrive: ranges over the whole ground set. Lemma 5.1 (ii) asks that, for every current state, one of the two decisions does not increase a non-linear function of all uncovered elements at once and this must hold for every state, not only for the states a particular run reaches. On the fractional side, Theorem 3.2 is only asserted, "along the same lines" as Theorem 3.1, so its constant has to be re-derived with in place of and with the scheme's continuous increase made discrete.
A tempting shortcut is to bound by the number of rounds or by directly; neither gives a logarithmic factor in , which comes only from the choice of in .
The instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance (elements E, set indices T, incidence elemSets, positive costs c), with elementWeight and coveredBy. Unit costs are the hypothesis ∀ s, inst.c s = 1 in Lemma 5.2; Theorem 3.2 is stated for general positive costs. Logarithms are natural (Real.log), because they invert Real.exp.
Committed conventions:
sInf) at which the new constraint holds. Arrival lists may repeat elements; an element already covered changes nothing.ord containing every set, and a set is added when . Lemma 5.2 holds for every order.Not in scope: the packing half of Theorem 3.2, Theorem 3.1 for general coefficients, and the doubling wrapper of p. 12 that removes the assumption that is known. The guarantee is for the algorithm run with the stated ; a formalization in which 's product ranges only over arrived elements, or in which the weights or the chosen family are free variables constrained by hypotheses instead of being produced by the algorithm ( is an input of the algorithm, as the page assumes it known), would be a different and weaker statement and is ruled out.
Contributions welcome: proofs of the three milestones and of the goal, and general lemmas about the fractional round (attainment of the least , monotonicity of the weights) that other online covering missions can reuse.
Alternating direction methods are used when one part of an optimization problem is easy to minimize and another part has a simple projection. Chapter 9 of Boyd, Parikh, Chu, Peleato and Eckstein (2011) examines this idea with nonconvex constraints. Its examples include sparse vectors, Boolean vectors and low-rank matrices. The chapter says explicitly that ADMM can fail to converge in this setting and that a limit need not be globally optimal. The useful claim here is narrower and concrete: several individual updates can still be computed exactly.
The capstone is factor-model fitting. A symmetric data matrix, such as an empirical covariance matrix, is approximated by a positive semidefinite matrix of prescribed rank plus a nonnegative diagonal matrix. This decomposition gives one component that captures shared variation and another that represents coordinate-specific variation. The chapter separates the diagonal fit from the rank constraint and writes the resulting ADMM X-update entry by entry. This mission formalizes that exact update and two other projection rules stated in the same chapter.
Fix a positive integer . Write for the real symmetric matrices, and let be the matrix to approximate. The Frobenius norm squares and sums every ordered matrix entry: . A vector is nonnegative when for every , and places those entries on a diagonal matrix. The book's reduced fitting loss is
In the scaled ADMM iteration, carries the positive semidefinite rank constraint and is the scaled dual matrix. Given the current symmetric matrices and a penalty , the X-step minimizes over . The X-step itself has no rank or positive semidefinite restriction. The following Z-step projects onto the chosen rank-constrained positive semidefinite set. The theorem here concerns the X-step, whose definition is independent of the chosen rank.
The other two results concern Euclidean projection of vectors . The cardinality is the number of nonzero coordinates of . The sparse set is for a nonnegative integer . The Boolean cube is . Projection means a nearest point in squared Euclidean distance; it may have more than one value when coordinates tie.
The first milestone identifies the book's infimum as the explicit componentwise loss and states that the optimizing diagonal is attained:
The sum over counts both and . The statement preserves that convention instead of treating a symmetric matrix as a list of independent upper-triangular entries.
The page 74 milestones say that retaining the entries of largest absolute value gives a nearest point in , and that rounding every coordinate to a nearest element of gives a nearest Boolean vector. They assert nearest-point status for ties without asserting uniqueness. These are chapter results on the same theme of exact nonconvex updates, although they are independent of the factor-model goal.
The goal identifies the unique symmetric minimizer of the X-subproblem. With , its off-diagonal and diagonal entries are
The target asserts both the formula and global minimality over symmetric matrices. It does not replace minimality with a stationarity condition.
The exact X-update separates the matrix fit from the nonconvex rank projection. It establishes that the factor-model algorithm's X-step is a well-defined, single-valued minimization for every symmetric current state and every positive penalty. It also makes the one-sided diagonal loss explicit: a nonnegative diagonal can absorb a shortfall below , but cannot absorb an excess. The two vector projections give similarly exact updates for sparse and Boolean constraint sets.
The mathematical claims are given in §9.1–9.1.2 of the published monograph; they are not open conjectures. The formalization work is to check the infimum, projection and unique-minimizer statements with every domain and tie convention explicit. The mission poses theorem statements for proofs; these draft statements themselves do not yet supply machine-checked proofs. A complete development can reuse its finite matrix loss and finite vector projection vocabulary in other splitting algorithms.
The diagonal partial minimization is one-sided, while the proximal penalty is symmetric around . An entrywise formula alone does not show that the assembled matrix minimizes the full objective or that it is the only minimizer. Symmetry also couples the two displayed off-diagonal positions and , so a scalar statement on one entry must agree with its transpose. For sparse projection, ties at the cutoff make a rule phrased as “the projection” ambiguous. For Boolean projection, the midpoint is a tie and requires a declared convention. These issues are part of the theorem statements, not numerical implementation details.
Matrices are Matrix (Fin n) (Fin n) ℝ; symmetry is an entrywise equality predicate. The factor-model statements assume , symmetric , and . The book uses at an iteration; the Lean theorem uses those current matrices as parameters and does not posit convergence of an ADMM sequence. The reduced loss is literally the infimum over all componentwise nonnegative , and the Frobenius square is the finite sum of entry squares. The stated X-minimization ranges over all symmetric matrices, with no positive semidefinite or rank hypothesis on .
For sparse vectors, the index set has size and its selected magnitudes dominate unselected ones. This covers , and cutoff ties. The Boolean rounding function chooses zero when an entry equals . The book uses indices ; Fin n uses . On page 75 the printed diagonal branch conditions omit the superscript on and ; the formalization uses the current that appear in the surrounding ADMM update. The theorem requires the candidate to minimize the book's reduced loss, preventing an arbitrary replacement loss from making the statement trivial.
The development needs finite-sum algebra, real infima with an attained lower bound, symmetry of matrices, and nearest-point arguments for finite vectors. The rank- singular-value projection on page 74 is already an open target elsewhere and is outside this mission. The positive semidefinite rank- eigenvalue projection on page 76 is also outside this goal; it would require a separate spectral development. Contributions that prove the three milestones or the goal against these definitions are in scope. The page also mentions rounding under integer constraints; this mission selects the preceding Boolean claim as its projection milestone.
The single-machine scheduling problem asks for an order in which to process jobs, each with a processing time and a weight, on one machine, respecting a partial order of precedence constraints, so that the weighted sum of completion times is as small as possible. It is NP-hard, and the best known approximation ratio for general precedence constraints is . Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) relate the problem to the dimension theory of partial orders: their Theorem 3.2 states that when the precedence constraints are given together with a realizer of size , the problem has a -approximation algorithm. Small realizers of structured precedence orders therefore translate directly into better approximation ratios.
This mission formalizes one such structural result, Lemma 4.1 of the paper: every convex bipartite order has a realizer of size . Convex bipartite orders form a class of precedence constraints that lies strictly between strong bipartite orders and general bipartite orders (Möhring, 1989). Combined with Theorem 3.2, the lemma gives a -approximation for on this class. According to the authors, the bound for convex bipartite orders had not been known before.
A poset is a set with a reflexive, antisymmetric, transitive relation . Two elements are incomparable, written , when neither nor ; the set of incomparable pairs is . A linear extension of is a linear order on with . A linear order reverses the pair when in . A realizer of size is a family of linear extensions of such that every incomparable pair is reversed by at least one . The dimension is the least for which a realizer of size exists.
A convex bipartite order has jobs split into minus jobs and plus jobs . Each plus job carries two indices , and a minus job precedes exactly when . There are no other precedences: the predecessors of each plus job form a nonempty interval of consecutive minus jobs.
For the Appendix construction, the incomparable pairs are sorted into three sets according to the kinds of the two jobs, the order of their indices and, for a pair (plus job , minus job ), whether precedes some plus job of larger index than . The sets describe what the -th linear order of the realizer must contain.
Equivalently, . The goal holds for every numbering of the jobs and every choice of interval ends .
The result. Lemma 4.1 places convex bipartite orders among the classes of precedence constraints for which has an approximation ratio strictly below , namely through Theorem 3.2 of the paper. The bound is tight: a bipartite order has dimension exactly when it is a strong bipartite order (Möhring), so the bound cannot be lowered for the class of convex bipartite orders. Since also gives for the graph of incomparable pairs, a -realizer yields an optimal colouring of that graph.
Formalizing it. The result is proved in the paper, with a short case analysis in the Appendix. No machine-checked proof is known to exist. Mathlib has no dimension theory of posets: realizers, reversals of incomparable pairs and the construction of linear extensions containing a given acyclic relation have to be set up here. The definitions of realizer and linear extension are stated for an arbitrary relation and can be reused for other dimension bounds (interval orders, semiorders, the other missions of this series).
The three relations are not partial orders. , for instance, is not transitive: with two minus jobs and one plus job with , the pairs and are present but lies in . The step that requires work is to show that each has no cycle, so that it extends to a linear order. For this depends on the convexity of the predecessor intervals and on the numbering of the plus jobs by their left ends: it is not a consequence of bipartiteness alone. The goal itself carries no numbering assumption, so any proof must also account for renumbering the plus jobs.
All declarations live in the namespace SingleMachinePrec.ConvexBipartite.
N → N → Prop. Linear orders use Mathlib's unbundled class IsLinearOrder. A linear extension of is a linear order with ; reverses when and . A realizer of size is a function Fin t → N → N → Prop, so repeated members are allowed, as in the paper's multisets.Fin a ⊕ Fin b: Sum.inl i is the minus job , Sum.inr k the plus job , with indices starting at . The interval ends are maps l r : Fin b → Fin a with l k ≤ r k, and is equality together with the pairs (minus , plus ) with . A file-level instance records that is a partial order. Any convex bipartite order in the paper's sense is one of these after naming its jobs. The cases and are allowed.Monotone l of this milestone only.A trivializing formalization would let the members of the realizer be arbitrary relations, which makes reversing every pair free. Here every member must be a linear order containing .
Contributions welcome: proofs of the two milestones and of the goal; a general lemma that a relation whose transitive closure is antisymmetric extends to a linear order on a finite type; and the renumbering argument that removes the numbering assumption.
Path-following interior point methods solve a linear program by tracking its central path, a smooth curve that runs through the interior of the feasible set and ends at an optimal solution. Their number of iterations is polynomial in the bit size of the input, and whether some interior point method is strongly polynomial (bounded by a polynomial in the number of variables and constraints alone) is open. Bayer and Lagarias called the central path "a fundamental mathematical object underlying Karmarkar's algorithm". Dedieu and Shub proposed its total curvature as an informal complexity measure: a path that turns little should be easy to follow with straight steps. Several results bound that curvature:
A linear program in slack form has a real matrix , , and :
For the point of the central path is the unique solution of
The primal central path is .
For and , the program minimizes over subject to
With slacks it becomes with , , .
For points of Euclidean space with , the turning angle is the angle between the vectors and . For a curve parameterized over , the total curvature is
The milestones also use the field of absolutely convergent generalized real Puiseux series . Such a series can be evaluated at large real , and it has a valuation , its leading exponent. Read over , is one linear program. The valuation of its central path at is the tropical central path , a piecewise-linear curve with an explicit recursive description (Propositions 20–21 of the paper).
For every and there is such that for all ,
for the central path of . Here may depend on and . Both the primal and the primal-dual curves are part of the goal, as in the paper.
The theorem shows that the total curvature of the central path is not bounded by any polynomial in the number of constraints: has constraints and curvature at least about . This settles the conjecture of Deza, Terlaky and Zinchenko in the negative. It also shows that the averaged upper bounds of Dedieu–Malajovich–Shub and De Loera–Sturmfels–Vinzant cannot hold for every region. A companion mission of this series formalizes the paper's second main result, an exponential lower bound on the number of iterations of log-barrier path-following methods on the same family.
The result is proved on paper. As far as is known, it has not been formalized in any proof assistant, and Mathlib has no notion of the total curvature of a curve, of Puiseux-series evaluation and valuation, or of the tropical central path. Formalizing the theorem would give a machine-checked reference point for a much-cited negative result in interior point theory. The Lean definitions of total curvature and of the turning angle are general and reusable.
The total curvature is a supremum over inscribed polygons, and a lower bound needs explicit polygons whose angles can be estimated for every large . The central path of has no closed form, so its points cannot be written down at given parameters . Numerical evidence at a fixed says nothing uniform in . The natural first idea, to compute the path's angles directly from system (1) for a fixed instance, gives no handle on how the number of turns grows with . What is needed is control of the path's geometry uniformly over the whole scale of , with turns located at once, and the threshold is not explicit.
Vectors in which angles are measured are EuclideanSpace ℝ (Fin d). The turning angle is InnerProductGeometry.angle (V - U) (W - V), not Mathlib's vertex angle ∠ U V W, which is minus it. A degenerate triple ( or ) contributes angle . Total curvature is an EReal-valued supremum over strictly increasing parameter sequences in the parameter set, and the goal uses the set . The primal and primal-dual curves are the vectors and . System (1) is the published Vanderbei central-path system with objective . The goal quantifies over every curve solving (1) for all . Existence and uniqueness of that curve is the referenced platform statement VanderbeiLP.CentralPath.central_path_exists_unique and is not posed again. Indices are the paper's, 1-based, mapped to Fin by subtracting one. Powers use integer exponents of the real number .
A trivializing formalization is ruled out explicitly: the curvature is a supremum in EReal (a real sSup of an unbounded set would be ), the turning angle is not the vertex angle, and degenerate polygons cannot add spurious right angles.
Lemmas 22–24 are stated over a model of by coefficient functions with the paper's support and absolute-convergence conditions. Equalities, products and order in are expressed through evaluation at all sufficiently large , which is how the paper characterizes them. Table 1 and the claims of the proof are stated for the explicit tropical central path of given by Propositions 20–21 (milestones of the companion mission), written as a definition here. One repair: the paper's "uniquely attained" claim fails at , , where . It is stated with that case excluded, which the proof does not use.
Welcome contributions: a general theory of total curvature of curves (monotonicity under refinement, behaviour under limits), asymptotics of evaluated Puiseux series, and the comparison between the central path over and its real specializations.
Single-machine scheduling with precedence constraints asks for an order in which one machine processes jobs while respecting prescribed comparisons between them. For the objective of minimizing total weighted completion time, the structure of the precedence order can influence the quality of approximation algorithms. Ambühl, Mastrolilli, Mutsanas, and Svensson connect one such approach to coloring a graph built from the order's incomparable pairs. A bounded number of colors would make a certain class of coloring-based guarantees uniform over the class of precedence orders. Their Theorem 4.3 shows that canonical interval orders have no such uniform bound for this particular graph. Ambühl et al., §4.2, p. 658
An interval order is a partial order whose elements can be represented by closed real intervals, with one element strictly before another when the first interval ends before the second begins. Interval orders are a familiar restriction of general precedence systems. The paper distinguishes them from semiorders, represented by intervals of equal length, for which it reports a three-element realizer bound and a corresponding scheduling guarantee. The chromatic obstruction here explains why that particular bounded-color route cannot be extended uniformly from semiorders to all interval orders. It does not assert that every scheduling approach to interval orders fails. Ambühl et al., §§3–4.2, pp. 656–658
For an integer , let be a linearly ordered set with points. The canonical interval order has one element for every pair of distinct points in , viewed as the closed interval . For two such intervals, write when or the right endpoint of is strictly less than the left endpoint of . Thus intervals that touch at an endpoint remain incomparable. The formalization represents each interval by its two-element endpoint set, and its order relation is equivalent to this endpoint rule. Ambühl et al., §4.2, p. 658
For any partial order on a ground set , an ordered incomparable pair is with neither nor . Both and are vertices when and are incomparable. A linear extension of is a linear order on the same elements that contains all comparisons of . It reverses if it places before . The graph has the ordered incomparable pairs as vertices. Two distinct vertices form an edge when no linear extension reverses both, while each singleton can be reversed by some linear extension. This singleton condition is the minimality clause in the paper's definition through its hypergraph of incomparable pairs. Ambühl et al., §2.1, p. 655, §3, p. 656
A proper -coloring assigns one of colors to every vertex of so that endpoints of an edge have different colors. The graph's chromatic number is the least positive number of colors that works, when the graph is nonempty. The mission uses the equivalent predicate that no proper map into a fixed -element color set exists once is large enough. This also gives a clear interpretation at .
The goal is Theorem 4.3: for each fixed integer , all sufficiently large canonical interval orders have incomparable-pairs graphs with chromatic number greater than . With , the Lean target is
The paper states as an integer. Its negative cases are immediate from nonnegativity of chromatic numbers; the target states the substantive range. The threshold may depend on , while and are constructed from rather than supplied as arbitrary objects. Ambühl et al., Theorem 4.3, p. 658
Two assertions from the theorem's proof serve as milestones. First, is nondecreasing as increases. Second, for four endpoints , the vertices and are adjacent in . They are recorded with their wording and provenance from §4.2. A separately published theorem on hypergraph Ramsey numbers is included as a reference because the source uses that theorem in its large- argument. Ambühl et al., proof of Theorem 4.3, p. 658
The result provides a precise structural limitation: across the canonical interval orders, the chromatic numbers of cannot be bounded by one constant. The graph is a specific graph of ordered incomparable pairs, distinct from other graphs that can be associated with a scheduling instance. Thus the conclusion addresses the bounded-color approach attached to this graph, without asserting an algorithmic impossibility for interval-order scheduling. The paper contrasts this limitation with the bounded-realizer situation for semiorders. Ambühl et al., §§3–4.2, pp. 656–658
The theorem is proved in the 2011 paper. The remaining work in this mission is a machine-checked development of its definition layer, its two stated supporting assertions, and the unbounded-color conclusion. The partial-order property of is already proved in the definition file; the three theorem statements are open proof targets in the proposal. A completed formalization would also give reusable components for finite interval orders, ordered incomparable pairs, and coloring arguments in dimension theory.
A pair of intervals overlapping or touching is easy to recognize as incomparable, but graph adjacency has a stronger meaning: it quantifies over every linear extension of the entire partial order. A local test based only on the four displayed intervals would silently change the graph. Likewise, the fact that two vertices have different endpoint descriptions does not by itself make them adjacent. The formal argument must connect the canonical interval representation to the global extension-based edge condition, then show that a bounded coloring cannot persist as the endpoint set grows. Ambühl et al., proof of Theorem 4.3, p. 658
The endpoint set is Fin n, hence indexed rather than the paper's ; the shift preserves order. Elements of are exactly two-element subsets of this set. The order relation includes equality and strict separation of endpoint sets and is proved to be a partial order. The graph is defined for an arbitrary binary relation so it can be reused, but every target here applies it to the concrete partial order . Vertices are ordered incomparable pairs, and adjacency retains both singleton reversibility and failure of simultaneous reversibility. Defining adjacency directly from the desired four-point pattern would trivialize the target and is excluded.
Colorable n k means existence of a proper function from all vertices of to Fin k. For an empty graph, zero-colorability is allowed by this representation. The theorem therefore includes a threshold and quantifies over every ; the assertion itself forces the threshold past any empty-graph exceptions. The formal target uses natural ; the paper's negative integer values need no separate theorem. No asymptotic notation or unspecified constants occur. The source's Ramsey number is not hard-coded into the goal, because the source asserts existence of a suitable threshold, not that the least threshold equals that value.
The printed adjacency justification names an alternating-cycle pair set different from the two adjacent vertices in the preceding sentence. The milestone formalizes the adjacency assertion itself and records the printed explanation verbatim for review; it does not turn the mismatched pair set into a hypothesis. The mission needs finite order embeddings, linear extensions, graph colorings, and a finite Ramsey theorem. The existing published Ramsey theorem is referenced as a reusable result. No scheduling approximation algorithm, polynomial-time statement, or numerical scheduling guarantee is formalized in this mission.
Expected utility theory explains a single attitude toward risk by the curvature of a utility function of final wealth: a concave utility makes a decision maker risk averse, a convex one risk seeking. Several well documented patterns of behaviour do not fit this picture. The same people buy insurance against small-probability losses and buy lottery tickets with small-probability gains (Friedman and Savage, 1948, doi:10.1086/256692); subjects who are risk averse for gains are risk seeking for the mirrored losses, the reflection effect; and subjects who are indifferent between full insurance and bearing a risk reject half-price insurance that pays only half the time, probabilistic insurance (Kahneman and Tversky, 1979, doi:10.2307/1914185).
David E. Bell's 1982 paper Regret in Decision Making under Uncertainty (doi:10.1287/opre.30.5.961) proposes that a decision maker cares not only about what she obtains but also about what she would have obtained had she chosen differently. Its first part (the companion mission of this series) derives the representation ; its Section 2 shows that the single additive form with linear explains all of the patterns above at once, provided the regret function is decreasingly concave. Regret theory, developed at the same time by Loomes and Sugden (1982, doi:10.2307/2232669), remains one of the standard alternatives to expected utility in decision analysis and behavioural economics.
A decision maker chooses between two alternatives and . Uncertainty is described by finitely many states with probabilities ; in state alternative gives final assets and gives . Choosing means forgoing , and an outcome is valued by the regret utility
where is the final assets received, the assets the foregone alternative would have given in the same state, and the regret function. The expected utility of selecting when is foregone is
and is strictly preferred to when (the paper's inequality (1)); and are indifferent when the two expected utilities are equal.
The comparisons are given by three payoff tables. Table II: a horse wins with probability ; betting \p1-p-p0p1-p-10q-10-p-p-1-p/2$.
The regret function is decreasingly concave if it is twice differentiable with strictly increasing second derivative . Section 3 also uses and the negative exponential , .
If is decreasingly concave and , then the bet of Table II is strictly preferred to not betting and insuring in Table III is strictly preferred to not insuring:
Both comparisons have equal expected values, so the statement is a pure regret effect. The goal fixes no constants and assumes nothing about beyond decreasing concavity; it is the weakest hypothesis the page offers.
holds iff full insurance is strictly preferred to probabilistic insurance, iff probabilistic insurance is strictly preferred to self insurance; and (11) follows from the same ratio condition. 5. The negative exponential (Sec. 3): concave, convex on , strictly increasing on , and decreasingly concave.
The goal is the paper's central behavioural claim: one regret function explains why the same decision maker gambles on long odds and buys insurance at fair prices, behaviour that a single concave or convex utility of wealth cannot produce. The milestones show that the reflection effect and the rejection of probabilistic insurance follow from the same model, and two of them reduce to the same inequality on the odd part of the regret function. The negative exponential example shows the hypotheses are met by a concrete, commonly used function, so the explanation is not vacuous.
The results are proved in the paper by short calculations, and none of them has been machine-checked before. The mission produces a formal statement of the regret model of Section 2 with its payoff tables, which pins down several points the printed text leaves loose: the meaning of "decreasingly concave", the domain on which "increasing" and "convex" are meant, and three misprinted intermediate displays.
The comparisons (5), (6), (9) and the reflection identity are algebraic once the payoff tables are expanded; the work is in expanding them correctly, since the foregone argument of changes with the alternative selected and three printed expansions are wrong. The substance lies in the analytic step: passing from a pointwise condition on to strict monotonicity of on , with strict inequalities throughout and through a quotient that is undefined at . The naive reading of the page's condition, " for all ", is unsatisfiable and cannot be used as a hypothesis.
All quantities are real numbers. The utility is regretU f x y = x + f (x - y), i.e. form (4) with exactly; the page assumes only "approximately linear" but computes every display with . A comparison is a finite state space Fin n with a real weight vector; the theorems instantiate it with for Tables II–III and with for Table IV, the accident state split by whether the insurer pays. Strict preference is strict inequality of expected regret utilities; indifference is equality.
Conventions and corrections, each disclosed in the item concerned:
Differentiable ℝ f, Differentiable ℝ (deriv f) and StrictMono (deriv (deriv f)). The page's presumption that is increasing and concave is not assumed.The goal cannot be satisfied vacuously: the negative exponential milestone exhibits a decreasingly concave , and the conclusion is a strict preference between two alternatives of equal expected value. Section 2(iv) (preference reversals) is not formalized: its printed rewriting of (12) in terms of drops a linear term and its conclusion is unquantified ("for sufficiently small units of money").
Contributions welcome: proofs of the algebraic reductions, the slope argument for , and the convexity facts for ; the latter two are reusable beyond this mission.
Many planning problems are made in two stages: a first decision is fixed before an uncertain parameter is revealed, and a second decision is taken afterwards. Two models compete for such problems. Two-stage stochastic optimization assumes a probability distribution over the scenarios and minimizes the expected cost, letting the second-stage decision depend on the scenario. Robust optimization asks for one solution that is feasible in every scenario and minimizes the worst-case cost. The robust problem is usually far easier to solve: it is a single deterministic problem, while the stochastic problem optimizes over policies. The question is how much cost one gives up by solving the easy problem instead of the hard one.
Bertsimas and Goyal (Math. Oper. Res. 2010) measure this loss by the stochasticity gap, the ratio of the robust optimum to the stochastic optimum. Their Theorem 2.1 shows that when only the right-hand side of the constraints is uncertain, the uncertainty set is symmetric and the distribution is centred at the point of symmetry, the robust optimum is at most twice the stochastic one. Section 3 asks whether the same holds when the second-stage costs are uncertain as well, and answers no with an explicit instance: Theorem 3.1. This mission formalizes that instance.
There are no first-stage variables. The second-stage decision is a vector with continuous coordinates, subject to the single covering constraint
the constraint with and . A set of scenarios carries a cost map ; in scenario the second-stage cost is . The uncertainty set is , here : the range of is the whole cube . A probability measure on makes the coordinates independent, each uniformly distributed on .
The stochastic problem , display (1.4) of the paper, chooses a policy satisfying the constraint in every scenario and minimizes ; its optimal value is . The robust problem , display (1.5), chooses one satisfying the constraint and minimizes ; its optimal value is . A set is symmetric (Definition 1.2) if there is with for every .
The Lean development names these zStochBD and zRobBD (the general problems (1.4) and (1.5) with data , , , , and integer coordinate sets), and IsSymmetricAbout (Definition 1.2).
The constant is the paper's. Both sides are pinned down separately by the milestones, so the goal cannot be satisfied by a degenerate value of either side.
Theorem 3.1 marks the boundary of the paper's positive results. The bound of Theorem 2.1 needs only symmetry of the uncertainty set and a centred distribution. The instance here has both, has no integer variables and a single constraint, and still has a gap that grows linearly in the dimension. So symmetry alone does not make a robust solution a good approximation of the stochastic optimum when costs are uncertain. The paper's abstract states this as one of its main conclusions, and it is why Sections 4 and 5 compare the robust problem with the adaptive problem, whose worst-case objective does not suffer from it.
The result is proved in the paper; to our knowledge it has no machine-checked proof. What this mission adds is a formal proof of the instance against the general definitions of the two-stage problems, including the probabilistic computation (3.2), the expected minimum of independent uniform random variables, which Mathlib does not contain. That computation is reusable wherever order statistics of uniforms appear, for example in auctions, secretary problems and random-assignment bounds.
The robust half is short. The stochastic half has two parts. Eq. (3.1) needs a measurable policy that selects a cheapest coordinate; the policy printed in the paper puts a unit on every minimizing coordinate, which at ties overpays, so a formal proof must choose a single minimizer measurably and use integrability on the probability space. Eq. (3.2) is the main work: it is a genuine integral over the -dimensional cube against a product measure, for every , and Mathlib has no lemma on the distribution or the expectation of the minimum of independent random variables.
Fin k → ℝ with the componentwise order; is the all-ones Matrix (Fin 1) (Fin n) ℝ, and live on Fin 0, , and the integer coordinate sets are empty ().EReal, when infeasible; the robust worst-case cost is an EReal supremum. No optimal solution is assumed to exist: the paper's "consider an optimal solution" is a proof device, and the statements are about the infima.A real-valued infimum would assign the value to an infeasible or ill-posed problem and make the goal trivially true; the EReal infima, and the separate milestones fixing and , rule that out.
Contributions are welcome on each milestone separately. The expected-minimum computation (3.2) is self-contained and of independent use; a general lemma on the law of the minimum of independent random variables would serve it and other missions.
Expected utility theory predicts that a decision maker's choice between two lotteries depends only on the distribution of final wealth under each. Observed behaviour contradicts this in systematic ways: the Allais paradox, the coexistence of insurance and gambling, and the reflection effect documented by Kahneman and Tversky (1979). David Bell's 1982 paper (Operations Research 30(5), 961–981) explains these patterns by regret: the dissatisfaction of learning that the alternative not chosen would have done better. In the same year Loomes and Sugden (1982) proposed a closely related theory; together the two papers are the origin of regret theory in decision analysis.
Bell's contribution is axiomatic. Instead of postulating a regret term, he derives the shape of a utility function that incorporates regret from three behavioural assumptions about how preferences respond to shifting all outcomes by an equal increment of value. This mission formalizes that derivation, Section 1 of the paper (pp. 965–970), culminating in Theorem 1.
An endpoint is described by two attributes: the final assets and the foregone assets , the asset level the decision maker would have had under the alternative not chosen. Utility is a function , strictly increasing in and strictly decreasing in .
A simple comparison is a choice between two alternatives whose uncertainties are resolved by one predetermined joint distribution. With states, a probability vector and alternatives ( the final assets of in state ), the expected utility of selecting while is foregone is
and is preferred to when (inequality (1) of the paper).
A value function , strictly increasing and onto , measures incremental value: moving from to is worth . An alternative is obtained from by a shift of incremental value if for every state.
Under Assumptions 2 and 3, there are a constant and a function with
Utility separates additively into a term in the value of final assets and a function of the regret . The coefficient is left free (see Formalization scope).
The additive form is the basis of the rest of Bell's paper: Section 2 uses it to show that a single decision maker with decreasingly concave both buys fair insurance and takes long-odds bets, and to account for the Allais paradox and the reflection effect. The same additive structure, a value term plus a function of the regret difference, is the form in which regret theory has been used since, alongside the parallel proposal of Loomes and Sugden (1982). Lemmas 1 and 2 have independent content: simple comparisons identify only the antisymmetric part , and the lemmas pin that part down to a function of the regret difference.
The results are published with proofs in prose; none has a machine-checked proof. Formalizing them checks the argument as printed, which turns out to need a correction (the coefficient of in (4)), and fills in the regularity steps the paper leaves implicit: the solutions of the Cauchy equations that appear, and the passage from to a general value function.
The obvious argument reads each assumption as a functional equation and solves it. Two steps resist this. First, the functional equations and have non-measurable solutions; excluding them needs boundedness of and on intervals, which must be extracted from the monotonicity of and is never stated on the page. Second, the proof of Theorem 1 compares two 50-50 lotteries that are indifferent and requires to take an arbitrary value ; when is bounded no such indifference exists, so the printed step does not cover every case. Passing from to a general requires transporting all three assumptions along .
u : ℝ → ℝ → ℝ with u x y . Every theorem assumes strictly increasing in and strictly decreasing in (the paper's "increasing"/"decreasing", p. 965, read strictly).Fin n and two alternatives on the same states. Assumption 3 quantifies over four alternatives on one common state space, the setting of the paper's own use of it.Online bipartite matching models a platform that must commit each arriving request to a resource immediately. The motivating application of Feldman, Mehta, Mirrokni and Muthukrishnan is display advertising: an ad server knows from past traffic how many impressions of each type (web page, audience segment) to expect, sells them to advertisers in advance, and must assign each impression to an interested advertiser the moment a user loads the page. The goal is to fill as many contracted impressions as possible.
When arrivals are chosen by an adversary, the best ratio an online algorithm can guarantee is , achieved by the RANKING algorithm of Karp, Vazirani and Vazirani (STOC 1990). The ad server, however, is not facing an adversary: it has a forecast. The i.i.d. model captures this: the graph and the distribution of impression types are known in advance, and the impressions are independent draws. The paper asks whether this knowledge allows an online algorithm to beat , and answers yes.
Timeline.
An instance is a bipartite graph with a finite set of advertisers, a finite set of impression types, and edges recording which advertisers want which types. The mission treats the case analysed throughout §4.2 of the paper, in which one impression of each type is expected (). So impressions arrive one at a time, with types drawn independently and uniformly from . On arrival an impression must be assigned at once and irrevocably to a still unassigned advertiser adjacent to its type, or discarded. is the number of impressions an algorithm assigns. is the size of a maximum matching of the realization graph, which has one node per arrival , joined to every advertiser with .
The two suggested matchings (TSM) algorithm works offline first. Its boosted flow graph has a source arc of capacity into every advertiser, a unit-capacity arc along every edge of , and an arc of capacity from every type to a sink. The algorithm takes the edge set of an integral maximum flow. Every vertex then has at most two edges of , so splits into vertex-disjoint paths and cycles. The algorithm colours each component blue and red:
Online, the first arrival of type tries the advertiser along 's blue edge, the second tries the one along its red edge, and later arrivals are discarded. A tried advertiser that is already taken is not reassigned. The advertisers fall into four classes by their coloured edges: (one blue, one red), (two blue), (one blue only) and (one red only).
Let
The goal has three parts. First, every maximum flow edge set admits a colouring that follows the rules. Second, for every and there are and such that, for every instance with , every maximum flow edge set and every rule-following colouring,
Third, .
The theorem separates the i.i.d. model from the adversarial one: knowing the distribution is worth a constant factor above . The suggested matching algorithm of the same paper (Theorem 4) shows that following a single offline matching gets exactly , so the second, red matching is what crosses the barrier. The paper's question started a line of work on the i.i.d. and random-order models, with later improvements to the constant by other authors under further assumptions.
The result has a written proof but, as far as the platform record shows, no machine-checked one. The mission formalizes the paper's own argument: the flow-and-colouring construction, the balls-in-bins concentration facts, the cut-based bound on OPT and the combinatorial Lemma 1. It also fixes two slips in the printed statements (see Formalization scope). The pieces are reusable beyond this paper. The occupancy concentration (Fact 1) and the satisfied-sequences bound (Fact 2) recur in analyses of online algorithms with stochastic input. The degree-capped flow encoding and its path/cycle decomposition are standard tools for 2-matchings.
The upper bound on OPT is the delicate part. A cut of the flow graph bounds the maximum matching of the realization graph only after a second surgery that depends on the random arrivals. Its size must then be compared with the colour classes, which are defined by a different structure (the components of ). Lemma 1 bridges the two, and it depends on the exact colouring rules: a colouring that only satisfies local degree conditions can put red edges at both ends of an even advertiser path, which breaks the inequality behind (2). On the probabilistic side, the advertisers of share impression types with each other, so the success events are dependent, and Fact 2 needs a bounded-differences argument in which one ball affects up to sequences.
All declarations live in the namespace OnlineStochMatching.TSM. Advertisers and types are finite types A I : Type, and is a Finset (A × I). Probabilities are counting ratios , so there are no measurability side conditions. OPT is a maximum over the finite, nonempty set of partial injective assignments. An integral flow of is its set of saturated middle edges, i.e. a subset of with at most two edges per vertex; is such a set of maximum cardinality. A colouring is given by a listing of the components of as vertex sequences. Every theorem quantifies over every maximum and every colouring the rules allow, since the paper fixes neither.
The paper's asymptotic phrases are replaced by explicit quantifiers that come from its own proofs:
Corrections to the printed statements:
The ratio is multiplied out, so no division by OPT occurs. A colouring condition that is unsatisfiable, or a flow set that is not maximum, would make the goal vacuous or false; part (a) of the goal rules out the first, and every statement requires maximality. Not included: the reduction to general integer (§4.2.4), the tightness sentence of Theorem 5 (§4.2.5), and footnote 7's variant of the algorithm.
Useful infrastructure: bounded-differences (McDiarmid/Azuma) inequalities for functions of i.i.d. uniform variables, which exist on the platform as separate theorems; path/cycle decomposition of graphs of maximum degree two; and max-flow min-cut for unit-capacity bipartite networks. Contributions are welcome on Facts 1 and 2 independently of the combinatorics, and on Lemma 1 and equations (1) and (3), which are deterministic.
A retailer that groups its products into categories (brands, store sections, flight classes) and decides which products to display in each faces the assortment problem: offering more products attracts more customers but also diverts sales away from the most profitable products. The nested logit model is the standard description of customer choice in this setting. A customer first selects a category (a nest), then a product within it. Choice-based models of this kind are the basis of revenue management under customer choice (Talluri and van Ryzin 2004).
Davis, Gallego and Topaloglu (DGT 2014) study the assortment problem under the nested logit model with two features that earlier work excluded: dissimilarity parameters larger than one, under which products in a nest act as complements rather than substitutes, and a no-purchase option inside each nest, under which a customer may enter a nest and still leave without buying. They show that the problem is NP-hard once either feature is present. For each regime they give a small linear program whose solution yields an assortment with a provable performance guarantee. This mission formalizes the guarantee for the most general instances, where both features occur together (§6.1, Theorem 11).
Timeline. Rusmevichientong, Shmoys and Topaloglu (2010) bound nested-by-revenue assortments under a multinomial logit mixture. [DGT 2014] prove that nested-by-revenue assortments are optimal for dissimilarity parameters at most one without within-nest no-purchase options (Theorem 4). They give factor-(6) guarantees with synergistic products, a factor-two guarantee via knapsack relaxations for partially-captured nests (Theorem 10), and the general factor (12) of Theorem 11. Li, Rusmevichientong and Topaloglu (2015) extend the nested-by-revenue result to -level nested logit models.
There are nests and, in each nest, products . Product of nest has revenue and preference weight , with . Nest has a no-purchase weight and a dissimilarity parameter , and is the weight of choosing no nest at all. For an assortment ,
A customer chooses nest with probability , and the expected revenue is
The optimal value of equals the optimal value of the linear program
which has constraints per nest. Problem (4) keeps only the constraints for a chosen candidate collection of assortments in each nest.
A nest is fully captured if () and partially captured if (). is the nested-by-revenue assortment. is the set of the highest-revenue products among the products of nest with the smallest preference weights, with and .
Let be an optimal solution of (4) when the candidate collection of every nest is , and let
Then is feasible for problem (3).
The theorem assumes , as all of §6 does. Otherwise it places no restriction on the or the .
Two companions follow the goal. One is the resulting guarantee , through Theorem 1. The other is the bound when the preference weights within a nest differ by at most a factor (p. 26).
Theorem 11, combined with Theorem 1 of the paper, gives a polynomial-size method for an NP-hard problem. The method solves one linear program with variables and constraints, then reads off an assortment whose expected revenue is within the factor of the optimum. This holds for every nested logit instance, including nests where customers may walk away and nests whose products are complements. When the weights inside each nest are within a factor of each other, the guarantee is at most .
The theorem is proved in the paper's appendix. No part of it is machine-checked. Formalizing it checks a case analysis that reuses, by reference, arguments from two other theorems: Theorem 7 (synergistic, fully-captured nests) and Theorem 10 (competitive, partially-captured nests). It makes precise what these arguments need when the two regimes are mixed in one instance. The formalization also fixes the boundary conventions the printed proof leaves implicit: fully-captured nests with , zero-weight denominators, and the sign of .
Each nest falls into one of three regimes, and a different argument controls each. With the nest behaves like a knapsack problem. Its guarantee of two needs the knapsack collection of §5 to sit inside . With and , the constraint must be extended from nested-by-revenue sets to every subset. This goes through a continuous relaxation whose optimum has a fractional coordinate, and it costs the ratio , which is where (12) comes from. With and , the scaling argument of Case 1 fails because multiplying by a factor at most one no longer preserves the inequality. The proof switches to the different objective (31), whose convexity in one coordinate forces an integral optimum.
The first idea, bounding every assortment by a nested-by-revenue one, is false here. With or , nested-by-revenue assortments are not optimal, and the loss is exactly the factor .
Products are Fin n; is nbr n j. Powers are Real.rpow, and , so . Problems (3) and (4) are stated in constraint form: LP4Optimal means feasible and with minimal among feasible points. is the greatest element of the finite set betaSet I, which contains and the ratios of (12). Fully-captured nests skip , as on the page. The collection is constructed: nestedPR breaks weight ties by index and revenue ties by index.
Standing assumptions, all disclosed:
A trivializing formalization is ruled out. The goal states only feasibility for (3), with the maximum of (12), not any upper bound. The collection is the page's, not an arbitrary family containing it. The goal mentions none of the cases or the relaxations.
A complete development needs continuous knapsack solutions (greedy optimality, fractional prefixes), convexity of on , and the factor-two argument of Theorem 10. The knapsack and fractional-prefix lemmas are reusable for the companion missions of this series. Proofs of individual cases, and proofs of milestones in greater generality, are welcome.
A processing network must decide which activities receive scarce processor capacity while jobs move among buffers. Such decisions matter in manufacturing, service systems, and switches: one activity can consume several processors at once, and a job can be routed to another buffer after processing. A policy that sees current buffer levels but does not need to know arrival or routing rates is easier to operate when those rates are difficult to estimate. Dai and Lin's 2005 paper studies whether a maximum pressure policy, which uses the buffer vector and an input-output matrix, can stabilize every network that is stabilizable in their model. Their Theorems 1 and 2 give, respectively, a necessary planning condition for any stabilizing policy and a sufficient condition for maximum pressure under the extreme-allocation-available assumption. Dai and Lin (2005)
Here pathwise stability means that each internal buffer grows sublinearly in time almost surely. This is a rate statement about sample paths. It does not assert positive recurrence of a Markov chain, nor does it require a stationary distribution. The paper allows general primitive processing and routing processes with almost-sure long-run averages. Dai and Lin (2005), §§2–4
There are internal buffers, activities, and processors. Buffer represents the outside world. The matrix records resource use: when activity requires processor . The matrix records which buffers an activity processes. An input activity processes Buffer ; a service activity does not. Input processors serve only input activities and must be fully used, while all processors have at most unit capacity.
For activity , the processing requirements have mean and the routing counts have long-run matrix . Write . The input-output matrix is
Positive means activity consumes net material from internal buffer ; negative means it produces net material there. An allocation assigns nonnegative activity levels subject to the processor capacity bounds and the equality for every input processor. The finite set consists of the extreme points of this allocation set. At buffer vector , allocation has network pressure . The maximum pressure rule chooses an allocation of greatest pressure among the currently feasible members of . Feasibility depends on jobs actually available to each constituent buffer. Dai and Lin (2005), §§2–3
The extreme-allocation-available assumption (EAA) says that for every nonnegative , a pressure maximizer in can be chosen whose constituent buffers all have positive levels. It links the static pressure maximization to the jobs that a policy can process. The static planning LP asks for activity fractions and a service-processor load such that , every input processor has load one, and every service processor has load at most . Dai and Lin (2005), p. 202
The goal is Theorem 2. For a network satisfying EAA and run by a preemptive, processor-splitting maximum pressure policy, LP feasibility with implies
The milestones follow the paper's route from stochastic paths to deterministic fluid limits. A fluid limit is a uniform-on-compact limit of along positive scales . The milestones state that fluid limits satisfy (14)–(18), weak stability of the corresponding fluid model transfers to pathwise stability (Theorem 3), maximum pressure adds (52)–(55) and (20) (Lemmas 5 and 4), quadratic fluid energy obeys (22)–(23), and LP feasibility with EAA makes the maximum-pressure fluid model weakly stable (Theorem 4). Dai and Lin (2005), pp. 203, 213–214
Theorem 2 identifies a policy whose almost-sure buffer growth rate vanishes whenever the planning LP permits load at most one and EAA holds. Together with the paper's necessary condition in Theorem 1, it characterizes the feasibility boundary for this policy class under EAA. Its scope includes networks in which an activity uses multiple processors and processes multiple buffers simultaneously. It does not claim that all such networks satisfy EAA. Dai and Lin (2005), Theorems 1–2
The result is proved in the 2005 article. This mission asks for a machine-checked proof of that known theorem and its selected intermediate claims. The Lean statements are open draft targets. Reusable outcomes include a model of cumulative routing and service counts, a uniform-on-compact fluid-limit interface, and the weak-fluid-stability transfer theorem for networks without a Markov assumption.
Maximizing pressure over the static allocation polytope does not by itself describe an executable service policy. An allocation can demand work from an empty buffer. EAA addresses the existence of a maximizing allocation supported by positive buffer levels, but the stochastic policy acts on actual jobs and completion times. The proof must connect those discrete, pathwise decisions to the limiting differential equation (20). At a regular fluid time, the maximum-pressure equation is decisive; away from regular times, derivatives need not exist. The fluid model therefore carries a time qualifier that cannot simply be dropped. Dai and Lin (2005), pp. 201–203, 214
The Lean model uses finite index types for buffers, activities, and processors. Internal buffers are Fin I; Buffer 0 is the zero index of Fin (I+1), and an internal buffer maps to its successor index. Activity and processor labels use zero-based Fin. Time is real but all network equations are asserted for nonnegative time. The shared Bell–Williams Paths definition supplies the renewal count in and uniform-on-compact distance using the norm. The completion count is required finite wherever the network equations convert it to a natural number; this prevents infinity from becoming a zero count. Bell and Williams (2001)
The network standing assumptions record binary incidence matrices, nonempty constituencies, processor coverage, activity types, and an input activity. Two refinements are explicit: each input processor has an activity, so its mandatory unit allocation is feasible, and , so is defined as the intended positive rate. Routing counts are cumulative and nonnegative. Their row sums are constrained only for buffers an activity processes: the printed sentence requiring the same sum for every buffer conflicts with its immediately preceding statement that the count vanishes when the activity does not process that buffer. The corresponding rows of sum to one for processed buffers and vanish for unprocessed buffers, as follows from (4). Dai and Lin (2005), pp. 199–200
The policy predicate records allocation-time decomposition (49)–(51) and the non-employment consequence of Definition 1 used in (56)–(58). It checks feasibility of a competing extreme allocation through the paper's threshold at every time of the interval. Individual job states and tie breaking are outside the pathwise interface. The goal retains EAA, the exact bound, and all network and policy equations, so an empty allocation set or an unconstrained service path cannot make the target automatic. Contributions formalizing the finite extreme-point set, fluid-limit compactness, Lemmas 4–5, and the weak-stability transfer are welcome.
Infinite-horizon dynamic programs, including discounted Markov decision processes, stochastic games and semi-Markov models, are usually analysed through a single equation: the optimal return solves the optimality equation , where maximizes the one-step return over decisions. Denardo's 1967 paper (SIAM Review 9(2), 165–177) separated the argument from the particular model. It isolated two properties of an abstract return , contraction and monotonicity, and showed that the standard conclusions follow from them alone. The examples of §8 of the paper cover Howard's discounted model, Shapley's stochastic games and Blackwell's, Jewell's and Fox's models.
The plain contraction assumption (each one-step operator shrinks distances by a factor ) fails in models where the process stops only from a subset of states, or where discounting acts only after several transitions. §5 of the paper handles these with the N-stage contraction assumption: only steps of a policy need to contract, while one step only needs to be nonexpansive. This mission formalizes that section. Its companion mission (part 1 of the series) formalizes the plain contraction case.
Timeline:
Let be a set of points. Each point has a decision set . A policy picks a decision at every point, so the policy space is . Let be the bounded real functions on with the metric ; is complete. Write when for every .
The return assigns a real number to each point , decision and . It defines two kinds of operators on :
and both are assumed to map into . An operator on has modulus or less when for all .
Under these assumptions is a contraction, so it has a unique fixed point , the return function of . The optimal return is . The auxiliary operator is .
Under the monotonicity and N-stage contraction assumptions:
The mission also contains two consequences that are not milestones: is optimal for the mathematical programs s.t. and s.t. (§6, p. 171), and a policy is optimal exactly when it attains at every point (§7, p. 173).
Theorem 4 lets models whose one-step operators are not contractions use the contraction-mapping theory of dynamic programming. Under its hypotheses the optimality equation has exactly one bounded solution, and that solution is the optimal return. Successive approximation converges geometrically from below (part (e)). Lemma 2 shows that is the least with and the greatest with . This gives the linear-programming formulation of finite Markov decision processes (Program I) and the policy-improvement argument of §6. The characterization reduces the search for optimal policies to the decisions that attain the maximum in the optimality equation.
The results are proved in the paper. The work of this mission is to formalize them, in the abstract form that Mathlib does not have: monotone operators on bounded functions that are contractive only after steps, with suprema taken over arbitrary, possibly infinite, decision and policy sets. No machine-checked proof of Theorem 4 or of Lemma 2 is known. The closest formal statements, Propositions 4.1–4.2 of Bertsekas and Shreve under their Assumption C, concern a different model (extended-real costs, nonstationary policies) and are themselves unproved formally.
The obvious argument would apply the Banach fixed-point theorem to . That does not work: under the N-stage assumption, need not be a contraction. The paper gives an example (p. 170) with , , where has modulus for every . The supremum over decisions does not commute with composition, so the contraction of each says nothing directly about . The paper therefore works through the auxiliary operator , which is a contraction. The hard step is to show that , the supremum of the policy returns, is a fixed point of . This is the second half of Lemma 2(a), an -argument that uses both monotonicity and the modulus- bound on .
Part (e) holds only for . It is not a contraction property of on all of .
lp (fun _ : Ω => ℝ) ⊤ (as BFun Ω), and its dist is . The order is pointwise (PLe).IsPolicyOperator, IsMaxOperator and IsNStageSupOperator. Every supremum, including (IsOptimalReturn), is a genuine least upper bound (IsLUB). sSup/⨆ are never used, so no junk value can make a statement trivial.ModulusLE B c. NStageContractionAssumption H N c holds , , ModulusLE (H δ)^[N] c and ModulusLE (H δ) 1, with and independent of .v with , the paper's §5 definition. is the conclusion (a), never a hypothesis.IsNStageSupOperator H N E. The milestone Theorem 4 (a)–(c) proves that such an operator exists. is never defined as a fixed point of or . The goal asserts that the pointwise least upper bound of exists in and is the unique fixed point of both.A complete development needs the Banach fixed-point theorem for iterates (Mathlib's ContractingWith, applied to ), suprema of families of real numbers, and induction on iterates. The §3 observation and Lemma 1 are reusable for any monotone operator family on bounded functions. Contributions to every milestone and to the two §6–§7 consequences are welcome.
A stochastic processing network (Harrison 2000) models a system in which processors carry out activities and each activity draws jobs from one or more buffers. Manufacturing lines, call centers with cross-trained agents, and data switches all fit this model. A central question is which scheduling policies are throughput optimal, meaning they stabilize the network whenever any policy can.
Dai and Lin (Oper. Res. 53(2), 2005) show that maximum pressure policies are throughput optimal. These policies generalize the back-pressure rule of Tassiulas and Ephremides (1992) for wireless and switch networks, and at each moment they choose the allocation that maximizes a linear "network pressure". Their main theorem (Theorem 2) has one structural hypothesis, the extreme-allocation-available (EAA) assumption (Assumption 1). It holds for many familiar networks and fails for some (§6.2 gives a counterexample). Theorem 6 identifies a broad class where it always holds: strict Leontief networks, in the sense of Bramson and Williams (2003). This mission formalizes that theorem.
A network has internal buffers , an outside Buffer , activities and processors .
The input-output matrix is
An allocation gives the level at which each activity runs. The allocation set consists of the allocations with for every processor and for every input processor. Write for the set of its extreme points, the extreme allocations. For a buffer-level vector the network pressure is . Buffer is a constituent buffer of if .
Assumption 1 (EAA). For every there is with such that for every constituent buffer of .
A network is strict Leontief if every service activity has exactly one buffer in its constituency, denoted .
The result. Theorem 2 of the paper states that, under EAA, a maximum pressure policy is pathwise stable whenever the static planning problem has a feasible solution with . Theorem 6 removes the EAA hypothesis for strict Leontief networks. In that class maximum pressure is therefore throughput optimal with no further structural condition. The class includes multiclass queueing networks with alternate routes and networks of input-queued data switches (§9), so Theorem 6 is the step that turns the abstract main theorem into a statement about these concrete systems.
Formalizing it. The theorem is proved in the paper and, to our knowledge, has no machine-checked proof. Formalizing it fixes the exact standing assumptions of the model, several of which the paper uses without stating (see below). It also yields a reusable Lean vocabulary for stochastic processing networks with input activities: from (5), the allocation polytope with the input-processor equality (2), extreme allocations, network pressure and EAA. The companion missions of this series on maximum pressure policies build on the same vocabulary.
The naive argument stops at "take a maximizing extreme allocation". A maximizer may run a service activity whose buffer is empty, in which case EAA fails at . Removing such activities gives , which has the right support and pressure but is in general not extreme. The pressure inequality depends on the sign pattern of , which holds only because every service activity has a single buffer. In the network of §6.2 this sign pattern fails and so does EAA. Returning from to an extreme allocation without losing the support property needs a convex-geometry argument about the polytope . In Lean this means relating Set.extremePoints of a compact polyhedron to maximizers of a linear functional and to supports.
Indexing. Internal buffers are Fin I. Buffers including Buffer 0 are Fin (I+1), with Buffer as 0 and internal buffer as i.succ. Activities and processors are 0-based.
Standing assumptions (§2), one predicate Network.Standing.
Disclosed additions to the page.
Conventions.
Set.extremePoints ℝ 𝒜.sSup. Without attainment the statement would be vacuous.Trivializing formalizations ruled out. EAA must not be weakened to a supremum over a possibly empty , and Buffer must not be counted as a constituent buffer. Either change would make the goal trivially true or impossible.
Infrastructure. Solvers need two results:
IsCompact.extremePoints_nonempty and Krein–Milman;Both are reusable beyond this mission. Contributions proving them as general Mathlib-style lemmas are welcome.