Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Robust dynamic programming replaces the single transition law of a Markov decision process by a set of laws, and values a policy by its worst-case expected reward over that set. Iyengar (Robust dynamic programming, CORC Tech Report TR-2002-07, 2004; Math. Oper. Res. 30(2), 2005) and Nilim and El Ghaoui (Robust control of Markov decision processes with uncertain transition matrices, Oper. Res. 53(5), 2005) showed that under a rectangularity assumption the robust value satisfies a robust Bellman equation. Each step of that equation solves, for every state–action pair, an inner problem
the worst-case expectation of a value vector over the ambiguity set . Robust value iteration is only as practical as this inner problem is cheap.
The ambiguity sets of interest come from statistics: when transition probabilities are estimated from data, natural sets are confidence regions around the empirical distribution. Section 4 of Iyengar's report studies three such families: relative-entropy balls (Lemma 4), a χ² approximation of them (Lemma 5), and an outer approximation (Lemma 6). This mission formalizes the χ² case. The relative-entropy case is already posed on the platform as RobustMDP.EntropyInner.kl_ball_inner_problem_dual (Nilim–El Ghaoui series), up to the sign change .
Let be a finite set of states and let be the probability measures on . For and write
Fix a centre with for every (in the paper is the empirical next-state distribution of one state–action pair) and a radius . The χ² set (46) is
Since , the relative entropy is at most the χ² distance, so lies inside the relative-entropy ball of radius : it is a conservative approximation of it. The Lean development names these objects expect, variance, chiSqDist, chiSqSet, relEntropy and the dual objective dualObj q t v μ , all in the namespace RobustDP.ChiSquare.
For every value vector ,
where ranges over vectors with componentwise. Both extrema are attained. The lemma's complexity claim, for (48), is a statement about an algorithm and is not part of the mission.
Two further results stand on the same definitions: the inequality of Section 4.2, and the analogue of Lemma 5 established in the proof of Lemma 6 (p. 20):
The result. Lemma 5 reduces a worst-case expectation over a curved convex set of probability vectors to a concave problem in one scalar, which the paper solves by sorting. This makes robust value iteration with χ² ambiguity sets about as expensive as nominal value iteration, up to a logarithmic factor. The identity also explains the shape of the answer: a mean minus a standard-deviation penalty, applied to a value vector truncated from above at the level . The truncation comes from the constraint .
Formalizing it. The result is proved in the paper; no machine-checked proof is known. A complete formalization gives a verified finite-dimensional duality theorem for a quadratic constraint combined with polyhedral constraints, which is the computational core of χ²-ambiguity robust MDPs and of χ²-divergence distributionally robust optimization in general. Lemma 6's printed formula (57) is false (see below); the mission poses the corrected identity that the paper's proof establishes.
The obvious argument drops the constraint . Without it, the minimum of the linear function over the ellipsoid follows from Cauchy–Schwarz and equals . The page notes (p. 19) that earlier work solved only this relaxed problem. With the minimizer of the relaxation can leave the simplex, so the problem has an ellipsoidal constraint, a polyhedral constraint and an equality at once. The multiplier of is what Lemma 5 has to handle. Equality of the primal minimum with the dual supremum needs a duality theorem that is not in Mathlib in this form. Attainment of the dual maximum over the unbounded cone needs an additional argument, namely that an optimal multiplier has the truncation form (53).
Fintype; vectors are functions S → ℝ; is Mathlib's stdSimplex ℝ S. Nonemptiness of follows from . Finiteness is the standing restriction of Section 4 (p. 15).IsLeast and IsGreatest of image sets, so the goal asserts attainment on both sides, as the page's "minimize" and "max" do.0 ≤ μ). The multiplier of the equality ranges over . The page's "" in (50) is a misprint: the proof of Lemma 6 writes , and the optimal may be negative.⨆ over an unbounded set, would make the statement junk.The secretary problem asks how well an online decision maker can do when items arrive one at a time in random order and each must be accepted or rejected on the spot. With a single selection, the classical rule (observe a fraction, then take the first item better than everything seen) selects the best item with probability about , and no rule does better. Many allocation problems are not single-choice: a seller with identical goods facing bidders who arrive over time, an advertiser with a budget of impressions, an employer with openings. Each asks the multiple-choice secretary problem: how much of the best achievable total can an online rule collect when selections are allowed?
Kleinberg's 2005 SODA paper answered this for the sum objective. It gave a recursive algorithm whose expected total is at least times the sum of the largest values, so the ratio tends to as grows, and stated a matching upper bound for every algorithm, whose proof the extended abstract omits. The motivating application was online auctions: the algorithm becomes a strategyproof mechanism for selling identical items to bidders who arrive and depart over time, extending the single-item online auction of Hajiaghayi, Kleinberg and Parkes (EC 2004).
Timeline. Dynkin (1963) and the classical literature settle with ratio . Hajiaghayi, Kleinberg and Parkes (2004) turn the single-item rule into an online auction. Kleinberg (2005) proves for selections, with the explicit constant . Babaioff, Immorlica, Kempe and Kleinberg (2008) survey the resulting family of generalized secretary problems and their use in online auctions.
Let be a finite set of distinct non-negative real numbers. The elements of are revealed in a uniformly random order: each of the orders has probability . After each arrival the algorithm decides, irrevocably and using only the values seen so far, whether to select it. At most elements may be selected. Write for the set of the largest elements of (all of if ) and
for their sum, the best total any rule could collect knowing in advance.
Kleinberg's algorithm is defined by recursion on :
The expected value of the algorithm is taken over the random order and over every binomial draw at every level of the recursion.
The statement is uniform in and ; it says nothing beyond the explicit constant printed in the paper.
The paper proves the theorem by induction on . Its sketch introduces , the set of the first arrivals, , the modified value of a set (the sum of its elements lying in ), and , the number of elements of exceeding . The milestones are its stated claims, in order:
The result. Theorem 2.1 shows that random arrival order costs only a factor when many items are sold, against the constant for a single item. With the paper's matching upper bound, it pins down the optimal rate for the -choice problem. It is the base of the paper's strategyproof online auction for identical goods and a standard reference point for the later literature on secretary problems with combinatorial constraints and on online allocation in the random-order model.
Formalizing it. The paper is a two-page extended abstract, and the theorem's proof is a sketch: several steps are described as "easy", a stochastic-domination argument is stated without detail, and the behaviour of the algorithm when fewer than elements have been observed is not specified. A machine-checked proof would supply the complete argument for the explicit constant. The result is proved on paper only in this sketch; no machine-checked proof of it is known.
The obvious argument fixes and treats the threshold as if it split the remaining elements exactly. Both steps fail. With a fixed , the first arrivals are not a uniform subset of and is hypergeometric, so the clean binomial computations of the sketch are not available; the binomial choice of is what makes uniform. And the number of later elements beyond fluctuates by order : the second phase may run out of budget before reaching all of , or accept elements outside . Controlling this fluctuation, while the cap of also counts the first phase's selections, is the central step. The induction must then combine a recursive guarantee on a random, random-sized prefix with this estimate.
The Lean development fixes these conventions.
Finset ℝ with all elements non-negative; distinctness is automatic. The arrival at time (0-based) under the order is the -th smallest element of , and expectations over the order use the published uniform average SecretaryWD.DiscUpper.uniformAvg.PMF over sets of selected positions, defined by well-founded recursion on . The base case is the published SecretaryWD.DiscUpper.classicalSecretary. is Mathlib's PMF.binomial (1/2). At the algorithm selects nothing, for totality only; all statements assume .A complete development needs: the uniform-subset law of a binomially sized random prefix; conditional expectations over random subsets; tail and absolute-deviation bounds for sums of geometric variables and a stochastic-domination argument; and a careful treatment of the recursion through PMF.bind. The first and third are reusable beyond this mission, for other random-order and sample-based algorithms. Proofs of any milestone, of auxiliary lemmas about the random prefix, and of the goal by a route different from the sketch are all welcome.
Finite games in strategic form are the basic model of interaction between self-interested agents in economics, engineering and computer science. Among them, potential games (Monderer and Shapley, 1996) are the class with the most tractable equilibrium behaviour: every finite potential game has a pure Nash equilibrium, and simple learning dynamics such as best response and fictitious play converge to one. A natural question is what lies at the opposite end of the space of games, and how far a general game is from that tractable class.
Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405; Mathematics of Operations Research 36(3), 2011, DOI 10.1287/moor.1110.0500) answer this with a canonical decomposition of every finite game into a potential, a harmonic and a nonstrategic component, obtained by viewing the payoff differences of a game as a flow on a graph and applying the combinatorial Helmholtz decomposition. Harmonic games, those whose potential component vanishes, are the complement of potential games, and the paper shows that their equilibrium behaviour is opposite as well. This mission formalizes the first such result: harmonic games generically have no pure Nash equilibrium, so the guaranteed existence of pure equilibria in potential games has no counterpart on the harmonic side. The decomposition has since been used to study near-potential games and the convergence of learning dynamics in them.
A finite game has a finite set of players with and, for each player , a nonempty finite strategy set with elements. A strategy profile is , and denotes with player 's strategy replaced by . The utilities assign to each player a function ; for fixed and a game is identified with its utilities, an element of , where carries the inner product .
A profile is a pure Nash equilibrium if for every player and every .
Two profiles are -comparable if they are distinct and differ only in player 's strategy. The game graph has the profiles as nodes and joins every comparable pair. An edge flow is a function on ordered pairs of profiles with on edges and off edges; the space of edge flows carries . The combinatorial gradient is , with the edge indicator, and is its adjoint. Restricting to -comparable pairs gives , and is the flow of payoff differences of the game . With (Moore–Penrose pseudoinverse) and , the paper's Definition 4.2 sets
A game is a harmonic game if : its payoff differences form a flow with no source or sink at any profile.
For finite games in which at least two players have at least two strategies each, and for any additive Haar measure on the finite-dimensional space ,
This is the paper's "harmonic games generically do not have pure Nash equilibria", with "generically" read as the paper defines it: true except on a set of measure zero within the harmonic games.
For each profile , the harmonic games having as a pure Nash equilibrium form a proper linear subspace of . The exceptional set of the goal is then a finite union of lower-dimensional subspaces.
The result separates harmonic games sharply from potential games. A finite potential game always has a pure equilibrium; a harmonic game almost never has one. Together with the decomposition theorem, it says that the obstruction to pure equilibria in a general game is carried by its harmonic component, and it motivates the paper's later results on mixed equilibria of harmonic games (the uniformly mixed profile is always a mixed equilibrium). Proposition 4.1, a milestone here, also gives the dimension of the harmonic games, , and so measures how large that class is.
The results are proved in the paper; none of them is machine-checked. Formalizing them requires the paper's operator layer (flows on the game graph, the gradient with its adjoint, pseudoinverses) in Lean for the first time, and pins down two points the paper leaves informal: the measure with respect to which "generically" is meant, and the shape condition on the game under which the statement holds.
Lemma 5.1 is a short counting argument once the divergence-free condition is unpacked, but unpacking it requires knowing that kills and computing from the -weighted inner product. The main obstacle of the goal is showing that the exceptional subspaces are proper. The proof needs a harmonic game with nonzero payoff differences, that is , and the only route the paper offers is the dimension count of Proposition 4.1. That count rests on the full decomposition , on the kernel of each and on the connectivity of the game graph, all of which must be built in Lean. The measure-theoretic last step, that a finite union of proper subspaces is Haar-null, is in Mathlib.
A tempting shortcut fails: placing Lebesgue measure on all of and observing that is a proper subspace would prove the goal without saying anything about equilibria.
Players form a finite type ι with decidable equality, and the strategy sets E m are nonempty finite types, as in the paper (). A game is an element of PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)), with the unweighted sum inner product of p. 14. is the subspace of edge flows with the inner product of (7). is Mathlib's adjoint, and the pseudoinverse is defined directly as the inverse of on composed with the orthogonal projection onto . are defined by (28), not by the alternative description (29). Harmonic games are the submodule H ⊔ N, and pure Nash equilibrium is AGT.IsPureNash from the published agt_games definitions.
Added hypothesis. The paper leaves implicit that at least two distinct players have at least two strategies each. Its proof uses this through "dimension of is larger than zero". Without it Proposition 5.1 is false: with two players having and strategies, , every harmonic game is nonstrategic, and every profile is a pure equilibrium of every harmonic game. The goal and the structural theorem therefore carry this hypothesis explicitly.
The measure. The measure is an arbitrary additive Haar measure on the subspace itself, with the Borel σ-algebra of its subspace topology. A measure on the ambient would make the statement trivial, because the whole subspace is null there. Proposition 4.1 is stated as equalities in , so that and the subtraction in part 2 are not truncated.
Needed infrastructure: kernels of the (the paper's Lemma 4.2), the projection property of , the decomposition theorem, and the connectivity of the game graph. The operator layer is shared with the other missions of this series and is reusable for any work on flows on graphs. Proofs of the milestones, and of the structural form independently of the goal, are welcome.
The capacitated vehicle routing problem (CVRP) asks for delivery routes from a depot that serve every client exactly once without exceeding a vehicle capacity, at minimum total length. It was introduced by Dantzig and Ramser in 1959 and is the reference problem of the vehicle routing literature: most exact methods for richer routing models (time windows, heterogeneous fleets, split deliveries) are first developed and benchmarked on it.
Exact CVRP algorithms are driven by the lower bound of a linear relaxation. Two families dominated before 2005. Branch-and-cut works with the edge variables and the rounded capacity inequalities (Lysgaard, Letchford and Eglese 2004, among others); its bound degrades as the number of vehicles grows. Lagrangean and column-generation methods work with q-routes, walks from the depot of bounded total demand that may revisit clients (Christofides, Mingozzi and Toth 1981). Fukasawa, Longo, Lysgaard, Poggi de Aragão, Reis, Uchoa and Werneck combine the two in one linear program over the intersection of the two polytopes, priced by column generation with every cut written on the edge variables. According to the abstract, the resulting branch-and-cut-and-price solves to optimality all instances from the literature with up to 135 vertices. The design is called robust because cuts are written on the edge variables and therefore never change the structure of the pricing problem.
This mission formalizes the formulation itself (§2 of the paper) and the two exact facts of its column generation (§3.1).
Let be an undirected graph on . Vertex is the depot; are the clients, client having a positive demand . Each edge has a length . There are vehicles of capacity , both positive integers.
A list of clients describes the closed walk . Its edge incidence is the number of times the walk traverses (a one-client walk traverses twice); its load is , with repetitions.
For , is the set of edges with one end in , , and . The paper's constraints on and on weights of the q-routes are
is ; is the set of satisfying (1) together with some satisfying (5), (6); the Explicit Master is the projection onto of the system (1)–(6) with one . The Dantzig–Wolfe Master (DWM) is the LP in alone obtained by substituting (5) into (1)–(4), giving the rows (8)–(11), with objective (7) . The bounds are .
For a loop-free graph with positive demands and capacity, and arbitrary lengths:
with (7) equal to . The bounds are stated in lower-bound form: every lower bound of over or is one over , and every lower bound over is at most the cost of every solution.
The formulation theorem is what makes the algorithm exact: integer points of are solutions, so branching on terminates at an optimum, and is a relaxation, so is a valid bound that dominates both classical bounds. The DWM description is what makes it computable: is optimized by column generation over q-routes, and milestones 8 and 10 show that any cut on can be added without changing the pricing problem, which remains a shortest q-route problem with edge costs .
The paper proves none of these claims formally; most are stated in a sentence, and milestone 9 is stated with "It can be shown" and no proof. To our knowledge none of them has a machine-checked proof. A formal development produces a library of walks, edge incidences, cut values and column families on a general graph that later missions on branch-cut-and-price (subset-row cuts, ng-routes, other routing variants) can import.
Most items are linear-algebra bookkeeping on finite sums, but they require a working theory of walks: edge incidences along a closed walk, the cut value of an incidence vector, and the fact that a walk from the depot crosses every client set an even number of times. The integrality statements (milestones 5 and 9 and goal part 1) are the hard part: an integer vector satisfying degree constraints need not come from routes through the depot, and the statements must exclude every other structure. For there are no capacity cuts at all, so the capacity of the routes must be recovered from the columns, and the paper states this case without proof. The obvious reduction "an integer point of is an integer combination of q-routes" fails: may be fractional even when is integral.
Vertices are Fin (n+1) with depot 0; edges are Sym2 (Fin (n+1)); the graph is an edge set E assumed loop-free where needed. Edge vectors are functions on all unordered pairs that vanish off E, which encodes . Demands , and are natural numbers; positive demands, and (the paper's standing assumptions, p. 1) are carried by the integrality statements and the goal, while is used by no statement and is omitted. Loads count repeated visits. The cut value , the demand and are the published definitions LysgaardCVRP.Shrink.cut, .demand and .roundedCapacityBound. The matrix is replaced by finitely supported weights on client lists ranging over all q-routes without 2-cycles. and OPT are never real infima, since is empty for infeasible instances.
Three trivializations are ruled out by construction: is defined from the Explicit Master display, not as ; a CVRP solution is defined by its routes, not as an integer point of a polytope; and the columns are not a fixed finite list, which would turn into a restricted master.
The strictness of "CVRP routes q-routes" (p. 2) depends on the instance and is not stated. Contributions of reusable lemmas on walks and cut values of incidence vectors are welcome, as are proofs of any milestone.
Potential games (Monderer and Shapley, 1996) are the finite games whose incentives are captured by a single function on strategy profiles: every unilateral change of strategy changes the deviator's payoff by exactly the change of a common potential. They have pure Nash equilibria, and natural learning dynamics such as better-reply and fictitious play converge in them. Most games are not potential games, however, and before Candogan, Menache, Ozdaglar and Parrilo there was no canonical way to say how far a given game is from one, or what the remainder looks like.
Their paper (arXiv:1005.2405; Math. Oper. Res. 36(3), 2011) answers this by viewing a game as a flow on a graph. The payoff differences between profiles that differ in one player's strategy form an edge flow on the game graph, and the classical Helmholtz (Hodge) decomposition of edge flows into gradient, harmonic and curl parts (Jiang, Lim, Yao, Ye, 2011) pulls back to a decomposition of the game itself. Every finite game becomes the sum of a potential game, a harmonic game and a component that carries no strategic information. The decomposition is the basis for the rest of the paper (equilibria of harmonic games, projections onto potential games, approximate equilibria) and for later work on dynamics in near-potential games.
Fix a finite set of players and, for each player , a finite nonempty strategy set with elements. A strategy profile is , and denotes the strategies of the players other than . A game is a family of utilities with , so the space of games is , where with .
Two profiles are -comparable if they are distinct and differ only in player 's strategy. The game graph has the profiles as nodes and an edge between comparable profiles. An edge flow is a function that is antisymmetric on edges and zero off edges; the space of edge flows carries . Triangular flows live on ordered 3-cliques.
The operators are: the gradient , with the edge indicator; the curl on 3-cliques; the per-player gradient , with the indicator of -comparability; and , , the flow of pairwise comparisons of . Adjoints are written and Moore–Penrose pseudoinverses . The space carries the unweighted inner product . Further, , , , and .
A game is normalized if for all and (Definition 4.1). The potential, harmonic and nonstrategic subspaces are (Definition 4.2)
and every game splits as with
where is a potential function of , i.e. .
Lemma 4.6 (the unique normalized game with the same pairwise comparisons is ) is included as a supporting theorem.
The decomposition turns questions about a game into questions about its three components. The potential component inherits the equilibrium and convergence theory of potential games. The harmonic component has a sharply different structure: harmonic games generically have no pure equilibrium, and in each of them the uniformly mixed profile is a mixed equilibrium. The nonstrategic component does not affect any equilibrium notion. The closed-form expressions also give the potential game closest to a given game, and with it bounds relating the approximate equilibria of the two games. The other missions of this series formalize those consequences; all of them rest on the operator layer and the subspaces defined here.
Theorem 4.1 is proved in the paper; to our knowledge it has not been machine-checked. A formal development produces graph-flow infrastructure that Mathlib does not yet have: edge and triangular flows with their inner products, the combinatorial gradient and curl, the Helmholtz decomposition of a finite graph, and an operator Moore–Penrose pseudoinverse on finite-dimensional inner product spaces. The paper leaves Theorem 3.1 to the literature, so a full development needs a proof of it. The pseudoinverse identities of Lemma 4.4 also have a short appendix argument in the paper that a formal proof has to make complete.
The decomposition is not orthogonal decomposition along a single map. The subspaces and are defined through , which is assembled player by player from the , while the flow conditions involve and the combined operator . Connecting the two requires the player operators to have mutually orthogonal ranges ( for ) and the explicit form of as a scaled projection. Without these, (Lemma 4.4 (iv)) and (Lemma 4.4 (v)) are not available, and they are what make the formulas for and land in and . A direct attempt to apply the Helmholtz decomposition to produces a flow decomposition, not a game decomposition; the pullback through is not formal, because is neither injective nor surjective.
Players form a Fintype ι; strategy sets are E : ι → Type with Fintype, DecidableEq and Nonempty instances, and is Fintype.card (E m). Profiles are ∀ m, E m, and is Function.update p m q. The game graph is a Mathlib SimpleGraph; comparability requires , so the graph has no loops, as the Laplacian (15) requires. is EuclideanSpace ℝ on profiles. and are type synonyms of the subspaces of antisymmetric (resp. alternating) functions, with inner products built from (7), including the factor on . Lemma 4.4 (i) fails without it. The space of games is PiLp 2 of copies of , whose inner product is the unweighted sum used on p. 14, not the weighted inner product of the paper's Section 6. Adjoints are LinearMap.adjoint. The pseudoinverse is defined explicitly as the inverse of on composed with the orthogonal projection onto .
, and are defined by (28), not as the ranges of the component maps; the direct-sum part of the goal is stated independently of the formulas, so the goal cannot be satisfied by construction. Lemma 4.4 is split into five items, one per identity. "Orthogonal decomposition" in Theorem 3.1 is stated as pairwise orthogonality plus spanning. The paper's statements have no hypotheses beyond the setting, and none were added except nonemptiness of the strategy sets, which the paper assumes by writing .
Welcome contributions: a proof of the Helmholtz decomposition on a finite simple graph, general facts about the pseudoinverse (Penrose identities, is the projection onto , invariance under rescaling of inner products), and the explicit adjoint formulas (12) and (22).
Firms that buy from unreliable suppliers can protect themselves in two ways: they can spread orders across several suppliers, or they can invest in improving a supplier's reliability, for example through supplier-development programmes or joint process-improvement projects. Wang, Gilland and Tomlin (MSOM 12(3):489–510, 2010) compare the two strategies in a newsvendor model with random supplier capacity.
This mission formalizes one part of that comparison: single sourcing with improvement, in which improvement efforts may fail. The firm must then decide when to choose its supplier. Under early commitment it picks one supplier, invests in it, and buys from it whatever the outcome. Under late commitment it invests in both suppliers, observes which efforts succeeded, and only then buys from the better one. Empirical work on supplier development documents both practices and the reluctance of suppliers whose improvement efforts previously failed (Handfield et al. 2000, as cited by Wang et al. 2010, p. 496; Krause et al. 2007). The question is how much the option to postpone the choice is worth.
A firm sells a single product over one season. It earns a unit revenue , salvages leftovers at , and pays a penalty per unit of unmet demand, with . Demand is nonnegative with finite mean.
Supplier has design capacity , unit cost and committed-cost fraction . Its capacity loss has a continuous distribution that depends on a reliability index ; a higher index means a stochastically smaller loss. An order delivers . The firm pays , and the realized profit of single sourcing from is
The second-stage expected profit is , and is its optimal value.
Improvement. Supplier starts at index . Effort to reach index costs , where is convex and increasing with . The effort succeeds with probability ; on failure the index stays at .
and .
Let the suppliers be identical except for their unit costs, , with common , , and , and let be an optimal early-commitment index of supplier 2. Then
The results identify when the flexibility of postponing supplier selection has value. Late commitment never hurts. It has no value when one supplier dominates the other, even after the other's improvement. For suppliers that differ only in cost, Theorem 5 gives a checkable sufficient condition for strict value. The condition weighs the gain from switching in the outcome "the costlier supplier improves, the cheaper one does not", which has probability , against the cost of improving the costlier supplier. Together with Lemma 4 the results say that keeping the choice open lowers the reliability target but can raise expected profit. Corollary 3(a) says this value is easiest to obtain when costs are close.
The paper's proofs are in an online appendix that is not used here, and none of these statements has a machine-checked proof. The mission produces formal versions of the statements, with the hypotheses that the printed versions leave implicit made explicit (see Formalization scope), and invites proofs of them.
The late-commitment profit (9) is a probability-weighted sum of maxima of two optimal-value functions. It is "neither concave nor unimodal" (p. 498), so first-order conditions do not characterize its optimum, and optimizers need not be unique.
Everything is in the namespace MitigateSupplyRisk.LateCommit, with one definition module Model.
sSup over the feasible set. The sign conventions , make these sets bounded above, so no supremum is a junk value, and no optimum is assumed to be attained.Supplier record (committed cost, capacity, loss family) and the same Improvement record ().IsMaxOn), never as claims.Proofs of the milestones are welcome. A reusable lemma, that the supremum of expectations is monotone under first-order stochastic dominance of the loss, would serve the other missions of this series too.
Automatic program analyses for heap-manipulating code have to infer, for each procedure, a precondition describing the memory the procedure needs. Calcagno, Distefano, O'Hearn and Yang (J. ACM 2011) do this with bi-abduction: at a call site the analysis asks for an anti-frame , the missing memory, and a frame, the memory left untouched, so that the current state together with meets the callee's precondition. Their tool, Abductor, and its successor Infer, derive specifications compositionally, procedure by procedure, without a whole program.
A natural question is what the inferred preconditions mean. The paper's informal answer is that the analysis aims at footprints: descriptions of the cells a program actually uses. §4.2.4 makes this precise for straight-line sequences of actions: if each precondition is precise and the prover always returns the best anti-frame, the inferred precondition is exactly the footprint. That result rests on the semantic theory of best abductive solutions developed in §3.3: with respect to a natural order, the abduction question has a unique best solution, .
A heap is a finite partial map from locations to values; a stack maps variables to values; a state is a stack–heap pair . A predicate is an arbitrary set of states. Write when have disjoint domains and is their union, and for a subheap. The separating conjunction holds of when with and ; is the set of all states; the separating implication holds of when every disjoint with gives . Entailment is inclusion.
A solution of the abduction question is any predicate with . Solutions are compared by the spatial preorder and the betterness order
The minimal states of are : the states such that no proper subheap has .
An action is given by its specification , a pair of predicates. A predicate is precise if every has at most one subheap with . For a nonempty sequence of actions, the safe states and the footprint are
The canonical precondition of a sequence, as computed by an ideal bi-abductive prover, is for a single action and for , where is the best solution of .
If every precondition of the sequence is precise and every anti-frame is a -best solution, then
Theorem 3.13 gives the abduction question a canonical semantic answer, and it is the yardstick for every algorithm in the paper: the heuristic procedure of §3.2 is shown not to reach it, and the systematic procedure of §3.4 is proved to compute it on a restricted fragment. Theorem 4.11 connects this semantic optimum to program analysis: on straight-line paths, bi-abduction with an ideal prover infers neither more nor less memory than the program touches. It is the paper's theoretical justification for aiming the analysis at footprints.
Neither result has a machine-checked proof that this mission knows of; the platform has no separation-logic layer at all. The mission produces a self-contained semantic layer for separation logic over a concrete heap model (finite heaps, , , , the orders and , precise predicates) that the companion mission on the systematic abduction algorithm, and later work on frame inference or footprint analysis, can share. The paper proves both results; the work here is to formalize those proofs.
Most steps are short once the definitions are fixed, and the paper states several of them as "immediate". Two points are not. First, and the "if" direction of Lemma 3.10(3) need every state of to lie above a minimal one; this holds because heaps are finite, so the subheap order is well founded, and fails for infinite heaps. Second, the inductive step of Theorem 4.11 passes through and through distributing over a precise -factor. Precision of is what forces the split of a minimal heap of to be unique; without it, the two sides of the displayed chain on p. 50 differ. The induction must carry precision for every action of the tail.
Lean represents values and variables as natural numbers, with as nil and the nonzero naturals as locations; a heap is a cell map ℕ → Option ℕ with cell 0 = none and finite domain; disjoint union is a relation. Predicates are Set (Stack × Heap), entailment is ⊆, and is Set.univ. Program and logical variables are not distinguished, and actions carry no parameters, as in §4.2.4; the stack is the same on both sides of every connective. "The minimal solution w.r.t. " is the -least solution, competing against every predicate, not only symbolic heaps. A sequence of actions is a head action plus a tail list, so the empty sequence never occurs. Theorem numbers and pages are those of the accepted manuscript of the J. ACM article (pp. 1–72, footer "Journal of the ACM, Vol. V, No. N, May 2011"), not of the typeset Article 26.
The paper does not define "the canonical spec" in §4.2.4. The formalization reads it from the proof of Theorem 4.11, as an inductive relation whose anti-frames are arbitrary -least solutions. Defining the anti-frame as would build Theorem 3.13 into the definition, and dropping precision, allowing infinite heaps or restricting the competitors in the definition of a best solution would change the theorem; all of these are ruled out.
Needed infrastructure: the heap model with union and subheap lemmas, well-foundedness of strict subheap inclusion on finite heaps, the adjunction between and , and upward closure of . Reusable pieces, such as the heap model, the adjunction and the properties of , are welcome as separate lemmas.
Two-stage and multistage stochastic programs ask for decisions that react to uncertainty revealed over time. When the distribution of the uncertainty is known only partially, one optimizes against the worst distribution in a family consistent with what is known: a support set, a range for the mean, a covariance matrix, bounds on how fast the tails decay. Goh and Sim (Oper. Res. 58(4), 2010) show that once linear and deflected linear decision rules are imposed, the recourse costs of such models reduce to worst-case expectations of positive parts,
of affine functions of a random vector . These quantities are generally intractable, so the paper bounds them by optimization problems that are. Each kind of partial information gives its own bound, and in practice a modeller usually has several kinds at once. Theorem 4 of the paper, the target here, combines the separate bounds into a single one that uses all of the information.
Timeline: Scarf (1958) gave, for a newsvendor problem, the worst-case expected positive part of a scalar with known mean and variance. Chen, Sim and Sun (Oper. Res. 55(6), 2007) introduced the forward and backward deviations used here to describe tails of independent components. Chen and Sim (Oper. Res. 57(2), 2009) introduced the combination of bounds by infimal convolution that Theorem 4 restates in the present setting. Goh and Sim (2010) assemble the three kinds of information into one model and use the combined bound for their bideflected linear decision rules.
A distribution is a probability measure on , the law of the uncertain vector ; its mean is . Fix data: sets , matrices , , , a vector , a set and vectors in . Three families encode three kinds of information:
are at most and .
The bounds are the optimal values of (21), (22) and (24) of the paper. For instance
is an infimum over with of a supremum over of a Scarf-type expression, and is an infimum over with , that involves the function
For the unified bound is the infimal convolution
All values lie in , with the paper's convention that an infeasible minimization has value and an infeasible maximization .
With ,
The tightness halves of Theorems 1 and 2 are the subject of the two companion missions of this series; Theorem 4 does not use them.
The unified bound turns heterogeneous partial information into one tractable upper bound. When a modeller knows a support set, a covariance and tail information for some independent factors, is valid for the intersected family and is never worse than the best of the separate bounds; it is the bound the paper's deflected and bideflected linear decision rules (§6, (31) onward) use for every recourse term. Theorem 4 is thus the guarantee behind the paper's main approximation scheme, and the same infimal-convolution device applies to any collection of valid bounds on a common convex objective.
The theorems are proved in the paper's electronic companion. To the knowledge of this mission none of them has a machine-checked proof: the Lean library has neither a Scarf-type bound nor a bound on expected positive parts from deviation measures. Formalizing Theorem 3 in particular produces reusable facts about moment generating functions of independent sums under deviation bounds.
The left inequality of (26) looks like bookkeeping, but it rests on three separate bounds, each with its own argument: a weak-duality argument for , a Scarf-type mean–variance inequality for , and an exponential-moment argument for that needs independence of the components of to factor a moment generating function and the deviation bounds to control each factor. Each piece must be carried out with all values in the extended reals: suprema can be , families can be empty, and a term equal to in a sum can absorb a . The right inequality depends on how each behaves at the zero objective, which for is an infimum over that is not attained. The naive idea of proving (26) by attainment of the minimum in (25) does not work: the minimum need not be attained, and the statement must hold for every feasible split.
A distribution is a Measure on Fin N_E → ℝ with IsProbabilityMeasure; is the identity map. The mean is the published MomentDRO.Conf.meanVec. and require integrable coordinates and finite second moments, so that means and covariances exist. is an almost-everywhere statement. In , independence is iIndepFun of the coordinates of ; every exponential moment is required finite; and the deviation bounds are the published predicates FwdDevLe, BwdDevLe applied to the law of each coordinate, which state for all , equivalent to the square-root form above for .
Worst cases and bounds take values in EReal; the printed "min" of (25) and "inf" of (21), (22), (24) are read as infima, without attainment. In the supremum over is taken outside the increasing exponential, which gives the same value whenever is nonempty. The index set is a nonempty Finset (Fin 3) with index for the paper's , and vector indices are 0-based.
Two hypotheses come from the paper's model rather than its theorem statements: (deviations are square roots), and for every , which follows from , , and (pp. 905, 908, 910).
The bounds are defined by (21), (22), (24) and (25) verbatim; a formalization that defines through the worst case itself, sets some to , drops the exponential integrability from , or uses real-valued suprema (which return on unbounded sets) would trivialize or falsify the statement and is ruled out.
Contributions welcome: proofs of the three upper bounds, a Scarf inequality as a reusable lemma, and the EReal lemmas about infimal convolutions of extended-real functions.
Many problems in convex optimization, variational inequalities, mechanics, traffic equilibrium and signal processing reduce to finding a zero of a monotone operator on a Hilbert space. Frequently that operator is a sum of a monotone operator and a monotone operator composed with a linear map and its adjoint, and one also wants the solution of an associated dual inclusion. The prototype is Fenchel–Rockafellar duality: with and , the pair of problems is and .
Before this paper, splitting methods for the primal problem needed to be single-valued and smooth (forward–backward, or Tseng's forward–backward–forward method), or needed the resolvent of , which has no closed form in terms of and in general. Briceño-Arias and Combettes (arXiv:1011.5517, SIAM J. Optim. 2011) observed that the primal–dual pair is equivalent to a single inclusion on the product space involving a maximally monotone operator plus a bounded skew linear operator. Applying an inexact forward–backward–forward method to that inclusion gives the first algorithm that solves the primal and dual inclusions simultaneously and uses , and separately. Later primal–dual methods, including those of Combettes–Pesquet (2012), Vũ (2013) and Condat (2013), build on this construction.
Let and be real Hilbert spaces. A set-valued operator assigns to each point a subset; its graph is , its inverse has graph , and . is monotone if whenever , , and maximally monotone if no monotone operator has a strictly larger graph. For the resolvent is then an everywhere-defined single-valued map.
Problem 1.1. Let and be maximally monotone, bounded linear, , . Solve the primal inclusion
and the dual inclusion
Their solution sets are and .
Problem 1.2. On the Hilbert direct sum set
and find a zero of .
The algorithm (3.1) of the paper, for step sizes and error sequences , reads
Assume , , all six error sequences absolutely summable, and . Then for some and with and :
and the convergence of (resp. ) is strong if is uniformly monotone at (resp. at ).
GradErrors.Deterministic.lemma_1 (Bertsekas–Tsitsiklis), of which it is the special case , so that the alternative cannot occur.Theorem 3.1 gives a method that handles two arbitrary maximally monotone operators coupled by an arbitrary bounded linear map, with only resolvent evaluations of and (computed in parallel) and forward applications of and . It tolerates summable errors in every step and variable step sizes, and it produces a primal and a dual solution simultaneously, assuming only that the primal problem is solvable. The paper derives from it, as instances, methods for sums of composite operators (Theorem 3.8) and for Fenchel–Rockafellar-type composite minimization (Section 4).
The theorem is proved in the literature. This mission formalizes it, which in turn requires a machine-checked inexact forward–backward–forward theorem (Theorem 2.5) and the structural facts about the monotone+skew reformulation (Propositions 2.7, 2.8). These intermediate results are reusable for the descendants of this algorithm. No machine-checked proof of Theorem 3.1, of Theorem 2.5, or of the quasi-Fejér Lemma 2.2 is known to the mission's authors. On Prove2Me, CondatPD.FB.lemma_4_4 (inexact forward–backward with a cocoercive operator) and CondatPD.FB.theorem_3_1 (Condat's primal–dual method) concern related algorithms; CondatPD.PPA.A_maximal_monotone is an open subdifferential special case of Proposition 2.7(iii).
The obvious route, applying a known splitting method directly to with , fails: need not be maximally monotone, and its resolvent cannot be computed from that of . The reformulation on avoids this, but at a cost. is not a subdifferential, is not cocoercive (it is skew, so ), and forward–backward theory does not apply; one needs the forward–backward–forward method with Lipschitz, merely monotone . Proving that method's convergence with errors requires quasi-Fejér analysis in a possibly infinite-dimensional space, where bounded sequences only have weakly convergent subsequences and the limit must be identified through the maximal monotonicity of , whose graph is sequentially closed in the weak–strong topology. The strong convergence clauses (iii)–(iv) need a further estimate, since uniform monotonicity of at does not by itself control the coupled iterate.
[NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]; set-valued operators are maps E → Set E. Monotonicity, maximal monotonicity (no proper monotone extension of the graph), zer, the resolvent predicate IsResolvent, weak convergence WeakTendsto ( for all ), opInv and opAdd are imported from published platform definitions.WithLp 2 (H × G), whose inner product is ; the plain product would carry the sup norm.JA n satisfies for all , and likewise for . For maximally monotone operators and such maps exist (Minty's theorem) and are unique, so quantifying over them is the paper's statement. Proposition 2.7(iv) is stated as "the product map is a resolvent of ", which is the equality by uniqueness.Summable (fun n => ‖a n‖); indices start at ; is the operator norm and is kept, so the step-size window is nonempty.EReal, against every point of the graph. It is neither strong monotonicity nor uniform monotonicity on a set.GradErrors.Deterministic.lemma_1, of which it is a special case.The mission needs Minty-type facts (existence of resolvents), demiclosedness of maximally monotone graphs, sums of a maximally monotone and a Lipschitz monotone operator, and quasi-Fejér/Opial arguments in Hilbert space. None of these is in Mathlib in this form, and all are reusable beyond this mission. Contributions toward any of the milestones, or toward this general infrastructure, are welcome.
Second-order cone programming (SOCP) minimizes a linear function over the intersection of an affine subspace with a product of Lorentz cones. It contains convex quadratically constrained programs, robust linear programs with ellipsoidal uncertainty, and many norm-minimization problems, and it is solved in practice by primal–dual interior-point methods. At each iteration such a method computes a search direction from a linearized, symmetrized form of the complementarity conditions; the symmetrization depends on a scaling matrix , and different choices of give different directions. The two directions used in practice are the HKM direction (Helmberg–Rendl–Vanderbei–Wolkowicz, Kojima–Shindoh–Hara, Monteiro) and the NT direction (Nesterov–Todd).
A desirable property of a search direction is scale invariance: if the problem is transformed by an automorphism of the cone, the direction computed for the transformed problem is the image of the original direction. A scale-invariant method behaves identically on all problems related by such a change of coordinates, so its behaviour does not depend on an arbitrary choice of coordinates within each cone.
Timeline. Tsuchiya (1999, Optim. Methods Softw. 11 & 12, pp. 141–182; reference [27] of the paper) proved that the HKM and NT directions for SOCP are scale invariant, with a two-page argument for each. Tütüncü, Toh and Todd (2003), in the paper that describes the solver SDPT3 version 3.0, derived closed forms for the blocks of the Schur complement matrix ((23) for HKM, (29) for NT) and used them to give a short proof of Tsuchiya's result (their Proposition 1).
There are second-order cone blocks. Block has dimension , and a vector is split into its first coordinate and the rest . The cone is , and with and , the function is defined on the cone.
The data are matrices , a vector and vectors . The primal problem minimizes subject to and ; the dual maximizes subject to and .
The arrow matrix of is . Given an interior iterate and a scaling block , set
With and a centering parameter , a search direction solves the Newton system
The HKM direction takes from the explicit formula (19) in ; the NT direction takes from (20)–(21) in and .
The automorphism group of consists of the invertible linear maps with ; these are exactly the matrices with for some and . Scaling by sends the data and iterate to , , , , , .
For either direction (HKM or NT), every interior iterate, every , and every choice of ,
In attack order: the identities (31) for with ; the Schur complement reduction (10)–(15); for HKM; the HKM closed forms (23) and (24)–(25); the right-hand-side formula (28) for both directions; the HKM invariance step of the proof; the NT identities and (29); the NT block formula (30); and the NT invariance step of the proof.
The proposition shows that SDPT3's two second-order-cone directions do not depend on how each cone is coordinatized. The closed forms (23), (24), (29) and (30) are what SDPT3 uses to assemble the Schur complement matrix: they show that each block is a diagonal matrix plus a low-rank term, which is the basis for its sparse and Sherman–Morrison–Woodbury handling of large cones.
The result is proved twice in the literature (Tsuchiya 1999 and this paper). As far as is known, neither proof has been machine-checked, and no formal library contains the HKM or NT scalings, the arrow matrix of the Jordan algebra of the Lorentz cone, or its automorphism group. This mission produces those definitions and a checked proof. The printed proof assumes , that is ; the goal covers the whole group , so a complete formalization also closes the case , where (31) and the remark that is unchanged no longer hold as printed.
Every step is linear algebra, but none is a one-line rewrite. The inverse of appears everywhere, so one first needs invertibility of and for interior iterates, and the HKM and NT scalings must be shown to satisfy and respectively, which are identities involving , square roots and the denominators and . Transporting the Newton system directly through fails: and are built from , which is not equivariant in an obvious way, and the HKM scaling at is not . For , the quantities , and scale by powers of , and these factors must be tracked until they cancel.
A block of dimension is Fin (d i + 1) → ℝ, so ; is index 0 and the indices Fin.succ j. Mathlib's norm on this type is the sup norm, so every Euclidean quantity is written through . Interior points are encoded by and . Matrix inverses are Matrix.inv, which is on singular input; the milestones that invert a matrix state its invertibility.
Standing assumptions: the problem is a pure SOCP (); the iterate is interior; . The paper's assumption that has full row rank is dropped, because the goal is stated for solution sets of the Newton system and needs no uniqueness. is encoded algebraically (positive multiples of orthochronous Lorentz transformations) rather than as , so that the goal does not require the classification of cone automorphisms. The goal assumes nothing about the scaled iterate; its interiority is a consequence.
The Newton system is defined by its raw rows with , from (8) and from (19)/(21). A formalization that defined the direction through the closed forms (23)/(29), or defined implicitly by or , would make the goal nearly definitional and is ruled out.
Reusable infrastructure: the arrow matrix and of the Lorentz cone, the HKM and NT scalings, and the algebra of Lorentz transformations. Contributions toward any milestone, and alternative proofs of the goal that bypass the milestones, are welcome.
A retailer that carries several substitutable products, such as brands of the same item, loses part of a customer's demand when the preferred product is out of stock, but not all of it: some customers buy another product instead. How much of each product to stock then depends on the stocking levels of the others. When all products are managed by one company, the stocking problem is a joint optimization; when each product is managed by a separate firm, it is a game, and each firm ignores the effect of its stock-outs on its competitors.
A common view in the inventory literature is that competition drives inventories up for every product. Mahajan and van Ryzin and Lippman and McCardle demonstrated it in special cases (Lippman & McCardle, Operations Research 1997; Mahajan & van Ryzin, Columbia working paper 1999, published in Operations Research 2001). Netessine and Rudi (SSRN 303779, 2002, later published in Operations Research, 2003) study the general model with products, an arbitrary continuous joint demand distribution, and arbitrary substitution fractions. They show that the common view fails in general: some products may be stocked more under centralized management (Proposition 6(i)), but at least one product is always stocked no less under competition (Proposition 6(ii)). This mission formalizes Proposition 6(ii) and the centralized first-order analysis on which it rests.
There are products, indexed , sold in a single period. Product is stocked at units at unit cost , sold at unit price , and salvaged at unit value , with . Write (the underage cost) and (the overage cost).
The first-choice demand vector is random, with a known continuous joint law on the positive orthant. A fraction of the unmet demand for product switches to product , with and ; a customer whose second choice is also out of stock is lost. The effective demand for product is
Under centralized management a single company maximizes the expected profit
over all ; a maximizer is written . Under competition firm chooses to maximize
given the other firms' quantities; a Nash equilibrium is a vector at which no firm gains by changing its own quantity. In the Lean development these objects are Model, Ds, centralProfit, IsCentralOptimal, firmProfit, IsBestResponse and IsNash in the namespace DemandSubstitution.Comparison.
For every optimal centralized stocking vector and every Nash equilibrium ,
The statement quantifies over all optima and all equilibria; it asserts neither existence nor uniqueness of either.
Proposition 6(ii) bounds how far competition can depart from the centralized solution in the downward direction: it can never make every product understocked. Together with Proposition 6(i), it shows that neither "competition overstocks everything" nor its opposite holds in general, and it is the step from which the symmetric case, Proposition 6(iii) (every product is stocked at least as much under competition), follows. The centralized condition (7) and the derivative (8) are of independent use: they give the first-order conditions of the multi-product newsvendor with stock-out substitution for an arbitrary number of products and an arbitrary continuous demand law, obtained without Leibniz-rule integration over polyhedral regions.
The results are proved in the paper; none of them has a machine-checked proof. A formal proof requires differentiating an expectation of piecewise-linear functions of the demand under the integral sign, and handling the measure-zero boundaries where those functions have kinks. That machinery is reusable for other multi-product newsvendor models.
The centralized profit is not concave in general for three or more products (the paper's own example, pp. 3–5), so the optimum cannot be characterized as the unique solution of first-order conditions: the argument must work with an arbitrary maximizer and use only the necessary condition at an interior coordinate. The derivative (8) must be justified as a two-sided derivative of an integral whose integrand is not differentiable on hyperplanes in demand space; the paper's difference quotient argument leaves the boundary terms implicit. Finally, the obvious comparison of the two first-order conditions yields only an inequality between probabilities; turning it into an inequality between stocking levels requires the distribution function of to be strictly increasing, and an optimal may be zero, where (7) does not hold.
Products are Fin n (0-based). The model data and the standing assumptions , , , are fields of a structure Model n. The demand law is a probability measure on that is absolutely continuous with respect to Lebesgue measure, is concentrated on the open positive orthant, and has integrable coordinates (IsDemandLaw). Expectations are Bochner integrals and probabilities are μ.real of sets with the strict and weak inequalities exactly as printed. Derivatives are two-sided HasDerivAt in one coordinate, the others held fixed through Function.update.
Three hypotheses are pinned relative to the page and disclosed in the statements:
NeZero n in the goal: for "at least one " is false.HasPositiveDensity μ in the goal: a Lebesgue density strictly positive on the open positive orthant. The paper's last step uses strict monotonicity of the distribution function of without stating it.The centralized optimum is a maximizer of over nonnegative vectors and the Nash equilibrium is the no-profitable-deviation property over nonnegative quantities. Defining either by its first-order condition ((7) or (10)) would turn the propositions into definitions and is ruled out. Stating the goal for one chosen optimum or equilibrium is ruled out as well: it holds for every pair.
Contributions welcome: differentiation of expectations of piecewise-linear functions under absolutely continuous laws; null-set lemmas for ; Fermat's rule at a coordinate-wise interior maximizer; the Nash condition (10) of the competitive game, which milestone 5 needs and which is also posed in the companion mission on equilibrium existence.
Approximate dynamic programming replaces the exact value functions of a Markov decision process by approximations, typically produced by a regression algorithm. The classical guarantees for the resulting policies are stated in the max norm: if every state-action value is estimated to within uniformly over the state space, the greedy policy loses at most a multiple of (Williams and Baird 1993; Bertsekas and Tsitsiklis 1996). Regression algorithms, however, control an average error under the distribution on which they are trained, not a worst-case error, so these guarantees rarely apply to the approximations actually computed.
Chapter 5 of S. M. Kakade's PhD thesis (On the Sample Complexity of Reinforcement Learning, UCL 2003, pp. 57–66) identifies the distribution under which the error of an approximate policy iteration algorithm should be measured. For the finite-horizon, non-stationary approximate policy iteration algorithm (NAPI), the loss relative to any competitor policy is bounded by twice the horizon times the regression error averaged under the future state-time distribution of that competitor. Taking the competitor optimal, the relevant "test" distribution is the one visited by an optimal policy, generally not the distribution on which the regressor was trained; the thesis calls this the "mismeasure" of reinforcement learning. The key tool, the performance difference lemma, was proved for the discounted case by Kakade and Langford (ICML 2002) and is used throughout the conservative policy iteration and policy search literature.
A -epoch MDP has a finite state set , a finite nonempty action set , decision epochs , a transition kernel and a deterministic reward . A policy is a sequence of decision rules , distributions on ; it may be stochastic and non-stationary. A deterministic policy chooses the action .
Values are normalized. The -value is , so for and
The state-action value is , the advantage is , and the optimal value is . The future state-time distribution of from is
NAPI (Algorithm 6) starts from an arbitrary deterministic policy and updates its decision rules backwards, : at update a PolicyChooser receives the current policy and returns a decision rule , which replaces the rule at time . The output is . With RegressionPolicyChooser (Algorithm 7), a regressor returns an approximation of and is greedy for it. The per state error and per state regression error at update are
both measured against the input policy of update .
The discounted companions use the normalized discounted value , its advantage , and the Bellman error of a state vector , where .
For the policy returned by NAPI with RegressionPolicyChooser, every policy and every state ,
The regression outputs are arbitrary; the statement holds for every regressor and every tie-breaking rule.
The discounted half of Lemma 5.2.1 is already on the platform as ApproxOptRL.CPI.performance_difference and is referenced, not restated.
The goal replaces a max-norm hypothesis by an average one, under an explicit distribution. Its consequences: the approximation error only matters on the state-time pairs an optimal (or any good) policy visits; a regressor trained under a distribution over state-times performs well when resembles the state-time distribution of a good policy; and only one factor of the horizon appears, against two factors of in the max-norm bounds for discounted approximate value and policy iteration (Chapter 3 of the thesis). The same chain, Lemma 5.2.1 and Lemma 5.3.1, underlies the μ-policy search analysis of Chapter 6 and, in the discounted case, conservative policy iteration.
All statements are proved in the thesis; none of the finite-horizon ones is formalized on the platform. A related performance difference identity, FoundationsRL.RLBasics.performance_difference, is proved on the platform for episodic MDPs with layer-dependent kernels and unnormalized values, with roll-in by one policy; it is the same mathematics up to the normalization but a different object, and is not reused. The mission produces a reusable normalized -epoch layer (values, advantages, state-time distributions) and machine-checked proofs of the chapter's results.
The obvious approach to Theorem 5.3.2 compares with through max-norm contraction arguments, as in the discounted analysis of Chapter 3; that route only yields a bound in terms of and loses the averaging under . The averaged bound needs an exact identity between value differences and advantages along the competitor's trajectory distribution, which for non-stationary stochastic competitors requires a careful telescoping over epochs of the state distribution recursion. The second difficulty is bookkeeping in the algorithm: the regression error at update is measured against the input policy of that update, whose decision rules at later times have already been replaced, while the bound concerns the returned policy; relating the two requires showing that later updates do not change .
S, A are Fintypes with decidable equality, A nonempty; P s a s' is with IsTransitionKernel P; rewards satisfy 0 ≤ r s a ≤ 1 in every statement (the thesis's standing assumption, p. 22). The thesis also allows infinite state spaces; here S is finite.0 < T. All values carry the factor (discounted: ), and carries ; the constants and are right only in this normalization.ℕ → S → A → ℝ, valid when every rule at a time is a distribution. Deterministic policies ℕ → S → A enter through their indicator policies. is the supremum over the subtype of valid policies. Discounted statements use the published ApproxOptRL.Shared.Model; is the value of an optimal stationary policy.napiPolicy): the policy after updates , so the input of update is the policy at stage and the output is the policy at stage . The printed loop "For " omits the update at , which would leave the time-0 rule random and make the theorem false; the loop here runs to , as in the proof and in Algorithms 8–9.Finset.sup'; on state-action functions is Mathlib's sup norm on S → A → ℝ. is a single number, as printed in Definition 5.1.2.Welcome contributions: proofs of the milestones, general lemmas about the -epoch layer (values in , normalization of , the path-expectation form of ), and links to the platform's discounted performance difference results.
In a linearly parameterized bandit, a decision maker repeatedly chooses an arm from a possibly infinite set of vectors and receives a noisy reward whose mean is linear in an unknown parameter. Classical bandit policies treat arms as independent and must try each arm, so their regret grows with the number of arms (Lai and Robbins 1985); in applications such as marketing, where similar products are expected to have similar sales, the linear structure lets one observation inform many arms, and the regret can be made independent of the number of arms. Rusmevichientong and Tsitsiklis (arXiv:0812.3465v2, Mathematics of Operations Research 2010) show that when the arms form the unit sphere of , no policy has Bayes risk below order . This mission concerns their matching upper bound: a simple policy that alternates exploration and greedy exploitation in cycles of growing length attains regret of order whenever the best arm depends smoothly on the parameter.
The linearly parameterized bandit was studied earlier by Abe and Long (1999), Auer (2002) and, independently of this paper, Dani, Hayes and Kakade (2008), whose policies rely on confidence regions for the parameter. The result here shows that for arm sets with a smooth best arm, such as balls and, by Polovinkin (1996), ellipsoids, a phase-based policy with a single least squares estimate per cycle suffices.
Let and let be a compact set of arms. Playing arm in period yields the reward
where is an unknown parameter and the errors are independent of each other and of , identically distributed in for each arm, with mean zero.
Assumption 1 fixes constants that do not depend on : (a) every error satisfies for all ; (b) every arm has , and contains linearly independent arms with .
The smooth best arm response condition SBAR() requires that every have a unique best arm , the maximizer of over , and that for unit vectors .
The PEGE policy (Phased Exploration and Greedy Exploitation) runs in cycles . In cycle it plays once each, computes the ordinary least squares estimate
from all exploration rewards so far, and then plays a greedy arm for periods, ties broken arbitrarily.
The regret given over periods is , where is the arm played in period , and the risk is for a prior on .
Under Assumption 1 and SBAR(), there is depending only on such that for every , every and ,
and, if and for every , there is depending only on with
The constants are unspecified; only the order and its uniformity in are asserted.
Theorem 3.1 with the lower bound of Theorem 2.1 of the same paper identifies as the optimal order of the regret and the Bayes risk on the unit sphere, and Corollary 3.3 makes this precise. The bound is achieved by a policy with no confidence sets and no per-period optimization beyond one linear maximization per cycle. The factor shows how the difficulty depends on the size of the parameter; combined with the trivial bound , the regret does not deteriorate as .
The results are proved in the paper; none of them is machine-checked. A formalization yields a verified dimension-explicit regret bound for an explore–exploit policy with a continuum of arms, the least squares error bound under sub-Gaussian noise (Lemma 3.4), and Lipschitz properties of normalization and of the best-arm map on balls, all of which are reusable.
The expected instantaneous regret of a greedy arm computed from a noisy estimate is not obviously small: for a general compact arm set the best arm may jump under a small perturbation of the parameter, and the regret is then of order however good the estimate is. The SBAR condition prevents such jumps, but only for unit vectors, so the estimation error must be transferred to the direction of the estimate, which costs a factor . The estimate may also vanish with positive probability when the errors are discrete, where the greedy arm is arbitrary. Finally, the constants must be uniform in the dimension : a bound with an -dependent constant is immediate from , so the content of the theorem lies in keeping every constant independent of and of the arm set.
Vectors live in EuclideanSpace ℝ (Fin r), so the norm is Euclidean and the inner product is . The model's standing assumptions are encoded as follows: is compact; the errors of each arm have mean zero and a law ; Assumption 1(a) requires the moment generating function to exist and satisfy the sub-Gaussian bound; Assumption 1(b) writes as . Every constant is quantified before the dimension , the arm set, the error laws, the exploration arms, the tie-breaking rule, the prior, and ; a version with constants depending on or on the instance is trivial and is excluded by this quantifier order.
PEGE uses exactly the exploration arms of Assumption 1(b), which are an argument of the policy. The greedy rule is any measurable selection of a maximizer; measurability, implicit on the page, is a hypothesis. Since PEGE uses only exploration rewards, the expectation is over an independent table of exploration errors with laws , with the parameter fixed to ("given "). Regret and risk are lower Lebesgue integrals of nonnegative gaps, valued in , so an upper bound is never satisfied by a default value of an integral. The moment conditions on the prior are lower Lebesgue integrals, so if the prior charges the origin.
Two printed statements are adjusted. Lemma 3.6 is printed "for any ", but its bound is undefined at ; it is stated for . The p. 18 cycle-sum display is likewise stated for . In Corollary 3.3, the exploration arms are those of Assumption 1(b) with , as in its proof. Measurability of the density in Lemma 3.2(a) is added.
The source is arXiv:0812.3465v2; its printed page numbers equal the PDF page numbers. Contributions welcome: proofs of the milestones, a sub-Gaussian least squares library, and the Lipschitz analysis of best-arm maps.
Robust regression guards a linear model against errors in the data matrix. The observations are fitted by , but the features (the columns of ) are only known up to a disturbance from an uncertainty set . The robust estimator minimizes the worst-case residual,
Xu, Caramanis and Mannor (arXiv:0811.1790v1; IEEE Trans. Inf. Theory 56(7), 2010) showed that when each column is perturbed independently within a Euclidean ball of radius , this problem is exactly the weighted -regularized problem , an un-squared Lasso (their Theorem 1, the subject of the first mission of this series). Robustness then explains regularization: the penalty is the price of the worst disturbance.
Section III of the paper asks which regularizers arise when the disturbances of different features are coupled, that is, when a single budget limits all columns jointly. The answer it gives is that every norm-based regularizer arises this way: a norm budget on the vector of column-disturbance sizes produces the dual norm as the penalty. This links robust optimization (Ben-Tal, El Ghaoui, Nemirovski 2009) and regularized estimation, and it recovers the robust least-squares formulation of El Ghaoui and Lebret (1997) as the Euclidean special case.
Fix , , and an arbitrary norm on . The data are the columns of and the response ; for , . A disturbance is with ; the perturbed matrix has columns . For an uncertainty set the robust objective is
Three families of uncertainty sets appear.
A fourth, polytope set, for , , is the subject of Corollary 2. Write .
For an absolute norm and , for every the worst case over the norm-budget set is attained and
and the robust problem and have the same minimizers.
For and every : , attained, with the same minimizers.
For every , in the extended reals,
If some has , then for every the worst case over the polytope set equals (both sides when the constraints are infeasible), the infimum is attained when feasible, and robust minimizers are exactly the -parts of optimal solutions of that linear program.
The paper's general result, Theorem 4 (p. 6), expresses the coupled robust problem through a Lagrangian function under the assumption that has nonempty relative interior. The mission does not pose it: that assumption is not Slater's condition, and the statement fails without one (an explicit counterexample with is recorded in the series plan). The mission poses the decomposition (13), on which Theorem 4 rests, and the two corollaries, which are true as stated under the readings below.
The result. Corollary 1 says that any norm penalty is the worst-case cost of column disturbances whose sizes are jointly bounded in the dual norm. Taking gives the penalty (budget per column), gives (a shared budget), and both Euclidean gives the Frobenius-ball model of robust least squares. Corollary 2 shows that polytope budgets keep the problem a linear program apart from the loss, which allows modeling, for instance, corruption of an unknown subset of features. Eq. (13) is the common reduction behind these: the coupled worst case is the uncoupled one maximized over the admissible budget vectors.
Formalizing it. None of these statements has a machine-checked proof. The mission makes precise two points the paper leaves implicit: which "symmetric" norms the corollary is true for, and in what sense "max" holds when the budget set is empty or unbounded. The finished development is a self-contained library of worst-case residual identities for arbitrary norms on finite-dimensional or general normed spaces. Related platform items, credited and not reused: SPOBounds.StronglyConvex.dual_norm_ball_max (maximum of a linear functional over a norm ball, with the continuous-dual norm), and RobustLS.Unstructured.worst_case_residual_closed_form (El Ghaoui–Lebret, which perturbs in a Frobenius ball, a different set).
The upper bound of every identity is a triangle inequality. The content is in the matching lower bound: a disturbance must be exhibited that aligns all perturbed columns with the residual direction, and in (13) each column disturbance must have norm exactly , including columns with , which is where enters. The paper's first line of the proof of (13) rewrites as ; that set identity is false unless is downward closed, so the obvious route through it does not work for (13) as stated. For Corollary 1 the remaining step is the identity , which needs the absolute property and fails for norms that are only permutation invariant. For Corollary 2 the remaining step is linear programming duality, which Mathlib does not yet provide in this form.
is an arbitrary real normed space with Nontrivial E (the paper's implicit ); finite dimension is not imposed, a harmless generalization. Columns are a family a : Fin m → E, disturbances δ : Fin m → E, coefficients Fin m → ℝ, and . Explicit readings:
EReal; it is never defined by its closed form. "Max" is stated as IsGreatest of the set of residual values (attained) in Theorem 3 and Corollary 1, where the maximum exists, and as an EReal supremum in (13) and Corollary 2, where it need not.Seminorm on Fin m → ℝ with (the type already carries the sup norm, so the notation is not used for it). The dual norm is a real sSup of , a nonempty set that is bounded above because is a norm on .A trivializing formalization is ruled out: the robust objective is the EReal supremum (or the residual-value set) over the uncertainty set, so no identity holds by unfolding, and no real sSup junk value enters a robust objective. Welcome contributions: the explicit worst-case disturbance in an arbitrary normed space, the absolute-norm duality lemma, and a finite-dimensional LP strong duality theorem, each reusable beyond this mission.
Facility networks fail: plants close after floods, distribution centres lose power, suppliers go bankrupt. The reliable uncapacitated facility location problem (RUFL) of Cui, Ouyang and Shen (UCTC-FR-2010-02, February 2010; published as Operations Research 58(4), 2010, doi:10.1287/opre.1090.0801) chooses which facilities to open and, for every customer, an ordered list of backup facilities, so as to minimize fixed cost plus expected transportation and penalty cost when facilities fail independently with site-dependent probabilities. It extends the uniform-probability model of Snyder and Daskin (Transportation Science, 2005).
RUFL is solved by Lagrangian relaxation in the sense of Fisher (Management Science, 1981): dualizing the constraints that link assignments to open facilities splits the problem into one relaxed subproblem (RSP) per customer. Every evaluation of the Lagrangian dual solves all subproblems, and (RSP) is itself a hard combinatorial problem, because the probability that a backup facility is used depends on which facilities sit above it. The paper therefore replaces (RSP) by a fixed-probability reformulation (RRSP), an assignment problem, and Proposition 4 asserts that its optimal value is a valid lower bound. A Lagrangian bound computed from (RRSP) is a valid bound on RUFL only if this holds.
Fix one customer and drop the index from the variables. The data are: the demand rate ; regular facilities with unit costs and failure probabilities ; an emergency facility with (the penalty per unit of unserved demand) and ; multipliers ; and levels with .
A level assignment is a binary array (: facility serves at level ) such that the customer has distinct regular facilities at levels , the emergency facility at a level , and nothing after it. In the paper's constraints:
The level- facility serves exactly when all facilities at the levels above it have failed. The transitional probabilities are and , with imposed through linear constraints. The relaxed subproblem is
Order the regular facilities by reliability, , and set and . The reformulation freezes the probabilities at these values:
over the same level assignments.
The proof works through a split formulation: chooses whose distance is paid at each level, a second level assignment chooses whose failure probability is used, and the cost is . Imposing gives back (RSP).
With , , , and any reliability ordering: for every (RSP)-feasible there is an (RRSP)-feasible with
The result. Proposition 4 makes (RRSP) usable as a lower-bounding oracle. (RRSP) is an assignment problem with rows and levels, so it can be solved in strongly polynomial time by the Hungarian method (Kuhn, 1955). The exact subproblem algorithm of §3.3.1 needs branch and bound over subsets. With the bound, every subgradient iteration of the paper's Lagrangian scheme still yields a valid lower bound on RUFL, which is what the gap-closing branch and bound relies on.
Formalizing it. The proposition has a printed proof, but the proof is incomplete (see below), and to our knowledge no machine-checked version exists. A formal proof certifies the bound, settles which hypotheses it needs, and gives a reusable model of multi-level backup assignment with transitional probabilities.
The obvious argument says that is the largest probability any facility can have of serving at level , so freezing the probabilities at can only lower the cost. That is false as stated: transport costs and the penalty may be negative, and a larger serving probability then means a higher cost. What is needed is a comparison of the whole cost profile, not level by level.
The paper's route is the split formulation. Lemma 1 shows that the probability facilities of some optimal split solution can be taken in increasing order of . The proof then ends with "without loss of generality, we can fix and … which leads to the (RRSP) formulation". This step has a gap. Lemma 1 only says that is ordered. Turning its probabilities into , also needs to use the facilities with the globally smallest failure probabilities, and the paper never shows this. A complete proof has to replace 's facilities by the most reliable ones and show that the cost does not increase. That replacement raises every cumulative service probability , so the comparison is a rearrangement argument over the ordered distances. Lemma 1 alone does not close the proposition.
The sign of the multipliers matters. With of mixed sign the proposition is false, for instance with , , , , , , . There while . Lemma 1, by contrast, holds for multipliers of either sign.
Facilities are Fin (J+1) with Fin.last J the emergency facility, levels are Fin (R+1), and every variable is a real array, with constrained to . The customer index is dropped. The ordering is a bijection of Fin J with monotone, and the goal quantifies over every such . "Lower bound" is stated as for-all/exists, so no infimum of a possibly empty set is taken; both feasible sets are finite and contain the emergency-only assignment.
Conventions fixed in Lean, each recorded in the docstrings:
The statements are not trivial. A sanity-check file exhibits a two-facility instance satisfying every hypothesis, together with feasible points of all three formulations.
A complete development needs finite sums and products over Fin, the explicit form of along a level assignment (a product of failure probabilities), and a rearrangement inequality for ordered sequences. All three are reusable for the other missions of this series and for reliability models in general. Contributions are welcome on the milestones, on a corrected proof of the final step, and on lemmas such as "the transitional probabilities of a level assignment are products of the 's".
Many operations models contain terms of the form : expected shortfall or overflow of an affine function of an uncertain vector. Inventory and newsvendor costs, penalties for violated soft constraints, and the Conditional Value-at-Risk of a linear decision rule all reduce to it. In practice the distribution of the uncertainty is rarely known; what is known are a few descriptive statistics, such as a range for the mean and an estimate of the covariance. Distributionally robust optimization then replaces the expectation by its supremum over every distribution consistent with that information.
The question goes back to Scarf (1958), who solved a single-product newsvendor problem against the worst distribution with known mean and variance , using the fact that over such laws; Gallego and Moon (1993) simplified the argument. El Ghaoui, Oks and Oustry (2003) obtained conic representations of worst-case Value-at-Risk under mean and covariance information, and Delage and Ye (2010) studied stochastic programs with uncertain mean and covariance. Goh and Sim (2010) use bounds of this kind inside a general framework for linear optimization under uncertainty with recourse: after a piecewise-linear decision rule is introduced, every expectation in the reformulated problem is of the form above, and the framework needs a tractable, ideally exact, value for its worst case. Section 5.2 of the paper provides it when the information consists of a set containing the mean and the exact covariance.
A primitive uncertainty is represented through a segregated uncertainty , , and a fixed matrix and vector with (equation (9) of the paper). The paper notes that has full row rank. Write .
The distributional information is:
The family is
For and the worst-case expected positive part is , and the bound of (22) is
Following the paper (p. 909), an infeasible minimization has value ; all values are in .
For of full row rank, positive semidefinite and nonempty,
This is an exact identity; it contains no constants that later work could improve.
Theorem 2 says that the deterministic problem (22) evaluates the worst case exactly, not merely bounds it. Through (23) it becomes a second-order cone program whenever is conic representable, so distributionally robust constraints and objectives with mean–covariance information can be handed to an off-the-shelf conic solver without loss. In the paper, is one of three building blocks (with the mean–support bound and the directional-deviation bound ) that are combined by infimal convolution into the unified bound of Theorem 4, which in turn prices the deflected linear decision rules of §6. Specialized to , and a singleton mean set, it recovers Scarf's mean–variance bound.
The theorem is proved in the paper's online appendix; no machine-checked proof of it, nor of Scarf's bound in this multivariate form, is known to exist. A formalization would certify the exact value, including the cases the printed statement treats only implicitly: outside the range of (both sides ), a degenerate quadratic form , and unbounded mean sets.
The upper bound is a moment inequality and is the easier half. The difficulty is tightness. The supremum over is in general not attained, so the proof must exhibit, for every point of , distributions on that meet the full covariance constraint on exactly while driving the expected positive part of the single linear functional to the bound. The constraint fixes second moments, not just the variance of , so the scalar extremal laws behind Scarf's bound do not directly give members of . The case infeasible requires showing that the worst case is , i.e. that contains distributions with arbitrarily large expectations; this is where the full-rank assumption on enters.
The random vector is the identity on Fin n → ℝ and a distribution is a measure P on it. The mean, the covariance matrix and the finite-second-moment condition come from the published definition MomentDRO_Conf_Setting (meanVec, covMat, HasSecondMoments). The covariance condition is , which equals the paper's by linearity; it constrains the covariance of the primitive vector, an matrix, not the covariance of . The positive part is max · 0. The worst case and take values in EReal: an infimum over an empty set is and a supremum over an empty set is , matching the paper's convention for infeasible problems. The paper's "inf" and "sup" are not claimed to be attained.
Readings fixed by this mission, each implicit in the paper:
Each is needed for the equality: without it can be empty (worst case ) while is finite or . No convexity or closedness of is assumed; the theorem does not need it. A formalization that takes the infimum in (where an empty infimum is ) or states only the inequality would trivialize or weaken the theorem and is ruled out.
A complete development needs a Scarf-type mean–variance inequality for , constructions of multivariate distributions with a prescribed mean and covariance (Gaussian or finitely supported laws), and the monotonicity and continuity facts behind (23). The scalar inequality and the constructions of distributions with given first two moments are reusable well beyond this mission. Proofs of any milestone, and supporting lemmas on moment-constrained families, are welcome.
In machine scheduling, preemption means that a job may be interrupted and resumed later, possibly on a different machine. Allowing it can only lower the optimal cost, and a basic question for every scheduling model is how much it can lower it: the ratio between the best nonpreemptive and the best preemptive schedule, often called the power of preemption. For identical parallel machines and the total weighted completion time, McNaughton (1959) showed that preemption does not help at all (doi:10.1287/mnsc.6.1.1). For unrelated machines, where every job has its own processing time on every machine, and with release dates, it does help, and no exact relation is known.
Skutella's paper (J. ACM 48 (2001), doi:10.1145/375827.375840) gives approximation algorithms for unrelated-machine scheduling based on convex quadratic programming relaxations. Its §4 adapts the relaxation of §3 to preemptive schedules and rounds it to a nonpreemptive schedule. A by-product is a constant bound on the power of preemption for : the factor , and without release dates. This mission formalizes that bound together with the steps of §4 that produce it.
There are jobs and unrelated machines . Job has a weight , and on machine a processing time and a release date before which it may not be processed there.
A preemptive schedule is a finite list of pieces: job runs on machine during . Running job for time units on machine completes the fraction of it. A schedule is feasible if every piece of on starts no earlier than , two pieces on the same machine never overlap, two pieces of the same job never overlap, and the fractions of every job add up to exactly . The completion time is the end of the last piece of , and the objective is . A schedule is nonpreemptive if every job consists of a single piece.
Smith's order on machine orders the jobs by nonincreasing ratio , ties broken by index. On each machine the release dates sorted nondecreasingly are , with , and the time slot is . For a preemptive schedule, is the fraction of job processed on machine inside slot . The convex quadratic program asks for and with , slot capacities , when , and
Randomized rounding puts job into slot with probability , pairwise independently over jobs, and schedules each slot's jobs back to back in Smith's order from the slot's start.
For every feasible preemptive schedule there is a feasible nonpreemptive schedule with
and if all , one with . This is the paper's ratio of optima, stated so that no existence of optimal schedules is needed.
The result gives a constant bound on how much preemption can help on unrelated machines with release dates, a model in which both the preemptive and the nonpreemptive problems are NP-hard (for the preemptive problem even without weights and release dates, by Sitters, J. Algorithms 57 (2005), doi:10.1016/j.jalgor.2004.06.011). The bound comes from an algorithm: a single relaxation that is valid for preemptive schedules, rounded to a nonpreemptive one. The same rounding is a randomized -approximation for and a -approximation for (Theorem 4.5), and since it never preempts, these bounds hold under any communication delays between machines.
The paper proves all of this on paper. As far as a search of the platform shows, none of it is formalized: the only formal preemption result found is McNaughton's theorem for identical machines. The mission produces a machine-checked model of preemptive schedules on unrelated machines with release dates, a checked lower bound on such schedules by a convex quadratic function of their slot fractions, and a checked analysis of pairwise-independent rounding into nonpreemptive schedules.
The natural first idea is to reuse the nonpreemptive relaxation of §3, which already allows fractional assignments. It fails. Example 4.1 of the paper gives two jobs on two machines where an optimal preemptive schedule costs but the corresponding value is , so is not a relaxation of the preemptive problem. The relaxation must be weakened: the term of §3 becomes , and this weakening is what raises the factor from to .
Proving that the weaker program is a relaxation (Lemma 4.2) takes real work. The fractions of a job inside a slot of an arbitrary preemptive schedule are scattered, so the bound needs a rearrangement inside each slot by completion times, then an exchange argument that compares this order with Smith's order slot by slot. On the rounding side, Lemma 4.3 reduces to the analysis of §3 (each job's expected completion time is at most twice its value in the relaxation) and, without release dates, to Theorem 2.1 of §2. Both have to be redone here on the slot model.
Jobs, machines and slots are Fin n, Fin m, Fin n (0-based). The standing assumptions , , of p. 2 are hypotheses of every theorem. Smith's order is cross-multiplied (), equivalent to the ratio form because . Sorted release dates come from Tuple.sort. The last slot of each machine has no right end, so is never a real number, and the slot capacity constraint is imposed only for slots with a successor. A preemptive schedule is a List of pieces with migration allowed and any number of pieces; nonpreemptive means one piece per job. Completion time is the latest end time among a job's pieces.
Added constraint. The display of on p. 22 omits the condition if (constraint (18) of §3). Without it the rounding can place a job in a slot that opens before its release date, and "computes a nonpreemptive schedule" in Lemma 4.3 fails. It is included here. The fractions of every feasible preemptive schedule satisfy it, so the program remains a relaxation.
Randomized rounding is a probability weight on the finite set of slot assignments with marginals and pairwise products . Pairwise independence is required, full independence is not, and the expectation is a finite sum. "Without nontrivial release dates" is read as for all . Communication delays are not modelled: without them the preemptive class is the largest, so the goal implies the bound for every delay model.
Not formalized: polynomial running time, solving within an additive error , derandomization by conditional probabilities (Theorem 4.5), and Corollary 4.4.
The goal is not trivial. Feasible preemptive schedules exist and are not vacuous, since each job's fractions must sum to and no machine runs two pieces at once. The nonpreemptive schedule is required to be feasible in the same model, and its value is compared with the given schedule's real objective, not with a relaxation value.
A complete development needs: the slot schedule (15)–(17) and its feasibility, the bound of §3 (Lemma 3.5) and Theorem 2.1 of §2, both restated on this slot model, and a product-measure argument showing that pairwise-independent rounding exists. The preemptive-schedule model and the slot machinery are reusable for other unrelated-machine results. Contributions to any milestone are welcome, and so are alternative proofs of Lemma 4.2.
In a road or communication network, traffic is routed by its users, not by a central planner. Each user picks the route that is cheapest for itself, and the resulting equilibrium can be much more expensive for the network as a whole than the best centrally planned routing. Roughgarden and Tardos, How Bad is Selfish Routing? (J. ACM 2002), quantified this loss. Their basic model is nonatomic: infinitely many users, each controlling a negligible amount of traffic. There, the cost of a Nash flow can exceed the optimum by an unbounded factor, but it never exceeds the cost of an optimal flow that routes twice as much traffic (their Theorem 3.1).
Many networks are not like that. A few large operators (internet service providers, freight companies, a navigation app routing its whole user base) each control a strictly positive share of the traffic and can split it over many paths. Section 5.2 of the paper treats this finite splittable model and proves the analogue of the bicriteria bound, Theorem 5.4. This mission formalizes that theorem and the three steps of its proof.
A network has a finite set of edges. Each edge carries a latency function , nonnegative, nondecreasing and continuous on : the delay on when units of flow use it is .
There are agents. Agent must send units of flow from a source to a destination , over its set of paths. Distinct agents may have the same source and destination; their path sets are then separate copies. A flow assigns a nonnegative amount to each path; agent 's part is , the restriction of to . The flow is feasible for the rates if for every , and feasible for if each agent instead sends .
The edge flow is the flow of all agents through . The latency of a path is , and
are the cost of the flow (its total latency) and the cost of agent . A feasible flow is at Nash equilibrium if no agent can lower its own cost by rerouting its own flow: for each , minimizes given for .
In Lean, edges, paths and agents are Fin J, Fin R and Fin Sd; a path is a incidence column A j r, s r is the agent owning path r, and rate i is . The edge flow linkFlow and the feasible set wardropFeasible come from the published definition KellyStochasticNetworks_Wardrop; pathLatency, cost and the modified latencies barLatency come from the series' shared model definitions (SelfishRouting.Bicriteria), and agentCost and IsSplittableNash are defined in this mission.
If is convex on for every edge, is at Nash equilibrium for the finite splittable instance , and is feasible for , then
The comparison flow is arbitrary, so the statement implies the bound against an optimal flow for without naming one.
The proof uses the modified latencies for and for , built from the Nash flow (p. 12). Writing :
Theorem 5.4 says that in a network shared by finitely many traffic-splitting operators, the inefficiency of selfish routing can always be offset by doubling the network's capacity to carry traffic, whatever the network topology and whatever the (convexity-qualified) delay functions. Theorem 3.1 is its limit as the number of agents grows and each share shrinks to zero. The finite splittable model is the setting of later work on atomic splittable routing games and their price of anarchy, which this mission's definitions can serve.
On the formalization side, the result is proved on paper but, as far as a search of the platform and of Mathlib shows, no part of selfish-routing equilibrium theory with finitely many agents has been formalized. The mission provides a reusable encoding of the finite splittable model (per-agent costs, per-agent best responses with all other agents fixed) on top of the published Wardrop definitions, and the three proof steps as separately provable milestones. Milestone 2 is the one with independent content: it turns a game-theoretic equilibrium into the optimum of a convex program.
The obvious attempt copies the proof of Theorem 3.1. That proof uses the nonatomic equilibrium condition: every used path of a commodity has the same, minimal latency , so for every path and the lower bound follows path by path. In the finite splittable model this fails: an agent at equilibrium balances marginal costs , not latencies, and its used paths can have different latencies. The proof must go through the optimality of for the modified program , and that needs both the convexity of and a comparison between the change of agent 's cost and the change of the -cost under the same local move. The paper invokes a first-order optimality lemma (its Lemma 2.4) for , which is not differentiable at ; a formal proof has to handle one-sided derivatives or argue by convexity directly.
0 ≤ ℓ j t for 0 ≤ t, MonotoneOn and ContinuousOn on Set.Ici 0, and ConvexOn ℝ (Set.Ici 0) (fun t => t * ℓ j t). Continuity replaces the differentiability of §2.1, as footnote 3 (p. 7) and §5.2 allow; this weakens a hypothesis.0 < rate i). The case of zero agents is allowed and trivial, as in the paper.wardropFeasible s (fun i => 2 * rate i).Contributions welcome: proofs of the three milestones and the goal; a general lemma that a feasible flow minimizing a convex separable edge cost has no improving two-path move, and its converse; a proof that is convex when is.
In a road or communication network carrying a large population of users, each user picks a route that is fastest for itself given the congestion caused by everyone else. The resulting traffic pattern, a Wardrop or Nash equilibrium, need not minimize the total travel time: Braess's paradox shows that adding a road can make every user slower. Transportation science has modelled such equilibria since Wardrop (1952) and Beckmann, McGuire and Winsten (1956), and the question of how much efficiency selfish behaviour costs was posed in computer science by Koutsoupias and Papadimitriou (1999).
Roughgarden and Tardos, How Bad is Selfish Routing? (J. ACM, 2002) gave the first general answers for networks with many infinitesimal users. This mission formalizes the first of them, from §2.5 of the paper: when every edge latency is a polynomial of degree at most with nonnegative coefficients, the total latency at equilibrium is at most times the optimum. The argument goes through the convex program of Beckmann et al., whose optimal solutions are exactly the equilibria (Dafermos and Sparrow, 1969).
Timeline. 1952: Wardrop states the equilibrium principle. 1956: Beckmann, McGuire and Winsten characterize equilibria as minimizers of a convex potential and prove existence. 1969: Dafermos and Sparrow reprove existence and essential uniqueness for general networks. 1999: Koutsoupias and Papadimitriou introduce the worst-case ratio between equilibrium and optimum. 2000–2002: Roughgarden and Tardos prove the bounds for polynomials (Corollary 2.8) and for linear latencies. 2002–2003: Roughgarden shows the worst ratio for degree- polynomials is , attained already on two parallel links.
An instance consists of finitely many edges , finitely many commodities and finitely many routes . Each route is a set of edges, recorded by a incidence matrix ( iff ), and serves exactly one commodity; is the set of routes serving commodity . Commodity has a rate .
A flow assigns a value to each route. It induces the edge flows and is feasible if for all and for all . Each edge has a latency function , nonnegative, nondecreasing and continuous on . The latency of a route is and the cost of a flow is
A feasible flow is at Nash equilibrium (Definition 2.1) if moving any amount of commodity from a used route to another route leaves at least as slow, after the move, as was before. Lemma 2.2 shows that this is the Wardrop condition: every route that carries flow has minimum latency among the routes of its commodity.
The Beckmann potential of a flow is , the objective of the program (NLP2) of the paper.
For latencies with an integer and , every flow at Nash equilibrium and every feasible flow satisfy
This is the paper's written without division.
The result. Corollary 2.8 was, according to the authors, the first bound of its kind for polynomial latencies (p. 11). It shows that for the latency functions used in practice (the Bureau of Public Roads function has ) uncoordinated routing loses at most a bounded factor, independent of the network size, the number of commodities and the rates. Corollary 2.7 isolates the mechanism: a single scalar property of each latency function, how far the cost can exceed the potential , controls the efficiency loss of the whole network.
Formalizing it. The results are proved in the paper (and the bound has since been sharpened); none of them is machine-checked on the platform. The mission produces a reusable Lean development of nonatomic selfish routing: Definition 2.1 in its deviation form, its equivalence with the Wardrop condition, the Beckmann characterization of equilibria with an honest integral potential, existence and cost-uniqueness of equilibria, and the potential-based efficiency bound. The same layer is used by the companion missions on the bicriteria bound and the bound for linear latencies.
The bound itself is a short chain of inequalities once the equilibrium is known to minimize the potential . That step is the substance: it requires showing that the Wardrop condition is a first-order optimality condition of a convex program over the polytope of feasible flows, with latencies that are only continuous, so is differentiable but its derivative may have kinks. Passing from Definition 2.1 (finite deviations) to the Wardrop condition needs a limit , which fails without continuity of the latencies. Mathlib has no Karush–Kuhn–Tucker theory for such programs, so the optimality characterization has to be built from first principles.
Fin J, Fin R, Fin Sd. Edge flows, feasibility, the Wardrop condition and the potential are the published KellyStochasticNetworks.linkFlow, wardropFeasible, IsWardropEquilibrium and wardropObjective, reused unchanged.A statement in which Nash flows cannot exist (the literal Definition 2.1), or in which is the junk value of a non-integrable function, would make the goal vacuous; the guards above rule both out, and the sorry-free check that two small instances admit Nash flows confirms it.
Contributions welcome: proofs of the milestones, in particular the first-order characterization of minimizers of over the feasible polytope, which is reusable for every potential game on flows.
A real symmetric matrix is copositive when its quadratic form is nonnegative on the nonnegative orthant. Copositive matrices appear wherever a quadratic objective meets sign constraints: standard quadratic programs over the simplex, linear complementarity problems, and conic reformulations of combinatorial problems such as the stability number of a graph. Parrilo's §7.5 (Math. Program. 96 (2003) 293–320) gives an example: if is copositive and , then is a lower bound on .
Deciding copositivity is hard. Murty and Kabadi (Math. Program. 39 (1987) 117–129) showed that checking whether a given integer matrix is not copositive is NP-complete, so the exact tests based on principal minors take an exponential number of operations in the worst case. Efficiently checkable sufficient conditions are therefore what applications use.
Timeline:
Fix and a real symmetric matrix . The matrix is copositive if
For real variables write . Three polynomials in are associated with :
A form is positive semidefinite if it is nonnegative at every point of , and a polynomial is a sum of squares if it is a finite sum of squares of real polynomials. A matrix satisfies if it is symmetric and for all .
The SDPs (7.7) ask for symmetric matrices , with entries , such that
Condition (7.6) asks for a decomposition with and for all .
For every real symmetric matrix ,
The second implication is the paper's "this test is at least as powerful as condition (7.6)".
Theorem 7.7 turns copositivity at level into a single semidefinite feasibility problem whose size is polynomial in : symmetric matrices, semidefinite constraints and linear ones. Its second half says that nothing is lost against the classical test (7.6): every matrix certified by the decomposition is also certified by (7.7). The milestones place the result inside the hierarchy: certificates at any level certify copositivity (milestones 2 and 3), and the sum-of-squares tests become weakly stronger as grows (milestone 5), with (7.6) equivalent to the test at level (milestone 4). This hierarchy underlies later SDP approximations of the copositive cone and of the stability number of a graph.
The paper prints no proof of Theorem 7.7. These statements are proved results of the literature; none of them is formalized in Mathlib or, as far as a search of the platform shows, elsewhere in Lean. The mission produces machine-checked statements and proofs of the level- test and of the structural facts about the hierarchy, built on the platform's published definition of copositivity.
The first half of Theorem 7.7 requires seeing a feasible point of (7.7) as a certificate for the polynomial : the semidefinite constraints control quadratic expressions in , while the linear constraints on the entries of must account for every monomial of degree six, grouped by which indices coincide. The bookkeeping over the three index patterns (all equal, two equal, all distinct) and over the superscript/subscript roles of is where a careless argument loses a term. The second half asks, for an arbitrary decomposition , for a point satisfying all semidefinite constraints and all the linear equalities and inequalities of (7.7) at once. The obvious first idea of testing fails: positive semidefiniteness is sufficient for copositivity but far from necessary, since every elementwise nonnegative matrix is copositive.
Matrix (Fin n) (Fin n) ℝ with a hypothesis M.IsSymm; is arbitrary, including .MurtyKabadi.Reduction.Copositive (Murty–Kabadi mission), for every coordinatewise nonnegative ; it is not replaced by .MvPolynomial (Fin n) ℝ; is defined by its own display, and its equality with at is a milestone.IsSumSq in the polynomial ring.Matrix.PosSemidef. is a family Fin n → Matrix (Fin n) (Fin n) ℝ, with = Λ i j k; each is required symmetric as on the page.Contributions welcome: proofs of the milestones, general lemmas on sums of squares in MvPolynomial (closure under multiplication, Gram-matrix representations of a quadratic form in monomials) and Gram-matrix arguments for forms that are even in every variable.
Conic quadratic optimization (also called second-order cone programming) minimizes a linear function over the intersection of an affine subspace with a product of quadratic cones. It contains linear programming, convex quadratically constrained programming, robust linear programming with ellipsoidal uncertainty and many problems from engineering design; see Lobo, Vandenberghe, Boyd and Lebret (1998). Primal–dual interior-point methods solve these problems in practice; E. D. Andersen, C. Roos and T. Terlaky describe one such method, and an implementation of it linked to the MOSEK optimizer, in On implementing a primal-dual interior-point method for conic quadratic optimization (Math. Program., 2003).
A primal–dual method needs the optimality condition "the duality gap is zero" in a form that can be relaxed into a central path and linearized by Newton's method. For linear programming that form is the componentwise product . For quadratic cones the scalar condition is not componentwise, and the paper's Lemma 3.1 gives the replacement: a block-wise system built from arrow-head matrices. This mission formalizes that lemma and the facts its proof uses.
A vector is written and ; is the Euclidean norm. The paper works with three cones (Definition 3.1):
the nonnegative half-line, the quadratic cone and the rotated quadratic cone. The cone of the problem is a product of such cones, of dimensions , and a point is partitioned accordingly, ; .
To each cone the paper attaches two matrices (Definition 3.2): for ; and for ; and for , is the identity except for the leading block , while is except for the leading block . The arrow-head matrix of a vector is
and , ; is the first unit vector of .
For the companion statements the paper defines and the neighbourhood
For ,
This is the paper's exact statement; it fixes no constants and covers every mixture of the three cone types.
Lemma 3.1 is what makes a primal–dual method for conic quadratic problems possible in the familiar form: replacing by gives the central path (21), and linearizing it gives the Newton system the paper analyses in §4. Lemma 3.2 ii) identifies with that central path, and the §6.1 statement shows the algorithm starts on it. The arrow-head product is the Jordan product of the Lorentz cone's Euclidean Jordan algebra, so the lemma is also the concrete, coordinate form of complementarity in that algebra (Alizadeh and Goldfarb, 2003).
The lemma is proved in the paper's Appendix and is classical; the mission's contribution is a machine-checked version. To our knowledge no proof assistant library contains complementarity for quadratic or rotated quadratic cones, the rotated-cone transformation, or the arrow-head matrix. The statements here are not yet proved anywhere in Lean.
The forward direction is an identity, (61). The converse is where the work is: is one scalar equation, yet it must force equations per block. The argument needs a reverse Cauchy–Schwarz bound inside each quadratic cone, an equality-case analysis that splits on whether a leading coordinate vanishes, and the reduction of the rotated cone to the quadratic one through . A block-by-block argument fails without first showing that each is nonnegative, since only the sum is known to vanish. In Lean, the arithmetic of in and the index bookkeeping of inside Fin n add their own friction.
Vectors are Fin d → ℝ; the paper's is index 0 and is index 1, read through coord v r. The Euclidean tails are written out as sums, tailSq v 1 and tailSq v 2 ; Mathlib's norm on Fin d → ℝ is the sup norm and is never used. Points of are stored block by block, x : (i : Fin k) → Fin (n i) → ℝ, with a cone kind kind i ∈ {nonneg, quad, rot} per block; is , and the block-diagonal , are represented by their blocks. Tmat, Qmat, arrow and e1 are defined entrywise from (16)–(19) and p. 9.
Standing assumptions and additions:
WellFormed: for , for , for (the rotated cone needs and ).The goal is stated with arrow and Tmat, not with the unfolded vector : replacing the arrow-head matrices by that vector, or dropping the rotated cone, would remove the content the lemma is about. Contributions welcome: proofs of any milestone, and reusable lemmas on tailSq (Cauchy–Schwarz for tails, its equality case) and on the arrow-head matrix.
Conic optimization minimizes a linear function over the intersection of an affine subspace with a closed convex cone. Linear programming (the nonnegative orthant), second-order cone programming (products of quadratic cones) and semidefinite programming (the positive semidefinite cone) are all instances. Primal–dual interior-point methods are the standard algorithms for these problems, and production solvers for conic quadratic optimization, such as the MOSEK solver described by Andersen, Roos and Terlaky (Math. Program. 95 (2003)), are built on them.
The classical primal–dual method assumes that both the primal and the dual problem have strictly feasible points. A practical solver cannot assume this: it must also recognize infeasible problems and return a certificate. The device that handles this is the homogeneous model, introduced by Goldman and Tucker for linear programming (1956) and used in interior-point form by Ye, Todd and Mizuno (Math. Oper. Res. 19 (1994)). The model embeds the primal–dual pair into a larger homogeneous system that always has solutions; a solution with a positive homogenizing variable yields an optimal pair, and one with a positive slack variable yields an infeasibility certificate. Section 2 of Andersen, Roos and Terlaky states this generalization to an arbitrary pointed closed convex cone, and this mission formalizes it.
Let , , , and let be a pointed closed convex cone: closed, convex, closed under multiplication by nonnegative scalars, and pointed, (it contains , and and imply ). Its dual cone is
The primal problem is : minimize subject to , . The dual problem is : maximize subject to , . A point satisfying the constraints is feasible; a feasible point is optimal if no feasible point has a better objective value; a problem without feasible points is infeasible. is strictly feasible if some with lies in the interior of , and if some with has in the interior of .
The homogeneous model (7) of the paper asks for with
The quantity is its complementarity gap. In the Lean development these objects are dualCone, PrimalFeasible, DualFeasible, PrimalOptimal, DualOptimal, PrimalInfeasible, DualInfeasible and HomFeasible, all in the namespace ConicQuadIPM.Homogeneous.
For every solution of (7):
Lemma 2.1 is the correctness statement behind every homogeneous-model interior-point solver for conic problems: whatever solution with the algorithm approaches, it is either a scaled optimal primal–dual pair or a certificate of primal or dual infeasibility. Parts (iii) and the certificates (5)–(6) are the conic Farkas-type alternatives on which infeasibility reporting rests. The paper also notes the limit of the statement: for conic problems a solution with need not exist (a feasible conic quadratic pair with a nonzero duality gap is an example), unlike in linear programming.
The results are classical and proved on paper; the strong-duality part is cited from the literature rather than proved in the source. Linear-programming versions of the homogeneous-model properties exist as formal statements on the platform (from Ye–Todd–Mizuno, Vanderbei and Matoušek), but those concern the nonnegative orthant only. This mission states the general conic version over an arbitrary pointed closed convex cone, and the weak-duality and certificate statements it introduces are reusable by any later conic formalization.
Parts (i) and (ii) and the certificates are short arguments from the definitions; the formal work is in handling the cone axioms and the bilinear algebra cleanly. The step that is easy to overlook is in (iii): the identities in (10) and in (11) do not follow from the equations of (7) alone, because the terms and are present; the paper passes over this point. The strong-duality milestone is of a different order: it is a genuine conic duality theorem, cited rather than proved in the source, and it fails without the Slater-type hypothesis (feasible conic quadratic pairs with a nonzero duality gap exist).
Vectors are Fin n → ℝ, is u ⬝ᵥ v, is A *ᵥ x and is Aᵀ *ᵥ y; the paper's first coordinate is index 0. The standing assumption that is a pointed closed convex cone is the hypothesis IsPointedClosedConvexCone K on every theorem, even where a proof uses less. The paper's further assumption that has full row rank is stated "for convenience and without loss of generality" and is not used in any of these results; it is dropped, which makes every statement a generalization. A nonempty interior of is not assumed, and no milestone except strong duality mentions interiors; there, interiors are topological interiors in . Optimality is a predicate (feasible, and at least as good as every feasible point), never a value defined through an infimum or supremum, and infeasibility is the non-existence of a feasible point. Division by is scalar multiplication by under .
A trivializing reading is excluded: part (ii) must conclude optimality of both the primal and the dual point against all feasible points, and part (iii) must conclude that the relevant problem has no feasible point, not merely the sign condition; the milestones (10) and (11) assume only and the respective inequality, never .
All definitions live in one module, Definitions.Def_ConicQuadIPM_Homogeneous_Setting. Contributions welcome: proofs of the milestones, a proof of conic strong duality in this standard form (the platform's Lagrangian conic Slater theorem may help), and reuse of weak duality and the certificates in later conic missions.
At a busy airport the runway is the bottleneck, and the order in which aircraft land or take off determines how much of its capacity is used. Wake turbulence forces a minimum time between consecutive operations that depends on the weight classes of the leading and trailing aircraft, so reordering a first-come-first-served (FCFS) queue can increase throughput or reduce delay. Controllers cannot reorder freely: constrained position shifting (CPS), introduced by Dear (1976, MIT Flight Transportation Laboratory Report R76-9), allows each aircraft to move at most positions from its FCFS position, which keeps the sequence fair and predictable.
Balakrishnan and Chandran (Oper. Res. 58(6), 2010) cast CPS scheduling as dynamic programming on a layered network whose paths are the admissible sequences. For makespan and total delay the separations are assumed to satisfy the triangle inequality, which holds for arrivals only or departures only. When arrivals and departures share a runway it fails: in the separation table of the paper, a heavy arrival followed by a departure and then a small arrival needs only seconds through the departure, while the direct requirement is seconds. Section 6.2 of the paper handles this case for arbitrary per-aircraft cost functions, by expanding the network state. This mission formalizes that construction and its correctness.
Time is discrete: all data are integer multiples of one period. There are aircraft labelled in FCFS order, a maximum shift , a minimum separation between a leading aircraft and a trailing aircraft , a time window for each aircraft, a finite set of precedence pairs ( lands before ), and a cost of landing aircraft at period .
A -CPS sequence is a bijection from positions to aircraft with . A feasible schedule is a -CPS sequence with integer landing times such that precedence pairs are respected, , and
Its cost is .
The CPS network has stages . A node of stage is a list of distinct aircraft that may occupy positions ; its last aircraft is the final aircraft . An arc joins consecutive stages when the lists overlap. Removing the nodes that violate a precedence pair gives the network . For a node , is the set of integer times in the window of .
The modified network of §6.2 has nodes : a node of , a time , and a lower bound on the separation between and its predecessor, with at stage and otherwise , where, for the penultimate and final aircraft of ,
An arc requires an arc of , , , and at least the separation between the penultimate aircraft of and . Arcs entering cost .
Under , positive costs, and the polygon inequalities of three or more hops (below):
each minimum existing exactly when the other does; 3. every minimum-cost path represents a feasible, optimal schedule.
The result turns a scheduling problem with arbitrary separable costs, time windows, precedence and non-metric separations into a shortest-path problem whose size is polynomial in for fixed and in the number of periods. It covers mixed arrival–departure operations, where the triangle inequality genuinely fails, and it is the basis of the paper's §7.1 algorithm for coupled arrivals and departures.
The paper proves Lemmas 5 and 6 in a few paragraphs and omits the proof of Lemma 4. No machine-checked version of the CPS network or of these lemmas exists. A formal development pins down the boundary cases the prose passes over (the first two stages, the last stage where has no successors), and it makes explicit an assumption the prose leaves unstated: Lemma 5 needs the polygon inequalities, not only the two-step check in its proof.
The obvious argument checks separations only between consecutive aircraft, which is what the network of §6.1.2 does. Without the triangle inequality this misses aircraft two positions apart. The state repairs that but is capped at , so one must show that the cap loses nothing: a capped value still certifies the separation to the next aircraft. That uses the definition of over the successors of a node in , so the proof depends on how the network is pruned. Separations three or more positions apart are not tracked at all and rely on the polygon inequalities. Relating network paths to sequences (Theorem 1) requires reasoning about overlapping windows of the sequence and about the precedence pruning rule.
Aircraft and positions are -based (Fin n), stages -based, and (NeZero n). Times, windows and separations are natural numbers (periods); , , and time differences are integers, since involves differences of separations that can be negative. Separation is required for all pairs of aircraft, not only consecutive ones. Minima are stated with IsLeast on sets of costs, never with a real infimum.
The following readings of the paper are committed:
A trivializing formalization is ruled out: the networks are concrete definitions computed from the instance, not arbitrary graphs pinned by hypotheses, and the goal compares two independently defined minima, so it cannot hold by an empty feasible set or an unconstrained optimum.
A complete development needs basic list combinatorics (windows of a sequence, overlap of consecutive windows), the correspondence between bijections and paths, and finite minimization. The CPS network layer is shared with the other missions of this series and is reusable for any CPS scheduling result. Contributions on Theorem 1 alone are welcome, as it is independent of the time-expanded networks.
Linear decision rules are a standard device for making multistage optimization under uncertainty computationally tractable: a recourse decision is restricted to be an affine function of the uncertain data observed so far. Their weakness is that a recourse variable that must stay nonnegative forces the rule to be very conservative. Goh and Sim, Distributionally Robust Optimization and Its Tractable Approximations (Operations Research, 2010), repair this with deflected linear decision rules, in which the violated part of an affine rule is corrected and paid for. The cost of the correction is the expected positive part of an affine function of the uncertainty.
The distribution is not known. The paper assumes only partial distributional information (a support set, a set containing the mean, a covariance, directional deviations) and bounds the worst case of this expectation over every distribution consistent with that information. Such worst-case bounds go back to Scarf's 1958 mean–variance newsvendor bound and form the core of distributionally robust optimization. This mission formalizes the first bound of §5, which uses support and mean information only.
Let be a random vector in (in the paper, the segregated uncertainty vector of dimension ). Two sets describe what is known about it:
The family of distributions consistent with this information is
For data and the worst-case value is , with . The paper's candidate for this value is the deterministic quantity of (21),
Both quantities live in the extended reals: following the paper (p. 909), an infeasible maximization has value and an infeasible minimization .
For closed convex with , and all ,
The result itself. Theorem 1 converts an optimization over an infinite-dimensional set of probability measures into a finite-dimensional convex program over the given sets. When and are representable by linear and second-order cone constraints, the epigraph of is a pair of robust constraints over those sets and is again tractable (Remark, p. 910). The bound is tight, so no better bound can be built from support and mean information alone. In the paper, is one of three building blocks; their infimal convolution (Theorem 4) prices the deflection in the deflected linear decision rules of §6, and the experiments there compare these rules against plain linear decision rules.
Formalizing it. The proof of Theorem 1 is in the paper's online appendix, not in the main text. A search of the Prove2Me library (October 2026) found no formal statement of this or any other mean-and-support bound. A formal proof has to settle the extended-real bookkeeping (empty families, unbounded suprema) and the exact hypotheses under which tightness holds. As printed, the theorem omits a condition: with no constraint qualification it fails when is empty, which can happen for disjoint closed convex sets. This mission states the corrected version.
The upper-bound part is weak duality and needs no structure on the sets. The difficulty is tightness. It amounts to a strong-duality statement between the worst case over distributions and the infimum over the multiplier , and strong duality for convex problems over unbounded sets needs a constraint qualification. Two obvious approaches fail. The first is to search for a single worst-case distribution: for unbounded the supremum over is generally not attained, and it may be . The second is to restrict to compact , which excludes the paper's main use, a segregation of an unbounded support such as . Mathlib has separating-hyperplane theorems but no Fenchel duality theorem, so this duality has to be built.
Fin n → ℝ with IsProbabilityMeasure P, and the random vector is the identity map. Every coordinate is required to be -integrable, so the mean is a genuine expectation; the mean is MomentDRO.Conf.meanVec from the published definition MomentDRO_Conf_Setting.∀ᵐ ζ ∂P, ζ ∈ V, which needs no measurability of .max (r0 + r ⬝ᵥ ζ) 0.EReal. An empty supremum is , an empty infimum , and an unbounded supremum . The paper's "inf" is ⨅; attainment is claimed only where the Remark claims it, via the objective (pi1Obj) at and .Needed infrastructure: finite mixtures of Dirac masses as members of , integration of almost-surely bounded functions, separation of convex sets in , and a Fenchel-type duality for a concave function over a closed convex set under an interior-point condition. The duality and the concave-envelope facts are reusable well beyond this mission, including for Theorems 2–4 of the same paper. Proofs of any milestone, and reusable lemmas on extended-real suprema of integrals, are welcome.
Scheduling jobs on unrelated parallel machines to minimize the total weighted completion time is a basic model of machine scheduling: each job may take a different time on each machine, and a job becomes available on a machine only at a machine-dependent release date. In the three-field notation the problem is . Already the sequencing problem on a single machine with release dates is strongly NP-hard, so the question is how well it can be approximated in polynomial time.
Timeline (as surveyed in §1 of the paper):
This mission formalizes that last result.
There are jobs and machines. Job has a weight ; on machine it has a processing time and a release date . A nonpreemptive schedule runs every job without interruption on one machine, starting no earlier than its release date there, and each machine processes at most one job at a time. With completion times , the objective is .
Smith's order on machine : if , or the ratios are equal and .
Time slots. Sort the release dates on machine as and set . The -th time slot holds the jobs started on machine within . An assignment of jobs to slots is feasible if job goes to a slot with . For assignment variables , the slot starts are
and for a 0/1 assignment the completion time of is (17).
(CQP). Minimize with
subject to (14), if (18), (20), and (21). In matrix form the objective is , which is convex.
Randomized rounding. Each job is put into exactly one slot , with probability , the choices being pairwise independent across jobs. The resulting slot assignment is turned into a schedule by (15)–(17).
For every instance with , , :
The bound is stated for every feasible , so it needs no optimum of (CQP), and with (3) it gives the positive half of Corollary 3.6.
The result gives a -approximation for from a program of polynomial size, with a short analysis that holds job by job. The relaxation (CQP) is also the basis of §4, where the same rounding compares nonpreemptive with preemptive schedules, and its relaxation property bounds the optimum of (CQP) against the optimal schedule within a factor .
The result is proved in the paper; none of it is formalized. A formal development adds a checked model of release-date schedules and time slots on unrelated machines, the exchange argument behind Smith's rule in the presence of release dates, and a measure-free treatment of pairwise independent rounding. These pieces are reusable for other slot-based relaxations.
The analysis of Lemma 3.5 is short; the work lies in the reduction to slot assignments. Lemma 3.1 is an exchange argument, but swapping two jobs can push a job into a different time slot, so the naive bubble sort within a slot does not obviously terminate in a slot-sequenced schedule. Lemma 3.2 needs an induction across slots that accounts for empty slots and ties . Lemma 3.3 is a shifting argument on fractional solutions whose objective change is a quadratic computation, and the step size printed on p. 18 must be divided by to land exactly on . The relaxation conjunct of the goal chains Lemmas 3.1, 3.2, 3.3 and the p. 17 identity.
Jobs are Fin n, machines Fin m, and slots Fin m × Fin n, all 0-based. is cross-multiplied, which equals the page's ratio order because . is the sorted tuple of release dates; is never represented by a real number. Constraint (21) is imposed only for slots before the last, and a job's slot is the largest with . Schedules are a machine and a real start time per job; two jobs on one machine must satisfy or . Randomized rounding is a probability weight on slot assignments with marginals and product joint probabilities for distinct jobs; full independence is not required, and the product weight is one instance. The standing assumptions , , of p. 2 are hypotheses of every theorem; Lemmas 3.1 and 3.3, which assert existence, also assume .
A statement of the bound alone, , would say nothing about schedules: conjuncts 1 and 3 of the goal are what tie it to the scheduling problem, and neither may be dropped.
Not formalized: polynomial-time solvability of (CQP), the running time of the algorithm, the tightness half of Corollary 3.6, and the first sentence of Lemma 3.1 as a statement about every optimal schedule (false when some ).
Contributions welcome: proofs of any milestone; a general library of time-slot schedules; and the convexity of (22) (positive semidefiniteness of ), which is not a milestone here.