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.
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?
In Stackelberg network pricing a leader sets prices on some resources, and a follower then buys the cheapest structure available to them, paying the leader for the priced resources they use. The Stackelberg Minimum Spanning Tree problem, introduced by Cardinal, Demaine, Fiorini, Joret, Langerman, Newman and Weimann (Algorithmica 2011), is the version in which the follower buys a minimum spanning tree. The best known approximation factors for it are those of uniform pricing, which gives every priced edge the same price (Berbeglia–Joret, p. 21).
Independently, revenue management studies assortment optimisation: a seller chooses which products to offer, and customers choose among the offered products according to a discrete choice model. Berbeglia and Joret (arXiv:1606.01371, Algorithmica 2020) analyse the revenue-ordered heuristic (offer every product whose revenue is at least some threshold) under any regular choice model, and prove tight approximation bounds.
§4.6 of that paper shows that the two problems are the same problem: a Stackelberg Matroid pricing instance is an assortment problem under a regular choice model, and uniform pricing is the revenue-ordered heuristic on that model. The bounds of Cardinal et al. on uniform pricing thus become special cases of the general bounds on revenue-ordered assortments. This mission formalizes that correspondence (Theorem 4.16).
Choice model. Let be a finite set of products. A system of choice probabilities assigns to each offered set and product a probability , with no-purchase probability . It is regular if (i) all probabilities are nonnegative, (ii) for , (iii) , and (iv) whenever and . With revenues , and . The revenue-ordered assortment generated by is .
Greedy algorithm. Given a family of independent sets, a linear ordering and a set , scans in the order induced by , starting from , and adds each element that keeps the current set independent.
Stackelberg Matroid problem. An instance is a matroid , a bipartition into red and blue elements, and red costs ; some base of lies inside . The leader chooses prices . The customer buys a minimum-weight base by running greedy on with an ordering that is non-decreasing in weight ( on , on ) and puts blue elements first on ties. The leader earns .
The assortment instance. Let be the distinct red costs. Products are with . The auxiliary matroid on declares independent when it holds at most one pair per blue and is independent in . With an ordering of that is non-decreasing in cost and puts products before red elements on ties, if and otherwise.
For the instance above, with and every admissible :
and uniform pricing corresponds to revenue-ordered assortments: for each some revenue-ordered assortment earns the revenue of the uniform price , and every revenue-ordered assortment earns the revenue of some uniform price .
Theorem 4.16 transfers every guarantee for revenue-ordered assortments under regular models to uniform pricing in Stackelberg Matroid pricing. Specialising Theorems 3.1, 3.2 and 3.3 of the paper through it gives exactly the three bounds on uniform pricing proved by Cardinal et al. for Stackelberg Minimum Spanning Tree (Theorem 3 of their paper), which those authors showed to be tight (p. 24). It also places uniform pricing inside a general picture: it is a threshold policy for a regular choice model whose purchase probabilities come from a matroid greedy algorithm, and the paper notes that the argument extends to polymatroids.
The result is proved in the paper, with two steps left to the reader ( is a matroid) or justified briefly (rounding prices). No machine-checked proof exists. A formalization also produces a reusable greedy algorithm on finite matroids with its monotonicity properties (Lemma 4.14, (14)), which Mathlib at the pinned revision does not have.
The obvious argument identifies the customer's run of greedy on with the run of greedy on step by step. That identification fails as stated: the choice probabilities are defined with one fixed ordering of , while the customer's ordering is any ordering compatible with the prices, and ties among blue elements of equal price, or between a product and a red element of equal cost, may be broken differently. Equality of revenues therefore needs the tie-independence property (14) applied to as well as to , which in turn needs to be a matroid. A second gap is axiom (iv) for the no-purchase option: it requires that offering more products never decreases the number of products greedy selects, which is Lemma 4.14 (i)–(ii) for combined, not a pointwise statement. Finally, the paper's "" price must be handled with the red base: without a base inside , a blue element priced above all costs can still be bought and the optimum is unbounded.
Matroid α; , are Finset α with equal to the ground set; costs and prices are functions α → ℝ, used only on and . A linear ordering is a duplicate-free List covering the set; greedy on scans the whole list and skips elements outside , so is never re-sorted.α ⊕ (α × ℝ). The paper's conditions (1)–(2) for contain two typos (a missing "" and for ); the intended conditions are formalized. The price is the real number , strictly above every red cost.IsGreatest) over positive real prices and all compatible customer orderings. Cost levels are quantified as elements of the set of red costs rather than by index.Contributions welcome: proofs of Lemma 4.14 and (14) for Mathlib matroids (reusable beyond this mission), the matroid property of parallel extensions such as , and the three revenue identities.
Strictly convex quadratic programs — minimize a positive definite quadratic subject to linear inequalities — are the subproblems solved at every iteration of successive quadratic programming (SQP) methods for nonlinear optimization, and they arise directly in least-squares estimation with constraints, portfolio selection and model predictive control. In SQP the unconstrained minimizer of the quadratic model is available at no cost, while a feasible point is not.
D. Goldfarb and A. Idnani (Math. Programming 27 (1983) 1–33) proposed a dual active-set method that exploits this asymmetry. It starts at the unconstrained minimizer, which is optimal for the problem with all constraints removed, and adds violated constraints one at a time while keeping the current point optimal for the subproblem defined by the current active set. No phase 1 is needed. The method, usually called the Goldfarb–Idnani algorithm, is the basis of widely used solvers (for example the quadprog package in R and QuadProg++), and the paper proves that it terminates finitely with a correct answer.
Earlier dual methods for quadratic programming include the modified-simplex methods of Lemke (Management Science 8 (1962) 442–453) and of Van de Panne and Whinston (1964), which the paper compares with its own in Section 7.
Fix , a vector , a symmetric positive definite matrix , an matrix with columns , and . The quadratic program (1.1) is
The gradient is . For , the subproblem keeps only the constraints indexed by ; is solved by . A set is linearly independent if the normals , , are.
For an independent , let be the matrix with columns , , and define
The multipliers are ; for a constraint with normal the infeasibility multipliers are ; a superscript denotes the same objects for .
An S-pair is an independent active set with for and optimal for . A V-triple has , independent, , for , and .
The dual algorithm starts from . In Step 1 it stops if is feasible; otherwise it picks any violated constraint . In Step 2 it moves along the primal direction and the dual direction with step , where is the largest step that keeps the multipliers nonnegative and makes constraint active. If both are infinite it reports infeasibility. A full step () adds and returns to Step 1. A partial step (), or a dual step (), drops a constraint attaining and repeats Step 2.
For every choice of the violated constraint and of the dropped constraint :
Theorem 3 is the correctness certificate of the Goldfarb–Idnani method: whatever rule an implementation uses to choose the entering and leaving constraints, it cannot cycle and its answer is right. In particular the infeasibility verdict is a proof that (1.1) has no feasible point, which matters in SQP where infeasible subproblems trigger a different branch of the outer method. The intermediate results (the operator identities, Lemma 1, Theorems 1–2) are the standard analysis of dual active-set methods for quadratic programming.
The result is proved in the paper; to our knowledge it has not been machine-checked. A formal development produces verified projector identities for and , a verified KKT characterization for equality-active subproblems, and a verified finite-termination proof for a nondeterministic algorithm with an explicit step relation. The platform already has a proved KKT sufficiency theorem for general convex programs (ConvexOptimization.kkt_sufficient_for_convex), stated over EuclideanSpace with general convex functions and gradient fields; it can serve as background for the sufficiency half of milestone 2, but it is not stated in this mission's matrix objects.
The obvious termination argument is that increases strictly at every iteration and there are finitely many active sets. It fails as stated: partial steps may leave unchanged (the dual steps of Step 2(c)(ii)), so is only nondecreasing between consecutive states. A termination proof therefore needs a measure that also decreases along steps that do not move . Any such argument relies on invariants (independence of , nonnegativity of the multipliers, along partial steps) that hold only on reachable states, and the operators and are meaningful only while those invariants hold. Correctness of the infeasibility verdict requires the dependent case (Theorem 2), not only Theorem 1.
Vectors are Fin n → ℝ, is Matrix (Fin n) (Fin n) ℝ with G.PosDef, is Matrix (Fin n) (Fin m) ℝ, and active sets are Finset (Fin m). Multiplier vectors are indexed by constraint index (Fin m → ℝ, zero off the active set), not by position in . Lean's matrix inverse returns for singular matrices, so every statement about and assumes and an independent active set (directly, or through an S-pair or V-triple).
The algorithm is the inductive relation Step on states step1 x A u, step2 x A p u⁺, stopOptimal x, stopInfeasible, with one transition per admissible choice of and . Infinite step lengths are separate transitions; a tie takes the full step, as the paper tests first. The running value of and the factorizations of Section 4 are not part of the state.
Explicit readings of the paper's words:
Step transitions from the Step-0 state, and every reachable state without a successor is a STOP whose verdict is correct (optimal for (1.1), or (1.1) infeasible);Property (2.10), printed , is false unless and is not formalized. Equality constraints (1.2), Section 4 (numerically stable implementation), Sections 5–6 (computations), Section 7 (comparisons) and the Appendix example are out of scope.
A trivializing formalization is ruled out: the goal quantifies over every run of the relation (not one selection rule, not "some run terminates"), the infeasibility verdict is about (1.1) itself, and the algorithm is a relation that always has a successor until a STOP, so correctness cannot hold because a run gets stuck.
Needed infrastructure: Schur-complement and projector identities for and ; first-order optimality for convex quadratics on affine subspaces with inequality multipliers; well-foundedness arguments for a nondeterministic relation. The operator identities and the KKT characterization are reusable for other active-set and SQP analyses. Contributions of proofs of any milestone, and of reusable lemmas about and , are welcome.
Many network design and production–distribution problems have economies of scale: shipping twice as much along an arc costs less than twice as much, because of fixed charges, set-up costs or volume discounts. Modelled as network flows, such problems ask for a flow of least cost when each arc cost is a concave function of the flow on the arc. Classical instances include the uncapacitated lot-sizing problem, the fixed-charge transportation problem, and the Steiner tree problem in graphs. Unlike linear costs, concave costs make the problem NP-hard in general, and the usual linear-programming arguments do not apply directly.
Erickson, Monma and Veinott (Math. Oper. Res. 12 (1987) 634–664) give the send-and-split method, a dynamic program that solves such problems in time exponential only in the number of demand nodes. Before the method can run, two questions must be settled: when does a minimum-cost flow exist at all, and can the arc costs be shifted so that they are nonnegative on flows? Theorem 1 of the paper answers both. This mission formalizes Theorem 1.
Timeline. Hirsch and Hoffman (1961) showed that a concave function bounded below on a polyhedron's extreme rays attains its minimum at a vertex; Rockafellar's Convex Analysis (1970, pp. 61, 343) gives the polyhedral form. Edmonds and Karp (1972) showed how to choose node potentials making linear arc costs nonnegative. Theorem 1 (1987) extends both to additive concave costs on uncapacitated networks.
A graph has nodes and a set of ordered pairs of distinct nodes, the arcs. A demand vector assigns a demand to each node (negative demands are supplies). A preflow is a nonnegative matrix carried by the arcs, and a flow for is a preflow with
inflow minus outflow equal to demand. A circulation is a flow for .
The flow cost is , where each is concave on and . A minimum-cost flow for is a flow whose cost is at most that of every flow for .
A preflow induces the subgraph of arcs with nonzero flow. An extreme flow is a flow whose induced subgraph is a forest (in the undirected sense; two antiparallel arcs form a cycle). A simple circuit is a directed cycle through at least two distinct nodes, with arc set ; a simple circulation is a circulation whose induced subgraph is a simple circuit. The slope at infinity is the limit of the right derivative of .
Two nodes are in the same strong component if chains (directed walks) join them both ways; a component is a sink if no chain leaves it. The augmented graph appends a node and an arc for exactly one node of each sink component. Its arc costs are on arcs inside strong components and arbitrary real numbers elsewhere; is the infimum of the costs of chains from to . For , the altered costs are .
The following are equivalent:
If moreover admits a flow and on arcs joining distinct strong components, where , they are equivalent to
and is real and satisfies .
The milestones are the statements the paper's proof rests on: the Hirsch–Hoffman extension (p. 638), , the bounds , the circuit-wise form of 4° ⇔ 5°, uniqueness of the extreme circulation, between strong components, and the two inequalities giving (all p. 639).
Theorem 1 decides existence of an optimum from the costs alone: conditions 4° and 5° do not mention the demand vector, so one test settles every demand pattern at once, and 3° guarantees the optimum may be sought among extreme (forest) flows, which is what the send-and-split recursion enumerates. Condition 6° is checkable by a shortest-chain computation, and 7° supplies node potentials that convert the instance into an equivalent one with nonnegative arc costs, the standing assumption of the paper's Theorem 2 and of its running-time analysis. For linear costs the theorem reduces to the familiar statement that a minimum-cost flow exists iff no simple circuit has negative cost.
The result is proved in the paper; it has not been machine-checked. The formalization adds a precise model of extreme flows over arcs (so that antiparallel arcs form a cycle), a treatment of slopes that may equal , and the Hirsch–Hoffman extension specialized to network polyhedra, which the paper cites rather than proves. Related platform items cover the linear, capacitated case: CycleCanceling.MinMean.minCost_iff_no_negative_cycle and CycleCanceling.MinMean.minCost_iff_exists_price (Goldberg–Tarjan), and LinearOptimization.positive_directed_cycle_of_circulation and LinearOptimization.network_basic_iff_tree on a different arc encoding.
The first idea, to argue as for linear costs by cancelling negative cycles, fails because concave costs are not additive along cycle decompositions: the cost of a flow is not the sum of the costs of its cycle and path components, and a circuit can be harmless at small flow and arbitrarily negative at large flow. Existence therefore depends on the asymptotic slopes , which may be , rather than on any finite cost evaluation. The implication from bounded rays to an attained minimum (Hirsch–Hoffman) requires identifying the vertices of the flow polyhedron with forest flows and its extreme rays with simple circulations. The potential step 6° ⇒ 7° needs a cost bound on arcs between strong components, where the concave cost is only controlled up to the total positive demand .
Nodes are Fin n; a graph is ArcGraph n, a Finset (Fin n × Fin n) of arcs without loops. Preflows are real matrices vanishing off the arcs; arc costs are functions , concave on Set.Ici 0 with value at (the paper's "without further mention" assumption, made a hypothesis). The augmented graph has nodes Option (Fin n), with none the node ; chain costs, and are EReal-valued.
The explicit readings of loose phrases are:
A formalization in which extreme flows are forests of a simple graph built from the support, in which chains are simple paths, or in which a chain of cost counts as a minimum would make 3°, 6° or the equivalence trivially or falsely true; all three are ruled out by the definitions. The running-time remarks, the computation paragraph and the linear-cost remark after the proof are not formalized. Contributions are welcome on the polyhedral side (vertices and extreme rays of ), on right derivatives of concave functions at infinity, and on walk costs with negative cycles; all are reusable beyond this mission.
A retailer that decides which products to display, an online platform that decides which items to show in a recommendation slot, and an airline that decides which fare classes to open all face the same problem: the set of options offered changes what customers buy, and the substitution pattern is not known in advance. The multinomial logit (MNL) model is the standard model of this substitution in revenue management (Talluri and van Ryzin 2004), and optimizing the offered set under a known MNL model is a classical, efficiently solvable problem (e.g. Rusmevichientong, Shen and Shmoys 2010, for a capacity constraint).
The MNL-Bandit asks what happens when the MNL parameters are unknown and must be learned from the purchases themselves, while revenue is being earned. Earlier approaches (Rusmevichientong, Shen and Shmoys 2010; Sauré and Zeevi 2013) separate exploration from exploitation and need the gap between the best and the second-best assortment to be known. Agrawal, Avadhanula, Goyal and Zeevi (Oper. Res. 2019, arXiv:1706.03880) give a single upper-confidence-bound policy whose regret is of order up to logarithmic factors, with no such knowledge. This mission formalizes that result, Theorem 1 of the paper.
There are products with known revenues . At each time the seller offers an assortment from a family of feasible subsets of , and one customer either buys a product or buys nothing (). Given , the choice follows the MNL model with attraction parameters and :
independently of the past. The expected revenue of is . The family is described by totally unimodular constraints, with the incidence vector of , totally unimodular and integral (cardinality constraints are the main example). A policy chooses from the past choices, and its regret is
The seller knows and but not .
Algorithm 1 works in epochs: epoch offers one assortment repeatedly until a customer buys nothing. Let be the number of purchases of in epoch , the number of the first epochs that offered , and the average of over those epochs. The algorithm forms the upper confidence bounds
starting from , and offers next the assortment in that maximizes .
Under Assumption 4.1 (every , and is closed under taking subsets) there are absolute constants such that for every instance and every horizon ,
The constants are not fixed: the goal asserts the order of the regret, which is what the paper claims.
The milestones follow the proof in Appendix A of the paper:
Theorem 1 shows that learning the choice model costs only revenue, with no dependence on how separated the instance is. The paper also proves a lower bound of order under a -cardinality constraint (its Theorem 2), so for small the bound is optimal up to logarithmic factors. The epoch device used here reduces the analysis of a choice model with substitution to unbiased i.i.d. estimates of each .
The result is proved in the paper (Appendix A, with the concentration bounds in Appendix D). It has not been machine-checked. A formal proof would also settle several printed slips that the formalization had to repair (listed under Formalization scope). The concentration bounds for geometric variables, Theorem 5 and Corollary D.1, are useful outside this mission.
The estimates are counted in epochs whose assortments are chosen adaptively from earlier estimates, so they are not independent a priori. The paper's argument that they are i.i.d. geometric with mean has to be made rigorous for an adaptive policy. The variables are unbounded, so the standard Chernoff–Hoeffding bounds for bounded variables do not apply, and the number of samples is random, which requires a union bound over all its possible values. Finally, the regret is a sum over customers while the analysis is per epoch, and the two are linked through the expected epoch length under a random number of epochs and a horizon that cuts the last one.
Fin N; a choice is none (no purchase) or some i. The parameter is normalized to , as the paper allows. Algorithm 1 is deterministic, so a history of horizon is a sequence of choices with the product law , and every expectation is a finite sum. The revenue is the published definition ChoiceCDLP.MNL.mnlObjective v r 1 S.The paper's own proofs are in its Appendices A and D.
Many stochastic optimization problems choose a decision by minimizing an expected loss. The optimum depends on an unknown distribution, so a data-based optimum alone gives no measure of uncertainty about the best achievable expected loss. This mission concerns a confidence set for that optimal value, rather than a confidence set for the decision itself. The result of Duchi, Glynn, and Namkoong shows that a broad class of divergence neighborhoods of the empirical distribution yields a calibrated limit for this set. The same construction covers nonsmooth losses and constrained decisions when the regularity assumptions below hold.
The paper develops generalized empirical likelihood for smooth functionals of a distribution and then applies it to optimization. Its Theorem 3 states the exact asymptotic coverage result for the optimal value; Appendix C identifies the functional derivative, while Appendix B gives the uniform linearization and expansion on which calibration rests. The statistical result is proved in the paper. The mission asks for a machine-checked development of its statements and proof under an explicit nondegeneracy condition required by the paper's general coverage theorem.
Let be a nonempty compact decision set. An observation has population law , and is the loss at decision . The quantity of interest is the optimal-value functional
The observations are independent and identically distributed with law . Write for their empirical distribution. A candidate distribution supported on the indexed observations is represented by nonnegative weights with . Indexed weights also cover samples with repeated observations. For a convex divergence generator normalized by and , its divergence from the empirical law is . Assumption A further requires to be three times continuously differentiable near ; it permits .
At radius , the divergence ball consists of the weights with . The confidence set is its image under :
Assumption B makes compact and requires to be Lipschitz on it with a measurable random coefficient . The theorem adds finite second moments for and for the loss at one feasible decision. These conditions control losses at every feasible decision. They also make the population and weighted empirical infima finite on the cases used in the limit.
The goal is the exact asymptotic coverage of the population optimal value, with the unique optimizer and :
Here denotes outer probability, and is the square of a standard normal variable. The milestone statements follow the paper's path to this theorem. Lemma 17 gives the directional derivative of an optimal-value functional. Lemma 13 bounds feasible empirical weights relative to uniform weights. Lemma 16 makes the nonlinear remainder uniformly negligible on the divergence ball. The display after (37) then gives a first-order expansion of the upper endpoint of ; the next display gives its one-sided Gaussian coverage limit. The goal concerns membership in the image set , including both sides of that interval.
The limit specifies a radius through a one degree of freedom chi square quantile. It applies to the value of a constrained stochastic optimization problem without requiring the optimizer or the loss to be differentiable. The positive variance condition ensures that the influence function supplies a genuine Gaussian scale. Without such a condition, a deterministic optimal loss can make coverage identically one, so the stated chi square limit would fail. The general theorem in the paper explicitly requires positive influence variance; this mission makes the condition visible in the specialized optimal-value statement.
A complete formalization would connect finite-sample divergence geometry to an asymptotic confidence claim about an optimization functional. The empirical mean and variance definitions, divergence ball, and normalized generator already exist as reusable declarations. This mission adds the optimal-value functional, its influence function, the nonlinear remainder, and the statistical limits. Those definitions can also support later confidence statements for other stochastic optimization models. The result is proved in the source paper; the Lean statements here are open targets awaiting proofs.
Pointwise control of each loss is insufficient for the optimal value: the decision minimizing an empirical weighted objective can move with the weights. A pointwise mean expansion therefore does not by itself control the infimum over . The required limit combines uniform control over the loss class with sensitivity of the infimum functional near its population minimizer. The uniform remainder in Lemma 16 is stronger than a statement for the ordinary empirical distribution because it covers every distribution in the shrinking divergence ball. The final event is membership in the image of that ball; bounds on its upper endpoint alone do not establish two-sided coverage.
Lean represents decisions by EuclideanSpace ℝ (Fin d) and assumes a nonempty compact feasible set. Assumption B uses its Euclidean norm. The paper allows any norm in finite dimension; norm equivalence permits this choice after rescaling the Lipschitz coefficient. The population law is the pushforward of the first measurable observation from a probability space. Samples are indexed from zero, so the first observations are indices . Independence and identical distribution are explicit hypotheses. Loss measurability is explicit so the population integrals have their intended values. Square integrability and compact Lipschitz control keep the real infima meaningful.
The generator takes values in EReal so a divergence infinite at zero is representable. The ball uses the published probability uncertainty set with radius and includes nonnegativity and unit mass. Its weights represent distributions absolutely continuous with respect to the empirical law. With tied observations, equal splitting across copies preserves the induced distribution and does not increase a convex divergence. The upper endpoint is ; the different minimax expression is not substituted. The chi square target uses the standard Gaussian measure of .
Mathlib measures are outer measures on arbitrary sets, so the probability of a possibly nonmeasurable membership or supremum event is the paper's outer probability. The Lemma 17 milestone expresses a signed measure through its action on the losses, as Appendix C.2 does, and uses positive directional steps. Real suprema and infima are used only where the hypotheses provide nonempty bounded values. The variance hypothesis rules out the trivial deterministic-loss counterexample. Useful contributions include the compactness and continuity facts needed for those extrema, the action-level derivative, empirical process limits, and the final two-sided event argument.
Distributionally robust optimization replaces the average of a loss over a sample by its worst-case average over all distributions close to the sample. When closeness is measured by an -divergence, the worst case over a ball of radius around the empirical distribution is also the upper endpoint of a generalized empirical likelihood confidence interval. Empirical likelihood (Owen, 1988–2001) is the case ; the , Cressie–Read and other divergences give the rest of the family.
Duchi, Glynn and Namkoong (arXiv:1610.03425, Mathematics of Operations Research 46(3), 2021) show that these robust objects behave, to first order, like the sample mean plus a variance penalty. Their Lemma 1 is the scalar version of that statement and, in the authors' words (p. 7), an expansion "that essentially gives all of the major distributional convergence results in this paper": with the central limit theorem it yields the asymptotically exact coverage of empirical likelihood intervals for a mean, and its uniform extension yields the coverage results for optimal values of stochastic programs.
Timeline. Owen (1988, 1990) proved the calibration of empirical likelihood for means of i.i.d. data. Its extension to smooth -divergences is, as the paper notes (p. 6), essentially due to Baggerly (1998), Corcoran (1998) and Bertail, Gautherat and Harari-Kermadec (2014). Lam (arXiv:1605.09349) proved an in-probability version of the expansion below for . Namkoong and Duchi (2017, arXiv:1610.02581) proved a finite-sample, high-probability version for the divergence and bounded variables. Duchi, Glynn and Namkoong proved the almost-sure version for every smooth and for stationary ergodic data.
Let be convex and lower semicontinuous, as every divergence generator in the paper is. Assumption A asks that be finite on , three times differentiable near , with and ; the value may be .
Let be a sample with empirical distribution . A distribution is a weight vector with , and . The robust mean is
The sample mean is and the sample variance is (normalised by ).
A sequence of real random variables is strictly stationary and ergodic if the law of the path on is invariant under the left shift and every -invariant measurable set of paths has -measure or . Every i.i.d. sequence qualifies (Kolmogorov's – law), as do stationary Markov chains started in a unique invariant law and stationary mixing sequences.
Let be strictly stationary and ergodic with , let satisfy Assumption A and . Then almost surely
This is the paper's (8), " with a.s.", with taken to be the left-hand side. No rate is asserted, so the goal is not tied to any constant.
The result. The expansion says the robust mean is a variance-regularised mean, , up to , for every smooth divergence at once. Combined with the central limit theorem and Slutsky's lemma, it gives , the exact asymptotic coverage of generalized empirical likelihood intervals (the paper's Proposition 1 for ). The paper's uniform expansion (Theorem 2) and its coverage theorem for optimal values (Theorem 3) rest on the same mechanism. Because the statement is almost sure and allows stationary ergodic data, it also covers time series and simulation output.
Formalizing it. The lemma is proved in the paper; no machine-checked version of it, of (30), or of Lemmas 6–9 exists. A complete development would give the first formal link between -divergence balls and variance regularisation for general , and a formal almost-sure theory for empirical likelihood beyond the i.i.d. case. The -only finite-sample expansion of Namkoong and Duchi (2017) is posed, not proved, on the platform.
The obvious route is a second-order Taylor expansion of around inside the supremum. It fails because the optimal weights are close to only if no single observation is large compared with ; a heavy observation drives a weight to , where may be infinite and is not approximated by its Taylor polynomial. The argument has to sandwich the divergence ball between a quadratic ball and a Huber ball valid on all of , then show that the event "no observation of order " holds eventually almost surely, which under only a second moment and no independence needs a Borel–Cantelli argument for identically distributed variables (Lemma 7). The sample variance limit needs Birkhoff's pointwise ergodic theorem, which Mathlib does not yet contain.
Z 0 is the paper's and the -th sample vector is fun i : Fin n => Z i ω. Stationary ergodicity is IsStationaryErgodic: each Z i measurable and Mathlib's Ergodic for the left shift on the path law (which includes shift invariance). The mixing display on p. 7 implies this; the Lean hypothesis is the weaker standard notion named in the lemma.EReal, using the published IsPhiDivergenceFunction (convex on , finite on , , allowed); AssumptionA adds lower semicontinuity on (the paper's standing condition on divergence generators), three-times differentiability on an interval , , . The reading "finite on " follows the paper's remark that only the behaviour at is unrestricted.probUncertaintySet, and the supremum is a real sSup of a non-empty bounded set. Mean and variance are the published empMean, empVar.PalmQueueing.Ergodic.discrete_pointwise, for bijective flows), Borel–Cantelli (in Mathlib), and elementary convex analysis of the Huber function. The pointwise ergodic theorem and Lemma 7 are reusable well beyond this mission. Proofs of any milestone, and of the ergodic theorem for one-sided shifts, are welcome.Consensus asks processors, each holding an initial value, to agree on one value despite some of them failing. It underlies replicated databases, atomic commit and state-machine replication. Its solvability depends on the timing assumptions. With fully synchronous processors and communication, fail-stop faults can be tolerated for any . With fully asynchronous communication, Fischer, Lynch and Paterson showed that no deterministic protocol tolerates even one fail-stop fault (JACM 1985).
Dwork, Lynch and Stockmeyer (JACM 1988) introduced partial synchrony, a model between these two extremes. Message delays have an upper bound , but either the bound is unknown to the protocol, or it holds only from an unknown time on. For each fault type they found the exact number of faults that can be tolerated. This mission formalizes the lower bound for fail-stop faults: when the processors are synchronous and communication is partially synchronous, no consensus protocol tolerates faults once .
Timeline. 1985: Fischer, Lynch, Paterson, impossibility of consensus with one fail-stop fault under asynchrony. 1987: Dolev, Dwork, Stockmeyer, which combinations of synchrony assumptions admit consensus (JACM 1987). 1988: Dwork, Lynch, Stockmeyer, partial synchrony, with matching upper and lower bounds on resiliency for fail-stop, omission, authenticated Byzantine and Byzantine faults. The global stabilization time of the 1988 paper became a common liveness assumption for later fault-tolerant agreement protocols.
There are processors . Each processor holds an initial value . Each runs a deterministic protocol: a transition diagram over a possibly infinite set of states. In each state the next instruction is either , which puts message in 's buffer, or , which removes a set of messages from 's buffer and delivers it. The next state depends on the current state and, for a Receive, on . A step never both sends and receives. Each state may record a decision, and the first decision a processor records is final.
Real time is the ticks . A run fixes the initial values and, at each tick, which processors take a step and which messages each Receive delivers. A message is delivered only after the tick at which it was sent, only to its addressee, and at most once.
A protocol is a -resilient consensus protocol achieving weak unanimity if the following holds for every set of at least processors and every allowed run in which the processors of are correct and the others fail-stop. No two processors of decide differently (consistency). Every processor of decides (termination). If all initial values are and no processor is faulty, every decision is (weak unanimity).
For integers with
there is no -resilient consensus protocol achieving weak unanimity for binary values with fail-stop faults and synchronous processors. This holds for every positive when holds eventually, and when delta is unknown.
Split the processors into groups and with .
The result. Theorem 4.3 shows that the resiliency of the paper's fail-stop and omission protocols (Theorems 4.1 and 4.2) is optimal. It holds even under three restrictions: binary values, weak unanimity, and processors in perfect lock-step. Partial synchrony costs a majority of correct processors, whereas full synchrony costs nothing. The same scenarios give the authenticated Byzantine bound (Theorem 4.4). The halting remark of Section 4.2 rests on an argument of the same kind.
The formalization. The theorem is proved in the paper, and its proof is short. It is not machine-checked anywhere known to the mission. No message-passing model is on the platform. This mission supplies one: a step-level model with buffers, per-message timing, fail-stop faults and both partially synchronous communication models. It also gives a machine-checked impossibility on top of that model. FLP, Theorem 4.4 and the lower bounds of Section 6 are natural follow-ups on the same definitions.
The informal proof is an indistinguishability argument. Making it formal means comparing different runs of the same deterministic protocol. Two points need care.
First, the scenarios must be allowed runs. Scenario C holds messages between the groups back past . With delta unknown, this needs a larger than that delay. When holds eventually, is fixed before the protocol, and the protocol fixes and . So the delay is legal only for messages sent before the global stabilization time, which must therefore be placed after . Read literally, "every message between the groups takes more than steps" is not an allowed run in this model.
Second, "the processors of act exactly as they do in Scenario A" is a claim about whole runs. Two runs must agree on states, on which messages are in which buffer, and on when each message is delivered, tick by tick up to . With one-to-one sends and atomic steps, "delivered in exactly time 1" also needs a reading: a processor that sends at the next tick cannot receive at that tick.
All declarations live in the namespace DLSConsensus.LowerBound. Processor is the index of Fin N. Values are Bool. The protocol's state type and message type are arbitrary types in Type, finite or infinite. R.state i n is the state after tick . A message instance is identified in the run by its sender and send tick. A Receive hands the protocol each delivered message as (sender, content); the absolute send tick is not exposed.
Explicit readings and conventions:
Trivializing formalizations are ruled out. The model has allowed runs for every protocol, so Resilient is never vacuously true. Correct processors step at every tick, so termination does not fail for the wrong reason. Unanimity is the weak form, applied only when no processor is faulty.
Contributions welcome: a general simulation lemma (equal inputs up to a tick give equal states up to that tick), the construction of runs from a delivery schedule, and proofs of the scenarios. These parts are reusable for the other lower bounds of the paper.
The diameter of a polyhedron is the largest number of edges needed to travel between two vertices of its graph, its 1-skeleton. Whether this number is bounded by a polynomial in the dimension and the number of facets is a long-standing open question in polyhedral combinatorics; edge walks are the moves of vertex-following methods such as the simplex method, so the question bounds what any such method can achieve in the worst case. For fixed dimension, Larman proved in 1970 that the diameter grows at most linearly in , with a constant exponential in (Larman 1970).
Eisenbrand, Hähnle, Razborov and Rothvoß ask how much of the geometry of polyhedra such upper bounds actually use. They isolate a single combinatorial path property shared by the graphs of non-degenerate polyhedra and announce that the known upper bounds, Larman's among them, "continue to hold in the base abstraction" defined by that property (Dagstuhl abstract, p. 3). The next sentence of the abstract reads: "While the first bound is merely an adaption of the proof in [13], our proof of the second bound is much simpler than the one which was proved for polyhedra in [16]."
The held source is the five-page Dagstuhl extended abstract dated June 15, 2010, which states the results and proves none of them. The full proofs appear in Mathematics of Operations Research 35 (2010), 786–794 (journal article). The goal is an asserted theorem of the paper, not an open conjecture; the formal proof remains to be supplied.
Let and write for the family of its -element subsets. A graph in the base abstraction has a nonempty vertex set : every vertex is a -element set of labels, and distinct vertices carry distinct sets. The edges are arbitrary subject to condition i): for each there exists a path connecting and whose intermediate vertices all contain . Condition i) makes connected. The class of all such graphs is ; is called the dimension and the number of facets of the abstraction, and denotes the largest diameter of a graph in (p. 2).
The distance is the least number of edges of a path from to . The motivating example is the graph of a non-degenerate polyhedron (each vertex on exactly facets), each vertex labelled by its facets: two vertices are joined by a path inside the minimal face containing both, and every vertex of that path lies on the facets the two endpoints share (pp. 2–3). The class is not restricted to such graphs.
The abstract prints the bound as and states that it continues to hold in the base abstraction. The target is the pointwise form of :
In Lean this is the existence, for every pair , of a walk from to with at most edges. The statement quantifies over every graph satisfying the paper's definition, not over polyhedron graphs or a chosen family.
For fixed the bound is linear in , and it holds for a class defined only by finite sets and one path condition. Together with the almost-quadratic lower bound announced in the same paper, it shows what this one property of polyhedra can and cannot deliver: linear growth in for fixed dimension, but not a linear bound uniform in and . Since the graph of every non-degenerate polyhedron lies in (a separate mission of this series), the result also recovers a Larman-type bound for polyhedra, with constant .
Prove2Me already has proved polytope versions: Hirsch.larman_bound (the sharper constant for nonempty bounded -polytopes), Hirsch.larman_high_dimension, Hirsch.larman_layer_recursion, and Hirsch.tight_row_interval, the polytope form of the interval property that condition i) abstracts. They concern a different object, the vertex-edge graph of an -polytope, and are credited as prior work; none states the bound for every graph of . The platform definition Hirsch_clf (connected layer families) is a related abstraction in layered form and is not the graph class used here.
The class contains graphs with no geometric realization, so a proof cannot use convexity, faces as polyhedra, or linear-algebraic facts about vertices; only labels, intersections and walks are available. Condition i) guarantees a path preserving the common labels of two endpoints, but says nothing directly about the length of that path. Mere connectivity on -subsets of gives only the trivial bound , which is far from linear in . A linear bound in has to be extracted from condition i) alone, uniformly over all graphs of the class. The abstract describes its proof only as much simpler than Larman's for polyhedra and states no intermediate lemma, so the mission carries no milestones.
Fin n, labels ; only the number of labels matters.V : Finset (Finset (Fin n)) and the graph is G : SimpleGraph V; vertices are therefore distinct label sets, as in the paper. InB d n V G requires V.Nonempty, every vertex of cardinality , and CondI V G.CondI asks for a walk all of whose vertices contain . This is the source's path condition: a walk contains a path on a subset of its vertices, and the endpoints contain automatically.Hirsch.larman_bound is not claimed here.Trivializing formalizations are ruled out: labels are the vertices themselves (not an arbitrary labelling that could repeat), and condition i) is required for all pairs, not for one chosen path or only adjacent vertices. A proof only for polyhedron graphs, for graphs with extra structure, or with a larger constant leaves the goal open. Useful contributions include general lemmas about CondI and walk-length bookkeeping for SimpleGraph on a finite vertex type; these are reusable by the other missions of this series.
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.
Online bipartite matching models decisions that must be made as requests arrive: an advertiser can be assigned to a compatible request once, and an assignment cannot be revised when later requests reveal a better alternative. Display advertising is the motivating example in Feldman, Mehta, Mirrokni, and Muthukrishnan's 2009 preprint: an ad server knows which advertisers accept each kind of impression and has estimates of how frequently those kinds will arrive. The question is how much this advance distributional information helps when decisions still have to be immediate.
This mission studies the paper's first offline-guided algorithm. It computes a maximum matching for the expected traffic and follows that matching during the actual random run. The paper shows that this natural policy reaches the familiar performance level and that its own analysis cannot be improved for this policy, even if performance is averaged over runs. The result sets the baseline for the paper's later two-suggested-matchings algorithm, which improves on that level under its stated assumptions. Feldman et al., §§1 and 4.1
An instance consists of a finite advertiser set , a finite impression-type set , and allowed edges . For each type , the nonnegative integer is its expected number of arrivals. There are arrivals. Each arrival independently has type with probability . A type with remains in the graph but has zero arrival probability. On an arrival of type , an online algorithm may assign it to an adjacent advertiser that has not been assigned before, or may leave it unassigned. The hindsight optimum, , is the largest matching in the realization graph with one vertex for every arrival position, including separate vertices for repeated types. Feldman et al., §2, pp. 3–4
The suggested matching algorithm first selects any maximum integral flow in the expected-instance network. Each advertiser has capacity one, and each type has capacity . Equivalently, the selected edges form a maximum degree-capped bipartite matching . Let be the advertisers covered by . When type arrives, the algorithm chooses each advertiser joined to by a selected edge with probability ; any remaining probability chooses no advertiser. It assigns the chosen advertiser if available and otherwise makes no assignment. Its number of assignments is . This rule includes the algorithm's random choice in addition to the random arrival types. Feldman et al., §4.1, p. 5
The canonical residual cut of places each advertiser and impression type on the source side if it is reachable from the source by residual edges. Write for advertisers on the sink side and for types on the source side. These sets describe the comparison between the expected-instance matching and the optimum of a realized run. The mission also uses occupancy: after independent uniform throws into bins, count how many bins in a fixed subset receive at least one ball. Feldman et al., §§2.1 and 4.1
Theorem 4's general-instance guarantee is expressed in the additive form established by its analysis. For every , there are and , uniform across all finite instances, all maximum integral flows, and all valid ways of realizing the algorithm's random choice, such that implies
The complete bipartite family gives the tightness target. When and every , every maximum expected-instance matching is perfect. For every run, , and
The milestone list follows the paper's Fact 1 and the named passages “Bounding ALG,” “Bounding OPT,” and “Tightness of the Analysis” in §4.1. The cut identity is a separate deterministic milestone. Feldman et al., Theorem 4 and §4.1, pp. 5–6
The result establishes exactly what this one-matching policy achieves under integer-frequency independent arrivals. It gives a guarantee for the actual number of assignments relative to the best assignment made with hindsight, and a family on which the limiting expected ratio equals the guarantee. That tight family explains why the paper introduces a second suggested matching rather than seeking a stronger bound for the same policy. Feldman et al., §4
The mathematical theorem is proved in the paper; the mission asks for its machine-checked formalization. The development would also provide reusable finite models of repeated-type realizations, integral degree-capped bipartite matchings, uniform occupancy, and residual reachability cuts. No machine-checked proof of these mission items is being claimed by this draft.
The expected-instance matching is selected before the arrivals, but the hindsight optimum can exploit the actual multiplicities of every type. Counting only the ads selected online does not compare the algorithm with that hindsight optimum. Also, a type may have several selected advertisers when , so replacing the algorithm's random choice by a deterministic designated ad would change its law. The cut and concentration statements have to apply uniformly to every maximum integral flow, including flows chosen by different tie-breaking rules. Feldman et al., §4.1, pp. 5–6
Advertisers and types are finite Lean types. The edge relation is a finite set, and and are natural numbers with . An integral maximum flow is represented by a maximum cardinality edge set with advertiser degree at most one and type- degree at most . The theorem quantifies over every such set. This is the unit-advertiser, integer-type-capacity flow used in §4.1, without a separate real-valued flow object. The canonical cut is defined through residual reachability. The hindsight optimum maximizes over matchings of the realized graph, with each arrival position distinct.
The run uses independent uniform draws from . A valid labelling assigns each selected advertiser at type to a distinct copy. The drawn copy determines the type and, if labelled, the ad selected by the algorithm. This gives type probability , conditional ad probability on selected edges, and the remaining “no ad” probability. Counts, probabilities, and expectations use finite sums, so there is no integrability convention. Since , the run sample space is nonempty; no value of at is needed. The complete-graph family has .
The paper writes in both bounding passages. The Lean statements spell this out as instances with , with preceding the instance. Theorem 4's ratio language is represented by the additive estimate its proof yields; a vanishing ratio error requires a separate lower bound on . The exact finite- expectation and its limit make “tight, even in expectation” precise. The printed Fact 1 exponent is , while its Appendix A proof yields ; the formalized concentration statement uses the proved exponent and the milestone retains the printed wording. Neither a ratio with a zero denominator nor a labelling that changes the algorithm's choice law is accepted as a shortcut.
Contributions toward the occupancy bound, the residual cut identity, the realized matching bound, and the complete-graph expectation are welcome. The finite occupancy and matching interfaces are intended for reuse beyond this specific algorithm.
The diameter of a polyhedron is the largest number of edges needed to travel between two vertices of its graph. Bounding that number from the dimension and the number of facets is a central question in polyhedral combinatorics because edge walks are the discrete moves available to many vertex-based optimization methods. The Kalai–Kleitman bound gives a quasi-polynomial upper bound in these parameters. Eisenbrand, Hähnle, Razborov and Rothvoß ask how much of the geometry is needed to retain such a bound. They isolate one path property of polyhedron graphs and show that the upper bound persists for every graph satisfying it, including graphs that need not arise from a polyhedron (Dagstuhl abstract, pp. 1–3).
This mission concerns that extension of the Kalai–Kleitman bound. The held source is the five-page Dagstuhl extended abstract dated June 15, 2010. It states the result without its proof. The full proofs appeared in Mathematics of Operations Research 35 (2010), 786–794 (journal article). The goal is an asserted result of the paper, not an open conjecture; the formal proof remains to be supplied.
Let , and let be the family of its -element subsets. A graph in the paper's base abstraction has a nonempty vertex set . Thus each graph vertex is labelled by a distinct -element subset. The edges can be chosen freely subject to condition i): for every pair , there is a path from to u\cap v\mathcal B_{d,n}dn$ the number of facets of the abstraction (definition and footnote, p. 2).
The distance between two vertices is the minimum number of edges in a path between them. A graph's diameter is the largest of these distances, and is the largest diameter among graphs in . Condition i) is motivated by non-degenerate polyhedra: if a vertex lies on exactly facets, its tight facets provide a -element label, and two vertices can be connected inside the smallest face containing them. Every vertex on that path retains the facets common to the endpoints (pp. 2–3). This motivation does not restrict to a realizable polyhedron graph.
For positive dimension, the target is the pointwise form of the paper's assertion that the upper bound continues to hold in the base abstraction:
Equivalently, every pair has a connecting path with at most edges. Consequently . The statement covers every graph with the paper's labels and condition i), rather than a selected realization or a graph with extra geometric properties. The source prints the inequality for , its polyhedron-diameter notation, and says in the same sentence that it continues to hold for the base abstraction (p. 3).
The bound shows that a common-facet path property is enough to prevent arbitrarily large diameter once and are fixed. It extends an upper bound first attached to graphs of polyhedra to a class specified entirely by finite sets and graph paths. This locates a concrete portion of the polyhedral diameter theory within combinatorics. The same paper gives an almost-quadratic lower bound for the abstraction, so the path property alone does not imply a linear bound in (p. 3).
A machine-checked proof would connect a precise finite graph model with the real-exponent inequality, without relying on a polyhedron representation. Prove2Me already has a proved theorem called Hirsch.kalai_kleitman_bound for a bounded -polytope, with a different exponent , and a proved Hirsch.kalai_kleitman_recursion for that polytope model. It also has Hirsch.clf_endpoint_peeling for connected layer families. Those results concern different objects or bounds and are useful prior work, but none is a formalization of the present claim for all .
The class permits edges and vertex families with no geometric realization, so a proof cannot use metric or convexity properties of a particular polyhedron. Condition i) guarantees one path preserving the common labels of two endpoints; it does not directly bound that path's length. Connectivity by itself would be too weak: a connected graph on the allowed labels can have a long shortest path unless its labels and the path condition constrain it. The formal task is to obtain the claimed uniform length bound from that condition across all finite families of -sets. The Dagstuhl abstract calls the argument an adaptation of Kalai and Kleitman's proof but states no intermediate lemmas, so this proposal does not assign any in-source milestones (p. 3).
Lean represents by Fin n, with labels instead of ; only the number of labels matters. A vertex set is a Finset of Finset (Fin n), and a SimpleGraph has exactly those sets as vertices. This representation enforces distinct labels. InB d n V G requires to be nonempty, every label to have cardinality , and CondI for every ordered pair. The walk in CondI is equivalent to the source's path: repeated vertices can be erased, and the endpoints themselves contain . Nonemptiness and condition i) together give the source's connectedness. A path through all graph vertices without the common-intersection condition would be a weaker and inadmissible model.
The theorem takes , so the logarithm has its ordinary positive-dimension interpretation. The source does not print a logarithm base; the statement reads it as base two, following the cited Kalai–Kleitman convention. This interpretation is explicit in the theorem's prose and is an open source-reading question. The exponent is real: the path length is cast from a natural number to for comparison with . No floor is applied to the exponent. The theorem asserts a bounded walk for each pair; that avoids defining through a supremum with an artificial value for an empty class. At with , InB has no instance, as there are no -element labels; at , the bound is , consistent with a connected graph on at most labels.
The development needs reusable finite-set reasoning about common intersections, graph walks and their lengths, and real-logarithm bounds. Contributions establishing those facts for the paper's CondI model are within scope. A proof only for polyhedron graphs, for graphs with extra edge restrictions, or for a single chosen graph would leave the goal open.
Consensus asks processors, each starting with a value, to agree on one value although some of them may be faulty. It underlies replicated databases, atomic commitment and state-machine replication. Two classical models bracket the problem. In a fully synchronous system, with known bounds on message delay and processor speed, consensus is solvable for many fault types. In a fully asynchronous system, Fischer, Lynch and Paterson showed in 1985 that no deterministic protocol tolerates even one fail-stop fault (FLP, J. ACM 1985).
Dwork, Lynch and Stockmeyer (J. ACM 35(2), 1988, 288–323) introduced partial synchrony between these extremes: message delays are bounded, but either the bound is unknown, or it holds only from an unknown global stabilization time (GST) on. This model, and the GST abstraction in particular, became the standard assumption under which practical consensus protocols (Paxos-style and Byzantine fault-tolerant replication) are proved live. The paper determines, for each fault type, the largest number of faults that consensus can tolerate under partial synchrony. This mission formalizes its first positive result: for fail-stop and omission faults, processors suffice.
There are processors , an integer , and an arbitrary set of values; processor starts with .
In the basic round model (Section 3.1 of the paper), computation proceeds in rounds . In each round every processor sends messages, each message is either delivered in that round or lost, and every processor then performs a state transition on the messages it received. Losses are described by a predicate . A set of processors (the correct ones) and a round constrain it: every message sent at a round from a processor of to a processor of is delivered. Before GST any message may be lost, and messages from or to processors outside may be lost at any time. Processors outside follow the protocol but lose sends and receptions (omission faults, which include fail-stop faults).
Algorithm 1 (Section 3.2.1) works as follows. Every processor keeps a set , initially , attaches it to every message, and merges in every PROPER set it receives. A processor may hold locks, each a value with an associated phase number; is acceptable to if has no lock on a value other than . Phase belongs to when . Trying phase occupies rounds , , :
Lock-release phase is round : every processor broadcasts its locks , and a lock on with phase is released on receipt of some with and .
The correctness conditions (Section 2.4) for the set are consistency (no two decisions of processors in differ), termination (every processor in decides), and strong unanimity (if all initial values equal , every decision in is ).
For all with , every value type , all initial values, every with , every , every delivery pattern allowed for and , and every admissible choice of proposals,
This is the theorem as printed; it fixes no constants.
Theorem 3.1 shows that, against omission and fail-stop faults, partially synchronous communication costs nothing in resilience compared with a majority bound: suffices, and Section 4 of the paper shows that does not. The lock-and-release structure of Algorithm 1 (a value is decided only after a quorum locks it, and locks are released only on evidence of a later competing lock) recurs in later partially synchronous protocols, where safety must hold regardless of timing and liveness is obtained only after stabilization. The result separates the two concerns cleanly: consistency and strong unanimity hold in every run, while termination uses GST.
The result is proved in the paper; to the best of the available information it has not been formalized in Lean, and no distributed-computing model exists on Prove2Me. The mission produces a machine-checked model of the basic round model with a GST delivery guarantee, a full executable specification of Algorithm 1, and proofs of its safety and liveness. The paper's own proof of Lemma 3.3 is one line and the termination argument relies on "sufficient communication"; a formal proof must make these steps explicit.
The safety argument is an invariant over an unbounded number of phases with an arbitrary loss pattern: a lock on the decided value must be shown never to be released without being replaced by a higher lock on the same value, while competing locks on other values may exist at faulty or slow processors. The obvious argument ("after a decision, every later proposal must equal the decided value") is circular without a persistence statement for locks such as Lemma 3.2. Liveness requires reasoning about what every correct processor knows after GST (its PROPER set and the locks of the others), and it depends on processors sending lock-release and list messages even when these carry no locks or no acceptable values. Quorum counting with and must be carried out over distinct senders.
Fin N; the paper's is the processor of index . Rounds start at ; exec … 0 is the initial state and exec … r the state after round . Phases start at .pick : ℕ → Set V → V, required only to pick an element of every nonempty candidate set, and universally quantified in every theorem.DecidesAt p k v (owner of phase , proposed , at least acknowledgements in round ); consistency requires all such events of processors in to agree.A formalization in which a run cannot exist, the delivery constraint is unsatisfiable, the choice of proposals is fixed, or faulty processors are absent ( = all processors) would trivialize the theorem; the model here admits runs in which processors decide, and ranges over all sets of at least processors.
Reusable beyond this mission: the round-based message-passing model with a GST delivery guarantee and omission faults. Contributions of general lemmas about runs (monotonicity of PROPER sets, persistence of locks, quorum intersection over Finset) are welcome.
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.
A manufacturing line can send the same job through several stations and return it to a station it visited earlier. Semiconductor fabrication is one example. Such a reentrant line has several customer classes at one server, and the server must choose which class to work on. A station may have enough capacity on average yet the line can still accumulate an unbounded queue under an unfortunate service rule. Dai and Weiss use deterministic fluid models to study this question: fluid represents large queues, and its motion exposes the long-run effect of the service rule. Their paper proves that two simple buffer priority disciplines have stable fluid models for every reentrant line satisfying the usual station load condition. This mission concerns Last-Buffer-First-Served, abbreviated LBFS. Dai and Weiss (1996).
The distinction between fluid and stochastic queue stability matters. Dai and Weiss cite an earlier theorem connecting stable fluid models to stable queueing disciplines under the stochastic assumptions of their introduction. The target here is their fluid theorem, Theorem 4.4, rather than a separate formalization of that stochastic implication. Dai and Weiss (1996), pp. 115, 119, 124.
There are classes, numbered in route order, and stations. Every unit of fluid enters class at rate one. On completing service in class , it becomes class ; after class , it leaves. The station serving class is . Different classes may share a station. The constituency of station is , and class has positive mean service requirement , so its service rate is . The nominal workload at station is . The paper assumes at every station. Dai and Weiss (1996), pp. 115–117.
For time , is the amount of fluid in class , and is the cumulative server time spent on that class. The flow equations say that class content equals its initial content plus completed service from the preceding class minus its own completed service. The first class receives the external unit-rate flow. Each remains nonnegative, each starts at zero and is nondecreasing, and the cumulative idle time of every station is nondecreasing. A priority rule adds a condition on when a server may reserve capacity for lower-ranked classes. These are the fluid equations of Definition 1.2 and §4. Dai and Weiss (1996), pp. 118, 122–123.
A priority ranking assigns a distinct rank to every class, with smaller rank meaning higher priority. For class , let contain the classes at the same station whose rank is at least as high as 's. In a preemptive-resume priority fluid model, capacity unused by may increase only when the fluid workload in is zero. Under LBFS, : a class later in the route has higher priority. Priority is compared within each station, even though the ranking is written globally. Dai and Weiss (1996), pp. 122–123, Definition 4.1.
Theorem 4.4 asks for stability of the LBFS fluid model for every reentrant line with positive service requirements and :
where . The same must work for every solution and every normalized initial configuration. This is exactly the fluid stability definition used by the paper. Dai and Weiss (1996), pp. 118–119, 124.
The milestones follow the paper's own intermediate statements. Lemma 2.2 treats a nonnegative absolutely continuous function whose derivative is negative whenever the function is positive. Proposition 4.2 identifies flow-rate relations at a regular point under a buffer priority rule. The proof of Theorem 4.4 records a uniform negative drift for total content and the explicit emptying time
The explicit time is stated for every initial fluid amount; normalization to one belongs only to the final stability theorem. Dai and Weiss (1996), pp. 120, 123–125.
The theorem gives a uniform finite clearing time for the LBFS fluid model whenever each station's nominal workload is below its capacity. It applies to any number of stations, any finite route, and any assignment of route stages to stations. This is stronger than checking a particular factory layout. The conclusion concerns every fluid solution, which matters because the defining equations need not determine a unique path. Dai and Weiss (1996), pp. 118–119, 124–125.
Formalizing the result requires a reusable interface for reentrant lines, service allocation, station workloads, and the priority complementarity condition, plus separate statements for the extinction criterion and priority flow rates. The theorem is proved in the 1996 paper; the remaining work in this mission is a machine-checked Lean proof of its fluid-model statement and of the listed milestones. The stochastic queueing theorem cited by Dai and Weiss is outside this mission's scope.
The load inequalities compare average work with available server time, but by themselves they do not specify which class receives service at an instant. Under other service rules, reentrant lines can amplify queued fluid despite every station being nominally underloaded; the same paper gives such an example. A formal proof therefore has to use the precise LBFS priority condition, not only the flow equations and the load inequalities. The regular-time argument must then yield a single bound valid across every possible fluid path. Dai and Weiss (1996), §§4–5.
Lean represents classes and stations by finite index types. Their indices start at zero: Lean class corresponds to paper class , and LBFS is Fin.revPerm. The paths and are functions on all real times, while the fluid equations and conclusions are imposed only for . The external arrival rate is one, as in the paper's normalization. The conditions that station idle capacity and priority-set unused capacity increase only when their relevant content is zero are expressed by constancy on each interval where that content stays positive. Service and fluid paths are not given extra continuity hypotheses; the fluid equations and monotonicity conditions provide the regularity used in the paper. Dai and Weiss (1996), pp. 116–119, 122–123.
The service requirements are explicit so has its intended value. The drift and emptying-time milestones explicitly assume , since their formula divides by the maximum station workload. The main theorem retains the universal quantification over lines; when , its normalization is impossible. A faithful solution predicate must include the priority condition (4.4), whose omission would change Theorem 4.4 into a false claim about all work-conserving policies. The definition layer, elementary real-analysis extinction lemma, and priority flow-rate relations are useful beyond this single stability theorem. Dai and Weiss (1996), pp. 117–125.
Network revenue managers sell access to limited capacity over time. An airline, for example, may have several products that use the same seat inventory, with some products earning more revenue than others. The decision to accept a request must be made when it arrives, before future requests are known. A standard way to guide that decision is to solve a deterministic linear program using expected demand, then use its optimal allocation as a probability of acceptance. As inventory changes, one can solve the program again. Bumpensanti and Wang study how often to do so, and show that frequent re-solving has a real limitation when the linear program is degenerate: on a particular instance its expected loss grows at least as the square root of the selling horizon. Bumpensanti and Wang, arXiv:1802.06192v3, Sections 3.1 and 5.1.
The same paper gives an infrequent re-solving policy with uniformly bounded regret and an upper bound of order for the frequent re-solving policy. The lower-bound result is the counterpart that identifies a case where that order cannot be removed by the frequent policy itself. It uses a two-class example small enough to expose the issue without other network complications. Bumpensanti and Wang, arXiv:1802.06192v3, Theorem 1 and Propositions 2–3.
There is one resource, initially with units of capacity, and two customer classes. Class arrives through an independent Poisson process of rate one. Accepting a customer uses one unit of capacity and earns price , where . Rejected requests earn nothing, and unused capacity has no terminal value. The higher-price class has priority in the deterministic allocation, but its realized demand is random. The horizon is a positive integer, divided into periods of length one. Bumpensanti and Wang, arXiv:1802.06192v3, Section 2, pp. 7–9, and Appendix C.1, p. 32.
At the start of a period with periods left and capacity , the deterministic linear program (DLP) chooses rates that maximize subject to and . In this instance its first coordinate is . The frequent re-solving policy (FR) accepts each class- request in that period with probability , provided capacity remains. It re-solves the DLP at the next period with the new capacity. This is Algorithm 2 specialized to the example. Bumpensanti and Wang, arXiv:1802.06192v3, Algorithm 2, p. 11, and Appendix D, p. 42.
The hindsight optimum knows the total demand from both classes at the end of the horizon and chooses the best feasible allocation using that information. Its expected value is ; the first argument is horizon length and the second is initial capacity. Let be the frequent policy's expected revenue. Since hindsight has more information, their difference is a regret benchmark. The formulation uses the paper's hindsight linear program, which is exact on this unit-consumption instance. Bumpensanti and Wang, arXiv:1802.06192v3, Eq. (3) and Definition 1, p. 9.
For every pair of prices , there are and such that, for all integer and every optimal DLP selector used by FR,
This specializes Proposition 2's existence statement to the explicit family in its Appendix C.1 proof. The constant may depend on the prices, but is chosen before the selector and the horizon. The benchmark is the hindsight value, as in the proposition. Bumpensanti and Wang, arXiv:1802.06192v3, Proposition 2, p. 18, and Appendix C.1, pp. 32–34.
The milestones record the optimal DLP allocation on the example and two clauses of Lemma 7. The latter estimate the probabilities that the high-price arrival count is moderately below its mean in the first third and moderately above its mean in the last third. With an integer phase length and , the first bound is
The third-phase bound uses the standard normal cumulative distribution function and the unrounded constant . Bumpensanti and Wang, arXiv:1802.06192v3, Lemma 7 and Eqs. (49)–(53), p. 40.
This result shows that solving the DLP every period does not, by itself, give a horizon-independent expected loss. The example has only one resource and two customer classes; the gap cannot be attributed to a large network. The paper's separate bounded-regret result uses a different re-solving schedule and acceptance rule, so formalizing this lower bound helps distinguish guarantees for the two policies. Together with the upper bound for FR, it identifies the square-root order as the relevant scale for this policy on the example. Bumpensanti and Wang, arXiv:1802.06192v3, Sections 4–5.
The mathematical proposition is proved in the cited paper; the Lean goal here remains an open theorem statement. Formalizing it requires precise interfaces for a Poisson arrival model, a capacity-limited randomized policy, a hindsight LP benchmark, and asymptotic lower bounds. Those interfaces can be reused in later revenue-management results, while the two-class instance gives a concrete check on the conventions.
The initial DLP solution allocates the average capacity to the high-price class. A simple intuition might therefore predict that repeated re-solving preserves capacity for that class. The remaining-capacity ratio, however, responds to realized arrivals; when the ratio rises above one, the re-solved LP assigns positive acceptance probability to the lower-price class. The policy then spends capacity before later high-price arrivals are known. The lower-bound analysis needs a path event that controls arrivals through the middle phase and a joint event involving the policy's accepted requests. Marginal Poisson counts alone do not determine those admissions. Bumpensanti and Wang, arXiv:1802.06192v3, Appendix C.1, pp. 32–34.
Lean uses Fin 2 for classes and Fin 1 for the resource. The general model takes positive Poisson rates, nonnegative prices and nonnegative consumption. On the lower-bound instance the rates and consumptions equal one, capacity equals , and prices satisfy . These are the operational standing assumptions of the paper's Section 2 and the positive-price reading used by the example. Optimal DLP ties are represented by quantifying over every selector. The LP value is the published RLPBidPrice.Unbiased.piValue definition, evaluated on nonnegative capacity vectors; the rate and capacity conventions make its real supremum well posed.
The window law superposes the independent class Poisson processes into a Poisson total count, independent class labels, and independent Bernoulli acceptance marks. A fold over ordered arrivals applies Algorithm 2's capacity check after every acceptance. The expected hindsight value sums over independent total demand counts, and the FR value is a backward recursion over the remaining unit periods. The target's is strictly positive and fixed before the horizon, so neither a zero constant nor a horizon-dependent constant can satisfy it trivially.
The two Lemma 7 milestones cover only and . Its continuous-time event and the joint admission event require a path probability space and are outside this draft. Equation (52) yields ; the printed rounds that value upward. The source proof divides into three exact integer-length phases, while Proposition 2 is stated for all sufficiently large ; this gap requires attention in a complete proof. The source here is arXiv:1802.06192v3, whose printed and PDF page numbers coincide.
Semiconductor wafer fabrication is the standard example of a reentrant line: every wafer follows the same long route through a set of machines, and visits several machines many times. Each visit is a separate processing step, and a machine with work waiting from several steps must choose which step to serve. Kumar (1993) proposed studying such lines through their buffer priority rules, and Lu and Kumar (1991) showed that a priority rule can make a line unstable even though every machine has spare capacity. The question is therefore not academic: a scheduling rule that looks reasonable can let queues grow without bound.
Dai (1995) reduced the positive Harris recurrence of a multiclass queueing network to the stability of a deterministic fluid model, and Dai and Weiss (1996) used this reduction to prove stability results for several reentrant lines. This mission formalizes their Theorem 4.3: under the First-Buffer-First-Served (FBFS) discipline, the fluid model of every reentrant line is stable whenever each station's nominal workload is below one. Kumar (1993) had proved the analogous statement for discrete deterministic systems.
Timeline:
A reentrant line has stations and classes. All fluid follows one route: it enters as class , becomes class when class is completed, and leaves after class . Class is served at station with mean service time , and . The constituency of station is , and its nominal workload is . The exogenous arrival rate is . The standing assumption of the paper is
A fluid model solution is a pair of paths , the fluid levels, and , the cumulative service time given to each class, such that for :
with ; each starts at and is nondecreasing; and the idle time of each station is nondecreasing.
A buffer priority discipline is a permutation of the classes; a class has priority over a class at the same station when . Write , , and . Under preemptive resume, may increase only at times when (condition (4.4)): a station never idles toward the classes of priority at least that of while any of them holds fluid. FBFS is , so earlier steps of the route have priority.
The fluid model is stable (Definition 1.3) if there is a time such that every solution with has for all .
For every reentrant line with and (1.7),
The goal asserts existence of an emptying time; it does not fix the value.
on, which gives the goal with an explicit constant.
Combined with Dai's theorem (Theorem 1.1 of the paper), Theorem 4.3 gives positive Harris recurrence of every multiclass reentrant line operated under FBFS, under the distributional assumptions of that theorem, whenever (1.7) holds. Since Lu–Kumar-type examples show that priority rules can destabilize a network with spare capacity, a rule that is provably stable on every reentrant line is a meaningful guarantee. FBFS, together with LBFS, is the basic positive case against which the instability examples in the same paper (Theorem 5.1) are compared.
Formalizing the result adds a machine-checked version of the fluid model with priority constraints, stated for an arbitrary line rather than a fixed network, and a checked explicit emptying time. The result is proved in the paper; no machine-checked proof is known. The rate identities of Proposition 4.2 and the extinction lemma are reused by the LBFS mission of this series.
The fluid model gives the paths only as nondecreasing functions subject to equations; nothing says they are differentiable. Every argument about rates holds only at regular times, and the conclusion must be integrated back through absolute continuity, which itself must be derived from the monotonicity conditions. The priority condition (4.4) is an "increases only when empty" condition; turning it into the rate identity (4.6) at a regular point requires continuity of the fluid levels and a careful local argument. The induction over classes needs uniform control of every earlier buffer for all later times, not only at one instant, so a pointwise reading of "buffer is empty" is not enough. Finally, the explicit constant requires bounding the content of buffer at time by the total content, which may have grown since time .
Fin K and Fin I, 0-based: the paper's class is Lean index .ℝ → Fin K → ℝ; every equation is imposed on only, and derivatives are taken at .ConstantWhile): the idle process is constant on every interval of on which the content stays positive. This is equivalent to the paper's Stieltjes integral form for continuous paths.Equiv.Perm (Fin K), FBFS is the identity; is .A trivializing formalization is ruled out: the goal uses the priority fluid model, not the work-conserving one alone (which would claim that every work-conserving fluid model is stable, false by Theorem 5.1), and a sorry-free witness shows that the FBFS solution predicate has solutions with , so stability is not vacuous.
Contributions welcome: the extinction lemma for absolutely continuous functions, the derivation of Lipschitz continuity from (1.10)–(1.12), and the rate identities of Proposition 4.2 are reusable beyond this mission.
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.
Network revenue management decides, in real time, which customer requests to accept when every request consumes a bundle of scarce, perishable resources: seats on several flight legs of an itinerary, room-nights of a multi-night hotel stay, bandwidth on several links. The exact dynamic program is intractable for realistic networks, so practice and theory rely on heuristics built from a deterministic linear program (DLP) that replaces random demand by its mean. The question is how much revenue such heuristics lose.
The classical answer (Gallego and van Ryzin 1994, 1997; Talluri and van Ryzin 1998) is that solving the DLP once and following its solution loses over a horizon of length . Re-solving the DLP as capacity is consumed was long believed to help, and Jasin and Kumar (2012) proved that re-solving in every period has bounded loss if the DLP solution is nondegenerate. Bumpensanti and Wang (arXiv:1802.06192v3) showed that the nondegeneracy condition matters: frequent re-solving can lose on degenerate instances. They then proposed a policy, Infrequent Re-solving with Thresholding (IRT), whose loss is bounded by a constant independent of the horizon and of the capacities, with no nondegeneracy assumption. This mission formalizes that result.
There are customer classes and resources . Class- customers arrive as independent Poisson processes of rate on . Accepting a class- customer earns and consumes units of resource ; is the bill-of-materials matrix with columns , and is the initial capacity. A customer can be accepted only if componentwise, being the remaining capacity; leftover capacity is worthless at .
The DLP with right-hand side is
and is times its value at . The hindsight optimum is , where is the value of the same LP with capacity and the realized demands as upper bounds. It bounds the expected revenue of every non-anticipating policy, and the regret of a policy is .
A probabilistic allocation on a window accepts each class- arrival with a fixed probability when capacity allows. The IRT policy uses and re-solving times for , where . At it solves the DLP with right-hand side (remaining capacity over remaining time), obtaining . In the epochs it accepts class with probability if , else if , else ; in the last epoch it uses . The family re-solves times on the same schedule; is static probabilistic allocation (SPA), and follows until and then earns the hindsight optimum of what remains.
There is a constant such that for every horizon and every capacity vector ,
The constant is not fixed; the content is its independence of , of , and of the optimal LP solution chosen at each re-solve.
The result separates two design choices in re-solving heuristics: how often to re-solve and how to turn an LP solution into a control. It shows that re-solving only times, combined with rounding nearly-degenerate acceptance probabilities to or , is enough for bounded regret, and that the constant is uniform over all capacity-to-horizon ratios, so degenerate DLP solutions, which occur only at particular ratios, cause no loss of order. Since , it also shows that the hindsight optimum is within a constant of the optimal policy's value in this model.
The result is proved on paper but not machine-checked. A formalization would produce a reusable Poisson-arrival revenue-management model, a precise account of the regret decomposition over re-solving epochs, and an independent check of a proof with known gaps (see Difficulty). No part of it is formalized on the platform.
The obvious argument compares the policy with the DLP solution and controls the deviation of Poisson demand by its standard deviation; this gives only , because the DLP value exceeds the hindsight optimum by order and the lost sales accumulate. Bounded regret needs a comparison with the hindsight LP, path by path: the acceptances made before the last re-solve must remain extendable to a hindsight-optimal solution with overwhelming probability. This requires LP sensitivity of the hindsight solution to the random right-hand side, uniformly over the degenerate cases, and the printed proof's statement of it (Lemma 5) is false as printed: on a two-class, single-resource instance its interval for is empty. A correct argument needs a proximity bound for optimal LP solutions under a change of the demand bounds, summed over all classes, not only over . The analysis of the schedule (the sum over epochs in (13)) is elementary but the printed chain of inequalities on p. 30 uses a monotonicity that fails for large arguments.
All objects are in the definition item ResolvingNRM.IRT.Model. Classes are Fin n, resources Fin m, A : Matrix (Fin m) (Fin n) ℝ. LP values reuse piValue from the published RLPBidPrice.Unbiased.Model; the hindsight LP is over real , as in (3). Expectations are explicit sums of Poisson weights. A window of probabilistic allocation is represented by its Poisson count of arrivals, i.i.d. classes with law and independent Bernoulli acceptance coins, the standard representation for controls constant on the window. Policies are backward recursions over the re-solving epochs. Ties in the LP are left open: a policy takes an arbitrary optimal-solution selector, and every theorem quantifies over all selectors after its constants.
Conventions and deviations from the page, each disclosed in the item concerned:
A statement that lets depend on or , compares IRT with the DLP instead of the hindsight optimum, uses a fixed number of re-solves, or assumes a nondegenerate or vertex LP solution is trivial or a different theorem, and is ruled out by the quantifier order of the goal. The milestone has a sorry-free local check.
Welcome contributions: LP proximity results (Cook–Gerards–Schrijver–Tardos type), Poisson concentration, superposition and thinning of Poisson processes, and lemmas on expectations of LP values. The source is arXiv:1802.06192v3; its printed page numbers equal the PDF page numbers.
Operations research has long studied the stochastic problem : choose a decision before an uncertain quantity (demand, prices, returns) is revealed. In practice the decision maker also observes covariates before deciding (web-search volume before stocking a product, weather before routing a shipment) and should solve the conditional problem instead. Bertsimas and Kallus (arXiv:1402.5481v4; Management Science 66(3), 2020) proposed predictive prescriptions: reweight historical observations by how relevant they are to the current , using weights borrowed from a nonparametric regression method, and minimize the reweighted sample cost. Their asymptotic theorems guarantee that this procedure converges to the decision that full knowledge of the conditional distribution would give.
The unconditional special case, sample average approximation (SAA) with i.i.d. draws of and no covariate, has a classical consistency theory (Dupačová–Wets 1988; Shapiro 2003). This mission conditions that theory on , with -nearest-neighbour weights.
Decisions lie in a set , covariates in , uncertainty in ; all three spaces carry the Euclidean norm. A cost is given. Let be the joint law of , the law of and the conditional law of given . The conditional cost and the full-information problem (2) are
The data are , the first terms of an i.i.d. sequence with law . The kNN weights (12) are is one of the nearest neighbours of among , with ties among equidistant points broken by lower index first. The predictive prescription (3) is any
The paper's standing assumptions: Assumption 3 ( for every , and for a.e. ); Assumption 4 ( is equicontinuous in , uniformly over ); Assumption 5 ( closed and nonempty, and either bounded, or is bounded below for large and for each there is a set of positive conditional probability on which uniformly as ).
Definition 1. is asymptotically optimal if, with probability 1, for -a.e. , ; it is consistent if, with probability 1, for -a.e. , .
Under Assumptions 3, 4, 5 and i.i.d. sampling, with , , : with probability 1, for -a.e. , is nonempty, the argmin is eventually nonempty, and every selection from it satisfies
The goal covers both cases of Assumption 5, including unbounded such as the newsvendor's .
Theorem 5 says that a decision computed from data alone, with no model of the conditional distribution, performs asymptotically as well as the decision a decision maker with full knowledge of would take, for almost every covariate value and under mild conditions on the cost. It justifies the kNN prescription in the paper's newsvendor and shipment-planning experiments, and its proof skeleton (a pointwise strong law for the weights, then Lemmas 5–7) is reused for kernel, local-linear and recursive-kernel weights (Theorems 6–9), which could follow as missions of the same shape.
The result is proved in the paper; it has not been machine-checked anywhere. Formalizing it requires a strong law for nearest-neighbour regression with integrable responses (Walk 2010, building on Devroye, Györfi, Krzyżak and Lugosi 1994), which Mathlib does not have, and a careful treatment of conditional laws at a point. One of the paper's lemmas (Lemma 6) is false as printed for unbounded ; the formalization isolates the correct statement.
The deterministic optimization part (Lemmas 5 and 6 for bounded ) is a compactness argument. The central difficulty is the probabilistic input. A natural first idea, applying the strong law of large numbers to , fails: the kNN weights depend on all of and on , the effective sample size grows sublinearly, and convergence is required for almost every simultaneously, including that are atoms of where ties are the rule. A second difficulty is the exchange of quantifiers: the strong law gives a null set depending on and on the set , and the conclusion needs one null set for all . Finally, for unbounded the minimizers of must be kept bounded, and weak convergence of alone does not do so.
All spaces are EuclideanSpace ℝ (Fin d), so kNN distances and are Euclidean. The data are a measurable, mutually independent sequence S i : Ω → ℝ^{d_x} × ℝ^{d_y} with each term of law ; samples are indexed from . The following readings are explicit in the Lean:
μ.condKernel x of the conditional law, and is its Bochner integral; Assumption 5's "for every " refers to this version, and is measurable.A formalization that replaces the conditional law by an arbitrary kernel unrelated to , takes to be a fixed measurable selection chosen outside the almost-sure quantifier, or reads on an empty set as without Assumption 3 would trivialize or weaken the result and is ruled out by the statements above.
Needed infrastructure: nearest-neighbour ranks and their combinatorics (Stone's lemma: a point is among the nearest neighbours of at most a bounded number of others), a strong law for kNN regression, portmanteau-type characterizations of weak convergence for weighted empirical measures, and stability of minimizers under locally uniform convergence. The kNN strong law and the stability lemmas are reusable well beyond this mission. Related platform items, credited but not reused (they concern unconditional SAA): SolutionQuality.SRP.prop1_i, SolutionQuality.SRP.prop1_ii, SolutionQuality.SRP.fbar_tendstoUniformlyOn (Bayraksan–Morton 2006) and DupacovaWets.Consistency.consistency_of_measurable_estimates (Dupačová–Wets 1988). Proofs of any milestone, and alternative routes to the goal, are welcome.
Many operations decisions are made after observing side information: an inventory manager sees weather, search trends and calendar effects before ordering; a supply-chain planner sees market signals before shipping. Bertsimas and Kallus, in From Predictive to Prescriptive Analytics (arXiv:1402.5481v4, Management Science 2020), study how to turn such data into decisions. Besides their local, weight-based prescriptions (the subject of mission 1 of this series), their §8 analyses a second approach: choose a decision rule from a structured class, such as norm-bounded linear rules, by empirical risk minimization — minimizing the average historical cost of the rule.
The question this mission formalizes is the one any practitioner of that approach must answer: how far can the true expected cost of the chosen rule exceed its in-sample cost? Classical statistical learning answers it with Rademacher complexity (Bartlett and Mendelson, JMLR 2002), but only for real-valued predictors. Operations decisions are vectors (order quantities for several products, shipments to several locations), so the paper extends the theory to multivariate decision rules.
Covariates take values in a measurable space , the uncertain quantity in a measurable space , and decisions in , unconstrained. Data are an i.i.d. sample from a probability measure on , and is its covariate part. A cost is incurred when decision meets outcome . A decision rule is a measurable map ; is a class of decision rules. Its expected cost is , and its empirical cost is , the objective of problem (4).
The empirical multivariate Rademacher complexity of (Definition 3) on a sample is
with independent uniform signs, and the marginal complexity is its expectation over the sample. For real-valued classes () these are the usual Rademacher complexities with factor and no absolute value. Lean notation: empRademacher, margRademacher, expCost, empCost, costClass in PrescAnalytics.ERM.
If and , then for any each of the following holds with probability at least :
In particular they hold for the empirical risk minimizer. The goal is stated for a general class , not only the linear rules (25).
Theorem 13 says that the quantity empirical risk minimization optimizes is, up to confidence terms that do not depend on the rule, an upper bound on the true expected cost of every rule in the class, uniformly. Bound (27) is computable from data, so it certifies a learned policy without a holdout set. Combined with complexity bounds for norm-restricted linear rules (the paper's Lemmas 2 and 3, not part of this mission), it shows the confidence terms vanish as .
The results are known: (29) and (30) for -valued classes are the standard Rademacher bounds (Mohri, Rostamizadeh and Talwalkar, Foundations of Machine Learning, Thm 3.3, after rescaling). What is new in the paper is the -norm vector comparison inequality of Lemma 1 with constant . None of these statements has a machine-checked proof on the platform. A formal development would supply a reusable symmetrization-plus-McDiarmid pipeline and a vector contraction lemma. Related items posed in this repository are Bartlett–Mendelson's Theorem 8 (RadGauss.RiskBound.theorem_8, with an absolute value in the complexity and constant ), Maurer's Euclidean vector contraction with constant (SPOBounds.Margin.maurer_vector_contraction), and the open uniform law HighDimStat.UniformLaws.uniform_law_rademacher_complexity; none is the same statement as a target here.
The uniform bound needs three ingredients: a concentration inequality for the supremum of the deviation over the class (bounded differences), a symmetrization step relating the expected supremum to the Rademacher complexity, and a comparison inequality to pass from the cost class to the decision rules. The scalar contraction principle of Ledoux and Talagrand does not apply directly, since each cost depends on a -dimensional output; applying it coordinatewise loses a factor of , and Euclidean vector contraction loses and uses the wrong norm. Lemma 1 needs an argument specific to the -norm. Measure theory adds its own difficulty: the supremum over an uncountable class must be shown measurable before its expectation or probability means anything.
Decisions are Fin d → ℝ, whose Lean norm is the -norm; , are general measurable spaces. Samples are drawn from the product measure Measure.pi (fun _ : Fin N => μ), with . The following readings are explicit:
EReal (an unbounded class gives ), marginal ones are lower Lebesgue integrals in ; .A trivializing formalization is ruled out: the quantifier over the class sits inside the probability, the complexity has no absolute value and is never a junk for unbounded classes, and the hypotheses are satisfied by a clipped newsvendor cost. Solvers will need McDiarmid's inequality, symmetrization with a ghost sample, and the comparison lemma; each is reusable for any Rademacher-based generalization bound. Formalizations of these tools as separate lemmas are welcome.
Smooth optimization with nonnegative variables appears when the variables are Lagrange multipliers for inequality constraints or when an objective incorporates an augmented Lagrangian or an exact penalty. Bertsekas studies how to retain a Newton-like convergence rate in this setting while using an iteration that projects a scaled gradient step onto the nonnegative orthant. His 1982 paper also discusses large optimal-control examples, where repeatedly solving a quadratic subproblem may be costly. These are the applications motivating the method, rather than assumptions of the theorem. Bertsekas, 1982.
The paper contrasts a partly diagonal scaling matrix with two other approaches: a fully diagonal projected gradient step, which generally has a linear rate, and a constrained Newton step defined by a quadratic program. The main theoretical question is whether the simpler projected iteration can still identify binding coordinates and converge superlinearly near the solution. The mission covers the nonnegative-orthant method in §2 and its stated convergence results. The paper's later extension to general linear constraints and its computational examples concern different objects. Bertsekas, 1982.
Fix a dimension and a continuously differentiable function . Problem (1) minimizes over the nonnegative orthant . The positive part replaces each negative coordinate of by zero. A feasible is critical when every partial derivative is nonnegative and wherever . This is the paper's componentwise first-order condition.
For a feasible iterate , the binding set is . The paper selects a larger working set using a fixed and the projected-gradient residual , where is fixed, diagonal and positive definite. More precisely, contains the indices with and . The matrix is symmetric positive definite and has zero off-diagonal entries in the rows indexed by . The projected arc and update are
Here , and is the first nonnegative integer passing the paper's two-sum Armijo test (37), with . One sum uses the scaled gradient outside ; the other uses the actual projected displacement on . These details define the algorithm whose rate is at issue. Bertsekas, 1982, pp. 228–229.
The first targets establish the fixed-point and descent properties of the projected arc, positivity of the Armijo right-hand side, well-defined step selection, criticality of limit points, and local attraction with finite binding-set identification. Proposition 3 identifies both the working set and the actual binding set:
The goal is Proposition 4. Let be convex and , let be the unique minimizer on satisfying Assumption (C), and suppose the Hessian quadratic form has uniform positive lower and finite upper bounds on the initial, unrestricted sublevel set. The scaling matrix is , where retains Hessian entries except for off-diagonal entries touching . Then
If the Hessian is Lipschitz in a neighborhood of , the same proposition states an at-least-quadratic error bound: eventually for some . The separate final milestone records the paper's claim that the initial unit trial is eventually accepted. Bertsekas, 1982, pp. 233–236.
Proposition 4 says that this specific orthant-projected Newton iteration converges to the unique constrained optimum with a superlinear rate under its stated smoothness and curvature conditions. Proposition 3 supplies a distinct finite-identification statement: the working and binding coordinates eventually match those at the optimum. These facts specify the behavior of an algorithm that does not define its direction by solving a quadratic program at every step. The paper proves the preceding propositions and states Proposition 4 with its proof left to the reader, referring to its earlier discussion and standard unconstrained Newton results. Bertsekas, 1982, pp. 234–236.
Formalizing the claims would provide machine-checked statements and, once solved, proofs for the exact projected arc, two-part line search, matrix selection, identification result and rate conclusion. The local mission items are open proof obligations; their compilation checks the definitions and theorem types, not the mathematical claims. The geometry definitions can also support other orthant-constrained algorithms, while the enlarged working set and Armijo rule belong to this paper's method.
A positive definite matrix by itself does not make projection along a descent move. An off-diagonal coupling can push coordinates against the boundary in a way that defeats the usual unconstrained descent calculation; the paper gives such a situation before Proposition 1. The partly diagonal condition is therefore substantive. A second obstacle is that the exact active set can jump at a boundary point: iterates approaching that point from the interior need not have the same indexed rows. The enlarged and its dependence on the residual are central to the finite-identification and rate claims. Bertsekas, 1982, pp. 225–229.
Lean represents as EuclideanSpace ℝ (Fin n), with the Euclidean norm and zero-based coordinates. The dimension is positive. gradient and the derivative of gradient represent first and second derivatives; the paper's is diag μ with every . The run predicate includes a feasible initial point and the first acceptable integer , and the matrix choices are indexed by iteration. Propositions 1–3 use the paper's explicit admissibility condition. Proposition 4 constructs from and does not assume its invertibility, admissibility, convergence or eventual active-set equality.
Assumption (C) includes local smoothness, curvature bounds on directions zero at the binding coordinates, and strict complementarity. A local minimum is required to be feasible as well as locally minimal on the orthant. Limit points use subsequential convergence. Superlinearity uses a uniform eventual error inequality, which also covers an iterate that reaches the solution exactly; a ratio with a zero denominator would distort this case. The paper's Proposition 4 display mistakenly binds a direction to the level set while leaving the Hessian's point free. The formalization states the intended reading: every point in the unrestricted initial level set and every direction satisfy the Hessian bounds. The displayed level set has no restriction, so neither does the Lean hypothesis.
A definition that accepts any Armijo exponent or a goal that assumes the eventual identification or convergence conclusion would erase the paper's claim. Contributions can build the matrix and projected-arc lemmas, the convergence and identification proofs, and the final rate proof. The local inverse-Hessian observation before Proposition 4 is discussed in the notes but has no separate milestone until its full local setting can be captured without weakening it.
Many operations problems are decided in two stages: a first-stage decision is fixed before an uncertain quantity is revealed, and a second-stage (recourse) decision is chosen afterwards. Two classical ways to optimize such a problem differ in how they treat the uncertainty. Two-stage stochastic optimization minimizes the expected cost under a probability distribution over scenarios, with a recourse decision adapted to each scenario. Robust optimization fixes a single solution that must be feasible for every scenario in an uncertainty set, and minimizes the worst-case cost. The robust problem is usually far easier to solve, but it is conservative; the question is how much it can lose.
Bertsimas and Goyal (Math. Oper. Res. 35(2), 2010) answer this for uncertain right-hand sides. Their main positive result (Theorem 2.1) bounds the stochasticity gap: if the uncertainty set and the probability measure are both symmetric, the robust optimum is at most twice the stochastic optimum. This mission formalizes the companion negative result, Theorem 2.6: once the uncertainty set is not symmetric, the gap is not bounded by any constant. The example is the simplest non-symmetric set in practice, the corner of the unit simplex, with the uniform distribution on it. It shows that the symmetry hypothesis in the positive result is not an artefact of the proof.
Fix matrices , and costs , . Let be a set of scenarios, the right-hand side realized in each scenario, and the uncertainty set. Let be a probability measure on .
In general some coordinates of and are required to be integers; in this mission's instance there are none. A set is symmetric (Definition 1.2) if some satisfies for every .
The instance of Theorem 2.6 has no first stage (, so , ), , , and . The uncertainty set is the corner simplex (2.29)
and is the uniform probability measure on it: .
On this instance,
The constant is the paper's, and it is exact: the robust optimum is and the stochastic optimum is at most .
The result. Together with Theorem 2.1, Theorem 2.6 locates the boundary of the paper's positive theory. Theorem 2.1 says a static robust solution loses at most a factor of against the fully adaptive stochastic optimum under symmetry; Theorem 2.6 says that without symmetry the factor can be , hence arbitrarily large as the dimension grows. The paper's later results (the bound for "positive" uncertainty sets, Theorem 2.7) are motivated by this example: some structural condition replacing symmetry is necessary. The same instance also separates the adaptive problem from the stochastic one (p. 21), which shows that the gap comes from comparing a worst case with an expectation, not from the lack of adaptivity.
Formalizing it. The theorem is proved in the paper; no machine-checked version exists. The formalization adds two things beyond the paper. First, it pins down the problems as optimization problems over integrable policies with values in the extended reals, so that the inequality cannot hold for a degenerate reason. Second, it requires the volume of the corner simplex and the first moment of a coordinate on it, which the paper calls "standard computation". Neither is in Mathlib at the time of writing: Mathlib has the standard simplex as a convex set but no volume formula for it.
The optimization part is short: one feasible stochastic policy and the vertices of the simplex give both bounds. The work is in the measure theory. The volume and the moment are iterated integrals with variable upper limits, and the paper calls them "standard computation"; as statements about Lebesgue measure on they are dimension-dependent identities that Mathlib does not contain, for the simplex or for the convex hull of points. The other technical point is the scenario model: the uniform measure lives on , while the integrals live on , so the expectation must be moved through the push-forward of by .
Fin k → ℝ with the componentwise order; products are A *ᵥ x and c ⬝ᵥ x. The paper's -th coordinate is index of Fin n, and is lastUnit n.EReal infima over the feasible set, equal to when the problem is infeasible. No optimal solution is assumed to exist.Needed infrastructure: the volume of the corner simplex in and the integral of a coordinate over it (reusable well beyond this mission, for example for Dirichlet distributions and order statistics), and the change of variables from to through the push-forward. Contributions of either simplex integral, in any form that implies the stated milestones, are welcome.
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.