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?
A stochastic dominance constraint asks a random outcome of a decision to be at least as good as a benchmark outcome for every risk-averse decision maker: in the second-order version, for every concave nondecreasing utility . Dentcheva and Ruszczyński introduced optimization problems with such constraints in Optimization with stochastic dominance constraints (SIAM J. Optim. 2003), where the outcome itself is the decision variable, and extended the theory in the paper this mission formalizes, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints (Math. Program. 2004, DOI 10.1007/s10107-003-0453-z), to outcomes that depend nonlinearly on a decision .
The paper's §4 builds a Lagrangian dual of these problems. The multipliers of the -th dominance constraint are a utility function and an almost-sure multiplier for the coupling . The dual functional splits into a part that involves only the decision and one part per dominance constraint. This mission is about the second kind of part: Theorem 4 computes in closed form as a concave conjugate, and Theorem 5 gives its subgradients. Those two facts are what make the dual problem amenable to nonsmooth optimization and decomposition methods, which is the purpose the paper states for them.
The underlying shortfall function and its dual characterization are due to Ogryczak and Ruszczyński (Dual stochastic dominance and related mean–risk models, SIAM J. Optim. 2002). The pure-dominance case of the optimality theory is the 2003 paper above.
Let be a probability space, the integrable and the essentially bounded random variables. Fix a bounded interval () and a reference outcome .
The utility class consists of the functions that are concave and nondecreasing, vanish on , and are affine on : for , with a constant . For such , the left derivative at is that slope .
The concave conjugate of is
For a random variable , is the extended-real random variable .
The dual functional of one dominance constraint, eq. (34), is
The functional of eq. (35) is , considered on , where is the space of Lipschitz functions with norm .
For every and every ,
The formal statement has two cases. If almost surely, then is a.s. finite and integrable and the identity holds between real numbers. Otherwise .
Theorem 4 reduces an optimization over the infinite-dimensional space to one scalar maximization per scenario: the dual functional is an expected conjugate. It identifies the effective domain of the dual in the multiplier (bounded between and the slope of the utility at the left end of the interval), and it makes evaluating as cheap as evaluating . Theorem 5 supplies explicit subgradients, the law of a maximizer and the maximizer itself, which is what bundle and cutting-plane methods for the dual problem (31) consume. The paper's §5–§6 build their finite-scenario theory and numerical method on this decomposition.
Both theorems are proved in the paper. Neither has a machine-checked proof; no concave conjugate on with values in , no dual functional of this kind, and no measurable-selection theorem for argmax correspondences of this shape exist on the platform. A complete formalization would provide reusable infrastructure: an extended-real concave conjugate, interchange of supremum and expectation for a scalar integrand with a bounded maximizer, and a concrete measurable-selection argument.
The hard step is the interchange . The inequality "" is pointwise, but "" needs a random variable that attains the pointwise maximum, is measurable, and is integrable. The paper cites Rockafellar–Wets for both the interchange and the selection. The maximizers are not unique: where or the argmax is an unbounded half-line, so an arbitrary measurable selection need not be integrable, and the bounded one must be constructed. The unbounded cases need care because is only essentially bounded and the test outcomes must be shown integrable.
This chunk's objects are in NonlinSSD.DualFunctional; it imports the already moderated utility class NonlinSSD.Optimality.U1. Random variables are functions on a probability space with IsProbabilityMeasure P; is Integrable, is MemLp ζ ⊤ P. The conventions and explicit readings:
derivWithin v (Set.Iic a) a, never deriv v a, which is at a kink.EReal-valued, so an infimum equal to and a supremum equal to are represented, not replaced by . The supremum in is over integrable only.A trivializing formalization is ruled out: a real-valued conjugate or dual functional (junk at ), a supremum over all measurable (junk integrals), or a one-sided case split would each make the goal easier than the paper's theorem, and a sorry-free check confirms that both cases of Theorem 4 are inhabited (, and ).
Contributions are welcome at every level: proofs of the milestones in order, general lemmas on extended-real conjugates on , and a measurable argmax selection for continuous integrands over a compact interval, which is reusable well beyond this paper.
A multiclass queueing network can be unstable even when every station has enough capacity on average: the queue lengths grow without bound although each server's nominal load is below one. Kumar and Seidman, Lu and Kumar (1991) and Rybko and Stolyar (1992) exhibited such networks under simple priority disciplines. This raised the question of which networks are stable under every reasonable policy, and which policies are stable in every network. Dai (1995) reduced the stability of a queueing network to the stability of its deterministic fluid model, so that the question becomes one about solutions of a system of linear equations and inequalities.
Dai and Weiss (1996) use this reduction to study reentrant lines, the model of semiconductor wafer fabrication in which a single route visits the same machines many times. Section 6 of their paper treats Kelly-type lines, in which every visit to a station has the same mean service time. Kelly (1979) showed that such networks with exponential service times are stable under FIFO and have a product-form stationary distribution. Theorem 6.1 shows that with two stations, and a route that never visits the same station twice in a row, stability holds under every work-conserving policy, not only FIFO. This mission formalizes that theorem.
A reentrant line has stations and classes . Fluid enters class at rate , moves from class to class on service, and leaves after class . Class is served at station with mean service time and rate . The constituency of station is and its nominal workload is . The traffic condition (1.7) is for every .
A fluid model solution is a pair : is the fluid in class at time and the cumulative service time given to class by time . They satisfy, for ,
with nondecreasing, and the idle time , where , is nondecreasing. The solution is work-conserving if increases only at times when station holds no fluid. The immediate volume of station is .
The line is of Kelly type with station means if for every class . Its routing has no immediate feedback if for every . A set of fluid solutions is stable (Definition 1.3) if there is a such that every solution in the set with is empty from time on.
For a two-station Kelly-type reentrant line without immediate feedback that satisfies (1.7), the work-conserving fluid model is stable: there is with
for every work-conserving fluid solution . The number of classes is arbitrary, of either parity, and the route may start at either station.
The milestones follow the proof on p. 130 and the two general lemmas it uses: the extinction criterion of Lemma 2.2 (ii); the derivative of a maximum at an active index, display (3.2), already proved on the platform; the piecewise-linear Lyapunov Lemma 3.2; the drift identity for , with ; the comparison ; and the verification that meet the hypotheses of Lemma 3.2 with .
The result. Theorem 6.1 gives a class of networks in which stability needs no knowledge of the scheduling policy: any policy that never idles a server with work waiting is stable whenever the nominal loads are below one. For queueing networks this is the property usually called global stability. Through Theorem 1.1 of the paper (Dai 1995, Theorem 4.3) the fluid statement implies positive Harris recurrence of the corresponding multiclass queueing network under every work-conserving head-of-the-line policy. The paper's Remarks 2 and 3 show the boundary: with immediate feedback (the line with all means ), or with three stations, a Kelly-type line can be unstable. A two-station Kelly-type line without immediate feedback is a unidirectional ring with one customer type, so the theorem is a special case of the ring-network result the paper proves as Theorem 6.2. That result is an open goal on the platform (ProcessingNetworks.GlobalStability.ring_globally_stable, Dai and Harrison's Theorem 8.24) in a different encoding of the fluid model.
Formalizing it. The theorem is proved in the paper, and the mission formalizes that proof. No machine-checked proof of the result, or of the Lyapunov lemmas it uses, is known to exist. The mission also produces reusable pieces: a fluid model of reentrant lines in the paper's own formulation, an extinction lemma for absolutely continuous functions, and the max-of-linear Lyapunov lemma, which the paper uses again in §§3 and 5.
The obvious Lyapunov function, the total workload, does not work: a work-conserving policy may starve a station while the other one is busy, so the total content need not decrease. The paper's components each decrease at the constant rate while station is busy. When station is idle, can grow, and the argument then needs the comparison , which requires the alternating route. The analytic difficulty is the passage from these pointwise statements to extinction. Fluid paths are only Lipschitz. The maximum need not be differentiable where the maximum switches, and the drift statements hold only almost everywhere. Lemma 2.2 (ii) and the derivative-of-a-maximum fact (3.2) make this step rigorous. The proof for odd is not printed ("can be proved similarly"), and the formal goal covers it.
All objects live in the namespace DaiWeissFluid.KellyType. The conventions are fixed as follows.
Fin K, Fin I). The paper's class is Lean k - 1.ℝ → Fin K → ℝ, and every equation is imposed for only. Derivatives are taken at via HasDerivAt.The goal must not be trivialized. It quantifies over all work-conserving solutions with , and this set is nonempty: a sorry-free witness with is checked locally. Neither the Kelly-type hypothesis nor the absence of immediate feedback may be dropped (Remark 2), nor may the goal be generalized beyond two stations (Remark 3). Restricting it to even , or to a route starting at station 1, would weaken it.
Contributions welcome: proofs of the general Lemmas 2.2 (ii) and 3.2, which apply across the whole series; the drift identity, which is pure algebra from (1.8); the continuity facts for fluid paths (Lipschitz bounds from (1.10)–(1.12)); and the final assembly.
Boundary feedback is the standard way to stabilize vibrating structures governed by wave equations: a sensor measures the velocity at the boundary and an actuator applies a force proportional to it. For the one-dimensional damped wave equation with such feedback, the closed loop is uniformly exponentially stable (Chen, 1979). In practice the measured velocity reaches the actuator only after a computation time, so the feedback acts with a time delay . The question addressed by Datko, Lagnese and Polis (1986) is whether arbitrarily small delays can destroy the stability of a system that is stable without them.
Their note answers it with an explicit example and a sharp threshold on the feedback gain. It is the founding example of delay-induced instability in boundary stabilization, cited by most later work on robustness of boundary control to delays.
Timeline.
Fix real numbers (damping), (feedback gain) and (delay), and put . The delayed system is
A classical solution is a function with complex values satisfying (1), (2), (8).
Separated solutions lead to the eigenvalue problem
The spectrum is the set of for which this problem has a solution not identically zero on . The paper encodes it through the entire functions
and the critical gain . In Lean these are K a, f a k ε ω, h a k ε ω, delaySpectrum a k ε, IsClassicalSolution a k ε u and IsExpUnstableSolution a k ε u in the namespace DatkoDelayWave.BoundaryDelay.
In attack order: the characteristic equation (16) ( for ); separated solutions; Lemma 1 (one zero of forces infinitely many zeros of and in every vertical strip around it); (17)–(18) (no zeros of in the right half-plane below or at the critical gain); the half-plane bound below the critical gain; (19) (no purely imaginary zeros at the critical gain); the explicit zero ; density of the delays ; the root family (12)–(15) above the critical gain; Lemma 2 (an open dense set of delays with zeros of in ); the three parts of the THEOREM separately; and, off the goal's path, the undelayed formula for .
The result shows that exponential stability obtained by boundary velocity feedback is not robust to delays when the gain is above : delays from a dense set of lengths, including arbitrarily small ones, produce exponentially growing modes. When the critical gain is , so every positive gain is fragile. Below the critical gain the spectral gap survives every delay. This identifies a quantitative robustness margin and motivated the later analysis of delayed boundary control, including the Nicaise–Pignotti theorems already posed on the platform for a different, multidimensional model (NicaiseDelayWave.*).
The result is proved in the paper, partly by citation: Lemma 1 is quoted from Datko (1978) without proof, and the open-mapping step of Lemma 2 is sketched. No machine-checked version exists. A formalization would check the threshold computations, supply the strip-zero lemma for this exponential polynomial, and give a rigorous version of the open-mapping step.
The algebraic parts, (16)–(19) and the explicit zeros, are calculations with complex exponentials. The difficulty is in Lemma 1 and Lemma 2. Lemma 1 needs the almost-periodic structure of exponential polynomials in vertical strips together with a Hurwitz or Rouché type argument, and neither is in Mathlib. Lemma 2 needs zeros of to persist under small changes of the real parameter . The paper's route through the logarithmic map (11) does not work as printed, because it is stated with the principal branch exactly on the branch cut. In part (i), the delicate step is excluding accumulation of zeros at the imaginary axis as , which the half-plane estimate alone does not give.
Parameters are real, , eigenfunctions are maps and solutions are maps (space first). Partial derivatives are deriv of the sections. Solutions and eigenfunctions are required to be on all of , resp. ; this loses no eigenvalue, since solutions of (5) are combinations of . Committed readings of the paper's loose phrases:
Trivializing encodings are ruled out: defining the spectrum as the zero set of would make a spurious spectral point, and reading "exponentially unstable" as "the spectrum meets " would delete the solution-level content of part (iii).
A complete development needs zero-counting tools for exponential polynomials in strips (almost periodicity, Hurwitz's theorem), which would be reusable for other delay equations. Contributions to any milestone, and to that general infrastructure, are welcome.
Online set cover is the basic covering problem in which the requests arrive over time. A ground set of elements and a family of sets are known in advance, but which elements must be covered is revealed one element at a time, and each arriving element has to be covered at once by a set chosen irrevocably. The problem models resource placement under unknown demand (facilities, servers, sensors that must serve clients as they appear) and is the prototype for a family of online covering problems.
Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 2009) gave the first deterministic algorithm, with competitive ratio for elements and sets, and showed that no deterministic algorithm does better than on some instances. Buchbinder and Naor (Math. Oper. Res. 2009) recast the fractional part of that algorithm as an instance of a general online primal-dual scheme for covering and packing linear programs, and turned an offline pessimistic estimator of Srinivasan into an online potential function. The result, in their Section 5.1, is a deterministic algorithm whose ratio depends on the maximum element frequency instead of the number of sets , and on the ratio instead of .
Timeline:
A set-cover instance consists of a finite ground set of elements and a finite family of sets. For an element , is the collection of sets containing , and bounds its size: for every (the frequency). In the unweighted problem every set costs .
Elements arrive in a list . The algorithm maintains:
gives ; here is a parameter;
With , the potential is with
where is the optimum number of sets covering the arrived elements, assumed known, and . The rounding rule: each time the weight of a set is augmented, is added to if this does not increase .
Every arriving element is covered by , and at every time
This is the paper's with the constant its proof gives.
The bound improves Alon et al.'s whenever sets are many but each element lies in few of them (), and whenever the optimum is large compared with . It also shows that the fractional part and the rounding part of an online covering algorithm can be designed separately: any online fractional solution with a competitive guarantee can be rounded deterministically by an online potential function. The same method gives the routing result of Section 5.2 of the paper.
As far as is known, none of these results is machine-checked. Related formal work on the platform covers Alon et al.'s algorithm and its bound (a different potential and a different fractional update), and the general covering scheme of Buchbinder and Naor's monograph; neither states Lemma 5.1 or Lemma 5.2, nor Theorem 3.2 for the scheme with in place of . A complete development here would give a verified derandomized rounding argument, reusable for other online covering problems.
The difficulty is not in the final inequality, which follows from in one line, but in keeping throughout. The decision to take a set must be made with no knowledge of future elements, and the potential has to account for elements that may never arrive: ranges over the whole ground set. Lemma 5.1 (ii) asks that, for every current state, one of the two decisions does not increase a non-linear function of all uncovered elements at once and this must hold for every state, not only for the states a particular run reaches. On the fractional side, Theorem 3.2 is only asserted, "along the same lines" as Theorem 3.1, so its constant has to be re-derived with in place of and with the scheme's continuous increase made discrete.
A tempting shortcut is to bound by the number of rounds or by directly; neither gives a logarithmic factor in , which comes only from the choice of in .
The instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance (elements E, set indices T, incidence elemSets, positive costs c), with elementWeight and coveredBy. Unit costs are the hypothesis ∀ s, inst.c s = 1 in Lemma 5.2; Theorem 3.2 is stated for general positive costs. Logarithms are natural (Real.log), because they invert Real.exp.
Committed conventions:
sInf) at which the new constraint holds. Arrival lists may repeat elements; an element already covered changes nothing.ord containing every set, and a set is added when . Lemma 5.2 holds for every order.Not in scope: the packing half of Theorem 3.2, Theorem 3.1 for general coefficients, and the doubling wrapper of p. 12 that removes the assumption that is known. The guarantee is for the algorithm run with the stated ; a formalization in which 's product ranges only over arrived elements, or in which the weights or the chosen family are free variables constrained by hypotheses instead of being produced by the algorithm ( is an input of the algorithm, as the page assumes it known), would be a different and weaker statement and is ruled out.
Contributions welcome: proofs of the three milestones and of the goal, and general lemmas about the fractional round (attainment of the least , monotonicity of the weights) that other online covering missions can reuse.
Alternating direction methods are used when one part of an optimization problem is easy to minimize and another part has a simple projection. Chapter 9 of Boyd, Parikh, Chu, Peleato and Eckstein (2011) examines this idea with nonconvex constraints. Its examples include sparse vectors, Boolean vectors and low-rank matrices. The chapter says explicitly that ADMM can fail to converge in this setting and that a limit need not be globally optimal. The useful claim here is narrower and concrete: several individual updates can still be computed exactly.
The capstone is factor-model fitting. A symmetric data matrix, such as an empirical covariance matrix, is approximated by a positive semidefinite matrix of prescribed rank plus a nonnegative diagonal matrix. This decomposition gives one component that captures shared variation and another that represents coordinate-specific variation. The chapter separates the diagonal fit from the rank constraint and writes the resulting ADMM X-update entry by entry. This mission formalizes that exact update and two other projection rules stated in the same chapter.
Fix a positive integer . Write for the real symmetric matrices, and let be the matrix to approximate. The Frobenius norm squares and sums every ordered matrix entry: . A vector is nonnegative when for every , and places those entries on a diagonal matrix. The book's reduced fitting loss is
In the scaled ADMM iteration, carries the positive semidefinite rank constraint and is the scaled dual matrix. Given the current symmetric matrices and a penalty , the X-step minimizes over . The X-step itself has no rank or positive semidefinite restriction. The following Z-step projects onto the chosen rank-constrained positive semidefinite set. The theorem here concerns the X-step, whose definition is independent of the chosen rank.
The other two results concern Euclidean projection of vectors . The cardinality is the number of nonzero coordinates of . The sparse set is for a nonnegative integer . The Boolean cube is . Projection means a nearest point in squared Euclidean distance; it may have more than one value when coordinates tie.
The first milestone identifies the book's infimum as the explicit componentwise loss and states that the optimizing diagonal is attained:
The sum over counts both and . The statement preserves that convention instead of treating a symmetric matrix as a list of independent upper-triangular entries.
The page 74 milestones say that retaining the entries of largest absolute value gives a nearest point in , and that rounding every coordinate to a nearest element of gives a nearest Boolean vector. They assert nearest-point status for ties without asserting uniqueness. These are chapter results on the same theme of exact nonconvex updates, although they are independent of the factor-model goal.
The goal identifies the unique symmetric minimizer of the X-subproblem. With , its off-diagonal and diagonal entries are
The target asserts both the formula and global minimality over symmetric matrices. It does not replace minimality with a stationarity condition.
The exact X-update separates the matrix fit from the nonconvex rank projection. It establishes that the factor-model algorithm's X-step is a well-defined, single-valued minimization for every symmetric current state and every positive penalty. It also makes the one-sided diagonal loss explicit: a nonnegative diagonal can absorb a shortfall below , but cannot absorb an excess. The two vector projections give similarly exact updates for sparse and Boolean constraint sets.
The mathematical claims are given in §9.1–9.1.2 of the published monograph; they are not open conjectures. The formalization work is to check the infimum, projection and unique-minimizer statements with every domain and tie convention explicit. The mission poses theorem statements for proofs; these draft statements themselves do not yet supply machine-checked proofs. A complete development can reuse its finite matrix loss and finite vector projection vocabulary in other splitting algorithms.
The diagonal partial minimization is one-sided, while the proximal penalty is symmetric around . An entrywise formula alone does not show that the assembled matrix minimizes the full objective or that it is the only minimizer. Symmetry also couples the two displayed off-diagonal positions and , so a scalar statement on one entry must agree with its transpose. For sparse projection, ties at the cutoff make a rule phrased as “the projection” ambiguous. For Boolean projection, the midpoint is a tie and requires a declared convention. These issues are part of the theorem statements, not numerical implementation details.
Matrices are Matrix (Fin n) (Fin n) ℝ; symmetry is an entrywise equality predicate. The factor-model statements assume , symmetric , and . The book uses at an iteration; the Lean theorem uses those current matrices as parameters and does not posit convergence of an ADMM sequence. The reduced loss is literally the infimum over all componentwise nonnegative , and the Frobenius square is the finite sum of entry squares. The stated X-minimization ranges over all symmetric matrices, with no positive semidefinite or rank hypothesis on .
For sparse vectors, the index set has size and its selected magnitudes dominate unselected ones. This covers , and cutoff ties. The Boolean rounding function chooses zero when an entry equals . The book uses indices ; Fin n uses . On page 75 the printed diagonal branch conditions omit the superscript on and ; the formalization uses the current that appear in the surrounding ADMM update. The theorem requires the candidate to minimize the book's reduced loss, preventing an arbitrary replacement loss from making the statement trivial.
The development needs finite-sum algebra, real infima with an attained lower bound, symmetry of matrices, and nearest-point arguments for finite vectors. The rank- singular-value projection on page 74 is already an open target elsewhere and is outside this mission. The positive semidefinite rank- eigenvalue projection on page 76 is also outside this goal; it would require a separate spectral development. Contributions that prove the three milestones or the goal against these definitions are in scope. The page also mentions rounding under integer constraints; this mission selects the preceding Boolean claim as its projection milestone.
The single-machine scheduling problem asks for an order in which to process jobs, each with a processing time and a weight, on one machine, respecting a partial order of precedence constraints, so that the weighted sum of completion times is as small as possible. It is NP-hard, and the best known approximation ratio for general precedence constraints is . Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) relate the problem to the dimension theory of partial orders: their Theorem 3.2 states that when the precedence constraints are given together with a realizer of size , the problem has a -approximation algorithm. Small realizers of structured precedence orders therefore translate directly into better approximation ratios.
This mission formalizes one such structural result, Lemma 4.1 of the paper: every convex bipartite order has a realizer of size . Convex bipartite orders form a class of precedence constraints that lies strictly between strong bipartite orders and general bipartite orders (Möhring, 1989). Combined with Theorem 3.2, the lemma gives a -approximation for on this class. According to the authors, the bound for convex bipartite orders had not been known before.
A poset is a set with a reflexive, antisymmetric, transitive relation . Two elements are incomparable, written , when neither nor ; the set of incomparable pairs is . A linear extension of is a linear order on with . A linear order reverses the pair when in . A realizer of size is a family of linear extensions of such that every incomparable pair is reversed by at least one . The dimension is the least for which a realizer of size exists.
A convex bipartite order has jobs split into minus jobs and plus jobs . Each plus job carries two indices , and a minus job precedes exactly when . There are no other precedences: the predecessors of each plus job form a nonempty interval of consecutive minus jobs.
For the Appendix construction, the incomparable pairs are sorted into three sets according to the kinds of the two jobs, the order of their indices and, for a pair (plus job , minus job ), whether precedes some plus job of larger index than . The sets describe what the -th linear order of the realizer must contain.
Equivalently, . The goal holds for every numbering of the jobs and every choice of interval ends .
The result. Lemma 4.1 places convex bipartite orders among the classes of precedence constraints for which has an approximation ratio strictly below , namely through Theorem 3.2 of the paper. The bound is tight: a bipartite order has dimension exactly when it is a strong bipartite order (Möhring), so the bound cannot be lowered for the class of convex bipartite orders. Since also gives for the graph of incomparable pairs, a -realizer yields an optimal colouring of that graph.
Formalizing it. The result is proved in the paper, with a short case analysis in the Appendix. No machine-checked proof is known to exist. Mathlib has no dimension theory of posets: realizers, reversals of incomparable pairs and the construction of linear extensions containing a given acyclic relation have to be set up here. The definitions of realizer and linear extension are stated for an arbitrary relation and can be reused for other dimension bounds (interval orders, semiorders, the other missions of this series).
The three relations are not partial orders. , for instance, is not transitive: with two minus jobs and one plus job with , the pairs and are present but lies in . The step that requires work is to show that each has no cycle, so that it extends to a linear order. For this depends on the convexity of the predecessor intervals and on the numbering of the plus jobs by their left ends: it is not a consequence of bipartiteness alone. The goal itself carries no numbering assumption, so any proof must also account for renumbering the plus jobs.
All declarations live in the namespace SingleMachinePrec.ConvexBipartite.
N → N → Prop. Linear orders use Mathlib's unbundled class IsLinearOrder. A linear extension of is a linear order with ; reverses when and . A realizer of size is a function Fin t → N → N → Prop, so repeated members are allowed, as in the paper's multisets.Fin a ⊕ Fin b: Sum.inl i is the minus job , Sum.inr k the plus job , with indices starting at . The interval ends are maps l r : Fin b → Fin a with l k ≤ r k, and is equality together with the pairs (minus , plus ) with . A file-level instance records that is a partial order. Any convex bipartite order in the paper's sense is one of these after naming its jobs. The cases and are allowed.Monotone l of this milestone only.A trivializing formalization would let the members of the realizer be arbitrary relations, which makes reversing every pair free. Here every member must be a linear order containing .
Contributions welcome: proofs of the two milestones and of the goal; a general lemma that a relation whose transitive closure is antisymmetric extends to a linear order on a finite type; and the renumbering argument that removes the numbering assumption.
Path-following interior point methods solve a linear program by tracking its central path, a smooth curve that runs through the interior of the feasible set and ends at an optimal solution. Their number of iterations is polynomial in the bit size of the input, and whether some interior point method is strongly polynomial (bounded by a polynomial in the number of variables and constraints alone) is open. Bayer and Lagarias called the central path "a fundamental mathematical object underlying Karmarkar's algorithm". Dedieu and Shub proposed its total curvature as an informal complexity measure: a path that turns little should be easy to follow with straight steps. Several results bound that curvature:
A linear program in slack form has a real matrix , , and :
For the point of the central path is the unique solution of
The primal central path is .
For and , the program minimizes over subject to
With slacks it becomes with , , .
For points of Euclidean space with , the turning angle is the angle between the vectors and . For a curve parameterized over , the total curvature is
The milestones also use the field of absolutely convergent generalized real Puiseux series . Such a series can be evaluated at large real , and it has a valuation , its leading exponent. Read over , is one linear program. The valuation of its central path at is the tropical central path , a piecewise-linear curve with an explicit recursive description (Propositions 20–21 of the paper).
For every and there is such that for all ,
for the central path of . Here may depend on and . Both the primal and the primal-dual curves are part of the goal, as in the paper.
The theorem shows that the total curvature of the central path is not bounded by any polynomial in the number of constraints: has constraints and curvature at least about . This settles the conjecture of Deza, Terlaky and Zinchenko in the negative. It also shows that the averaged upper bounds of Dedieu–Malajovich–Shub and De Loera–Sturmfels–Vinzant cannot hold for every region. A companion mission of this series formalizes the paper's second main result, an exponential lower bound on the number of iterations of log-barrier path-following methods on the same family.
The result is proved on paper. As far as is known, it has not been formalized in any proof assistant, and Mathlib has no notion of the total curvature of a curve, of Puiseux-series evaluation and valuation, or of the tropical central path. Formalizing the theorem would give a machine-checked reference point for a much-cited negative result in interior point theory. The Lean definitions of total curvature and of the turning angle are general and reusable.
The total curvature is a supremum over inscribed polygons, and a lower bound needs explicit polygons whose angles can be estimated for every large . The central path of has no closed form, so its points cannot be written down at given parameters . Numerical evidence at a fixed says nothing uniform in . The natural first idea, to compute the path's angles directly from system (1) for a fixed instance, gives no handle on how the number of turns grows with . What is needed is control of the path's geometry uniformly over the whole scale of , with turns located at once, and the threshold is not explicit.
Vectors in which angles are measured are EuclideanSpace ℝ (Fin d). The turning angle is InnerProductGeometry.angle (V - U) (W - V), not Mathlib's vertex angle ∠ U V W, which is minus it. A degenerate triple ( or ) contributes angle . Total curvature is an EReal-valued supremum over strictly increasing parameter sequences in the parameter set, and the goal uses the set . The primal and primal-dual curves are the vectors and . System (1) is the published Vanderbei central-path system with objective . The goal quantifies over every curve solving (1) for all . Existence and uniqueness of that curve is the referenced platform statement VanderbeiLP.CentralPath.central_path_exists_unique and is not posed again. Indices are the paper's, 1-based, mapped to Fin by subtracting one. Powers use integer exponents of the real number .
A trivializing formalization is ruled out explicitly: the curvature is a supremum in EReal (a real sSup of an unbounded set would be ), the turning angle is not the vertex angle, and degenerate polygons cannot add spurious right angles.
Lemmas 22–24 are stated over a model of by coefficient functions with the paper's support and absolute-convergence conditions. Equalities, products and order in are expressed through evaluation at all sufficiently large , which is how the paper characterizes them. Table 1 and the claims of the proof are stated for the explicit tropical central path of given by Propositions 20–21 (milestones of the companion mission), written as a definition here. One repair: the paper's "uniquely attained" claim fails at , , where . It is stated with that case excluded, which the proof does not use.
Welcome contributions: a general theory of total curvature of curves (monotonicity under refinement, behaviour under limits), asymptotics of evaluated Puiseux series, and the comparison between the central path over and its real specializations.
Single-machine scheduling with precedence constraints asks for an order in which one machine processes jobs while respecting prescribed comparisons between them. For the objective of minimizing total weighted completion time, the structure of the precedence order can influence the quality of approximation algorithms. Ambühl, Mastrolilli, Mutsanas, and Svensson connect one such approach to coloring a graph built from the order's incomparable pairs. A bounded number of colors would make a certain class of coloring-based guarantees uniform over the class of precedence orders. Their Theorem 4.3 shows that canonical interval orders have no such uniform bound for this particular graph. Ambühl et al., §4.2, p. 658
An interval order is a partial order whose elements can be represented by closed real intervals, with one element strictly before another when the first interval ends before the second begins. Interval orders are a familiar restriction of general precedence systems. The paper distinguishes them from semiorders, represented by intervals of equal length, for which it reports a three-element realizer bound and a corresponding scheduling guarantee. The chromatic obstruction here explains why that particular bounded-color route cannot be extended uniformly from semiorders to all interval orders. It does not assert that every scheduling approach to interval orders fails. Ambühl et al., §§3–4.2, pp. 656–658
For an integer , let be a linearly ordered set with points. The canonical interval order has one element for every pair of distinct points in , viewed as the closed interval . For two such intervals, write when or the right endpoint of is strictly less than the left endpoint of . Thus intervals that touch at an endpoint remain incomparable. The formalization represents each interval by its two-element endpoint set, and its order relation is equivalent to this endpoint rule. Ambühl et al., §4.2, p. 658
For any partial order on a ground set , an ordered incomparable pair is with neither nor . Both and are vertices when and are incomparable. A linear extension of is a linear order on the same elements that contains all comparisons of . It reverses if it places before . The graph has the ordered incomparable pairs as vertices. Two distinct vertices form an edge when no linear extension reverses both, while each singleton can be reversed by some linear extension. This singleton condition is the minimality clause in the paper's definition through its hypergraph of incomparable pairs. Ambühl et al., §2.1, p. 655, §3, p. 656
A proper -coloring assigns one of colors to every vertex of so that endpoints of an edge have different colors. The graph's chromatic number is the least positive number of colors that works, when the graph is nonempty. The mission uses the equivalent predicate that no proper map into a fixed -element color set exists once is large enough. This also gives a clear interpretation at .
The goal is Theorem 4.3: for each fixed integer , all sufficiently large canonical interval orders have incomparable-pairs graphs with chromatic number greater than . With , the Lean target is
The paper states as an integer. Its negative cases are immediate from nonnegativity of chromatic numbers; the target states the substantive range. The threshold may depend on , while and are constructed from rather than supplied as arbitrary objects. Ambühl et al., Theorem 4.3, p. 658
Two assertions from the theorem's proof serve as milestones. First, is nondecreasing as increases. Second, for four endpoints , the vertices and are adjacent in . They are recorded with their wording and provenance from §4.2. A separately published theorem on hypergraph Ramsey numbers is included as a reference because the source uses that theorem in its large- argument. Ambühl et al., proof of Theorem 4.3, p. 658
The result provides a precise structural limitation: across the canonical interval orders, the chromatic numbers of cannot be bounded by one constant. The graph is a specific graph of ordered incomparable pairs, distinct from other graphs that can be associated with a scheduling instance. Thus the conclusion addresses the bounded-color approach attached to this graph, without asserting an algorithmic impossibility for interval-order scheduling. The paper contrasts this limitation with the bounded-realizer situation for semiorders. Ambühl et al., §§3–4.2, pp. 656–658
The theorem is proved in the 2011 paper. The remaining work in this mission is a machine-checked development of its definition layer, its two stated supporting assertions, and the unbounded-color conclusion. The partial-order property of is already proved in the definition file; the three theorem statements are open proof targets in the proposal. A completed formalization would also give reusable components for finite interval orders, ordered incomparable pairs, and coloring arguments in dimension theory.
A pair of intervals overlapping or touching is easy to recognize as incomparable, but graph adjacency has a stronger meaning: it quantifies over every linear extension of the entire partial order. A local test based only on the four displayed intervals would silently change the graph. Likewise, the fact that two vertices have different endpoint descriptions does not by itself make them adjacent. The formal argument must connect the canonical interval representation to the global extension-based edge condition, then show that a bounded coloring cannot persist as the endpoint set grows. Ambühl et al., proof of Theorem 4.3, p. 658
The endpoint set is Fin n, hence indexed rather than the paper's ; the shift preserves order. Elements of are exactly two-element subsets of this set. The order relation includes equality and strict separation of endpoint sets and is proved to be a partial order. The graph is defined for an arbitrary binary relation so it can be reused, but every target here applies it to the concrete partial order . Vertices are ordered incomparable pairs, and adjacency retains both singleton reversibility and failure of simultaneous reversibility. Defining adjacency directly from the desired four-point pattern would trivialize the target and is excluded.
Colorable n k means existence of a proper function from all vertices of to Fin k. For an empty graph, zero-colorability is allowed by this representation. The theorem therefore includes a threshold and quantifies over every ; the assertion itself forces the threshold past any empty-graph exceptions. The formal target uses natural ; the paper's negative integer values need no separate theorem. No asymptotic notation or unspecified constants occur. The source's Ramsey number is not hard-coded into the goal, because the source asserts existence of a suitable threshold, not that the least threshold equals that value.
The printed adjacency justification names an alternating-cycle pair set different from the two adjacent vertices in the preceding sentence. The milestone formalizes the adjacency assertion itself and records the printed explanation verbatim for review; it does not turn the mismatched pair set into a hypothesis. The mission needs finite order embeddings, linear extensions, graph colorings, and a finite Ramsey theorem. The existing published Ramsey theorem is referenced as a reusable result. No scheduling approximation algorithm, polynomial-time statement, or numerical scheduling guarantee is formalized in this mission.
Expected utility theory explains a single attitude toward risk by the curvature of a utility function of final wealth: a concave utility makes a decision maker risk averse, a convex one risk seeking. Several well documented patterns of behaviour do not fit this picture. The same people buy insurance against small-probability losses and buy lottery tickets with small-probability gains (Friedman and Savage, 1948, doi:10.1086/256692); subjects who are risk averse for gains are risk seeking for the mirrored losses, the reflection effect; and subjects who are indifferent between full insurance and bearing a risk reject half-price insurance that pays only half the time, probabilistic insurance (Kahneman and Tversky, 1979, doi:10.2307/1914185).
David E. Bell's 1982 paper Regret in Decision Making under Uncertainty (doi:10.1287/opre.30.5.961) proposes that a decision maker cares not only about what she obtains but also about what she would have obtained had she chosen differently. Its first part (the companion mission of this series) derives the representation ; its Section 2 shows that the single additive form with linear explains all of the patterns above at once, provided the regret function is decreasingly concave. Regret theory, developed at the same time by Loomes and Sugden (1982, doi:10.2307/2232669), remains one of the standard alternatives to expected utility in decision analysis and behavioural economics.
A decision maker chooses between two alternatives and . Uncertainty is described by finitely many states with probabilities ; in state alternative gives final assets and gives . Choosing means forgoing , and an outcome is valued by the regret utility
where is the final assets received, the assets the foregone alternative would have given in the same state, and the regret function. The expected utility of selecting when is foregone is
and is strictly preferred to when (the paper's inequality (1)); and are indifferent when the two expected utilities are equal.
The comparisons are given by three payoff tables. Table II: a horse wins with probability ; betting \p1-p-p0p1-p-10q-10-p-p-1-p/2$.
The regret function is decreasingly concave if it is twice differentiable with strictly increasing second derivative . Section 3 also uses and the negative exponential , .
If is decreasingly concave and , then the bet of Table II is strictly preferred to not betting and insuring in Table III is strictly preferred to not insuring:
Both comparisons have equal expected values, so the statement is a pure regret effect. The goal fixes no constants and assumes nothing about beyond decreasing concavity; it is the weakest hypothesis the page offers.
holds iff full insurance is strictly preferred to probabilistic insurance, iff probabilistic insurance is strictly preferred to self insurance; and (11) follows from the same ratio condition. 5. The negative exponential (Sec. 3): concave, convex on , strictly increasing on , and decreasingly concave.
The goal is the paper's central behavioural claim: one regret function explains why the same decision maker gambles on long odds and buys insurance at fair prices, behaviour that a single concave or convex utility of wealth cannot produce. The milestones show that the reflection effect and the rejection of probabilistic insurance follow from the same model, and two of them reduce to the same inequality on the odd part of the regret function. The negative exponential example shows the hypotheses are met by a concrete, commonly used function, so the explanation is not vacuous.
The results are proved in the paper by short calculations, and none of them has been machine-checked before. The mission produces a formal statement of the regret model of Section 2 with its payoff tables, which pins down several points the printed text leaves loose: the meaning of "decreasingly concave", the domain on which "increasing" and "convex" are meant, and three misprinted intermediate displays.
The comparisons (5), (6), (9) and the reflection identity are algebraic once the payoff tables are expanded; the work is in expanding them correctly, since the foregone argument of changes with the alternative selected and three printed expansions are wrong. The substance lies in the analytic step: passing from a pointwise condition on to strict monotonicity of on , with strict inequalities throughout and through a quotient that is undefined at . The naive reading of the page's condition, " for all ", is unsatisfiable and cannot be used as a hypothesis.
All quantities are real numbers. The utility is regretU f x y = x + f (x - y), i.e. form (4) with exactly; the page assumes only "approximately linear" but computes every display with . A comparison is a finite state space Fin n with a real weight vector; the theorems instantiate it with for Tables II–III and with for Table IV, the accident state split by whether the insurer pays. Strict preference is strict inequality of expected regret utilities; indifference is equality.
Conventions and corrections, each disclosed in the item concerned:
Differentiable ℝ f, Differentiable ℝ (deriv f) and StrictMono (deriv (deriv f)). The page's presumption that is increasing and concave is not assumed.The goal cannot be satisfied vacuously: the negative exponential milestone exhibits a decreasingly concave , and the conclusion is a strict preference between two alternatives of equal expected value. Section 2(iv) (preference reversals) is not formalized: its printed rewriting of (12) in terms of drops a linear term and its conclusion is unquantified ("for sufficiently small units of money").
Contributions welcome: proofs of the algebraic reductions, the slope argument for , and the convexity facts for ; the latter two are reusable beyond this mission.
Many planning problems are made in two stages: a first decision is fixed before an uncertain parameter is revealed, and a second decision is taken afterwards. Two models compete for such problems. Two-stage stochastic optimization assumes a probability distribution over the scenarios and minimizes the expected cost, letting the second-stage decision depend on the scenario. Robust optimization asks for one solution that is feasible in every scenario and minimizes the worst-case cost. The robust problem is usually far easier to solve: it is a single deterministic problem, while the stochastic problem optimizes over policies. The question is how much cost one gives up by solving the easy problem instead of the hard one.
Bertsimas and Goyal (Math. Oper. Res. 2010) measure this loss by the stochasticity gap, the ratio of the robust optimum to the stochastic optimum. Their Theorem 2.1 shows that when only the right-hand side of the constraints is uncertain, the uncertainty set is symmetric and the distribution is centred at the point of symmetry, the robust optimum is at most twice the stochastic one. Section 3 asks whether the same holds when the second-stage costs are uncertain as well, and answers no with an explicit instance: Theorem 3.1. This mission formalizes that instance.
There are no first-stage variables. The second-stage decision is a vector with continuous coordinates, subject to the single covering constraint
the constraint with and . A set of scenarios carries a cost map ; in scenario the second-stage cost is . The uncertainty set is , here : the range of is the whole cube . A probability measure on makes the coordinates independent, each uniformly distributed on .
The stochastic problem , display (1.4) of the paper, chooses a policy satisfying the constraint in every scenario and minimizes ; its optimal value is . The robust problem , display (1.5), chooses one satisfying the constraint and minimizes ; its optimal value is . A set is symmetric (Definition 1.2) if there is with for every .
The Lean development names these zStochBD and zRobBD (the general problems (1.4) and (1.5) with data , , , , and integer coordinate sets), and IsSymmetricAbout (Definition 1.2).
The constant is the paper's. Both sides are pinned down separately by the milestones, so the goal cannot be satisfied by a degenerate value of either side.
Theorem 3.1 marks the boundary of the paper's positive results. The bound of Theorem 2.1 needs only symmetry of the uncertainty set and a centred distribution. The instance here has both, has no integer variables and a single constraint, and still has a gap that grows linearly in the dimension. So symmetry alone does not make a robust solution a good approximation of the stochastic optimum when costs are uncertain. The paper's abstract states this as one of its main conclusions, and it is why Sections 4 and 5 compare the robust problem with the adaptive problem, whose worst-case objective does not suffer from it.
The result is proved in the paper; to our knowledge it has no machine-checked proof. What this mission adds is a formal proof of the instance against the general definitions of the two-stage problems, including the probabilistic computation (3.2), the expected minimum of independent uniform random variables, which Mathlib does not contain. That computation is reusable wherever order statistics of uniforms appear, for example in auctions, secretary problems and random-assignment bounds.
The robust half is short. The stochastic half has two parts. Eq. (3.1) needs a measurable policy that selects a cheapest coordinate; the policy printed in the paper puts a unit on every minimizing coordinate, which at ties overpays, so a formal proof must choose a single minimizer measurably and use integrability on the probability space. Eq. (3.2) is the main work: it is a genuine integral over the -dimensional cube against a product measure, for every , and Mathlib has no lemma on the distribution or the expectation of the minimum of independent random variables.
Fin k → ℝ with the componentwise order; is the all-ones Matrix (Fin 1) (Fin n) ℝ, and live on Fin 0, , and the integer coordinate sets are empty ().EReal, when infeasible; the robust worst-case cost is an EReal supremum. No optimal solution is assumed to exist: the paper's "consider an optimal solution" is a proof device, and the statements are about the infima.A real-valued infimum would assign the value to an infeasible or ill-posed problem and make the goal trivially true; the EReal infima, and the separate milestones fixing and , rule that out.
Contributions are welcome on each milestone separately. The expected-minimum computation (3.2) is self-contained and of independent use; a general lemma on the law of the minimum of independent random variables would serve it and other missions.
Expected utility theory predicts that a decision maker's choice between two lotteries depends only on the distribution of final wealth under each. Observed behaviour contradicts this in systematic ways: the Allais paradox, the coexistence of insurance and gambling, and the reflection effect documented by Kahneman and Tversky (1979). David Bell's 1982 paper (Operations Research 30(5), 961–981) explains these patterns by regret: the dissatisfaction of learning that the alternative not chosen would have done better. In the same year Loomes and Sugden (1982) proposed a closely related theory; together the two papers are the origin of regret theory in decision analysis.
Bell's contribution is axiomatic. Instead of postulating a regret term, he derives the shape of a utility function that incorporates regret from three behavioural assumptions about how preferences respond to shifting all outcomes by an equal increment of value. This mission formalizes that derivation, Section 1 of the paper (pp. 965–970), culminating in Theorem 1.
An endpoint is described by two attributes: the final assets and the foregone assets , the asset level the decision maker would have had under the alternative not chosen. Utility is a function , strictly increasing in and strictly decreasing in .
A simple comparison is a choice between two alternatives whose uncertainties are resolved by one predetermined joint distribution. With states, a probability vector and alternatives ( the final assets of in state ), the expected utility of selecting while is foregone is
and is preferred to when (inequality (1) of the paper).
A value function , strictly increasing and onto , measures incremental value: moving from to is worth . An alternative is obtained from by a shift of incremental value if for every state.
Under Assumptions 2 and 3, there are a constant and a function with
Utility separates additively into a term in the value of final assets and a function of the regret . The coefficient is left free (see Formalization scope).
The additive form is the basis of the rest of Bell's paper: Section 2 uses it to show that a single decision maker with decreasingly concave both buys fair insurance and takes long-odds bets, and to account for the Allais paradox and the reflection effect. The same additive structure, a value term plus a function of the regret difference, is the form in which regret theory has been used since, alongside the parallel proposal of Loomes and Sugden (1982). Lemmas 1 and 2 have independent content: simple comparisons identify only the antisymmetric part , and the lemmas pin that part down to a function of the regret difference.
The results are published with proofs in prose; none has a machine-checked proof. Formalizing them checks the argument as printed, which turns out to need a correction (the coefficient of in (4)), and fills in the regularity steps the paper leaves implicit: the solutions of the Cauchy equations that appear, and the passage from to a general value function.
The obvious argument reads each assumption as a functional equation and solves it. Two steps resist this. First, the functional equations and have non-measurable solutions; excluding them needs boundedness of and on intervals, which must be extracted from the monotonicity of and is never stated on the page. Second, the proof of Theorem 1 compares two 50-50 lotteries that are indifferent and requires to take an arbitrary value ; when is bounded no such indifference exists, so the printed step does not cover every case. Passing from to a general requires transporting all three assumptions along .
u : ℝ → ℝ → ℝ with u x y . Every theorem assumes strictly increasing in and strictly decreasing in (the paper's "increasing"/"decreasing", p. 965, read strictly).Fin n and two alternatives on the same states. Assumption 3 quantifies over four alternatives on one common state space, the setting of the paper's own use of it.Online bipartite matching models a platform that must commit each arriving request to a resource immediately. The motivating application of Feldman, Mehta, Mirrokni and Muthukrishnan is display advertising: an ad server knows from past traffic how many impressions of each type (web page, audience segment) to expect, sells them to advertisers in advance, and must assign each impression to an interested advertiser the moment a user loads the page. The goal is to fill as many contracted impressions as possible.
When arrivals are chosen by an adversary, the best ratio an online algorithm can guarantee is , achieved by the RANKING algorithm of Karp, Vazirani and Vazirani (STOC 1990). The ad server, however, is not facing an adversary: it has a forecast. The i.i.d. model captures this: the graph and the distribution of impression types are known in advance, and the impressions are independent draws. The paper asks whether this knowledge allows an online algorithm to beat , and answers yes.
Timeline.
An instance is a bipartite graph with a finite set of advertisers, a finite set of impression types, and edges recording which advertisers want which types. The mission treats the case analysed throughout §4.2 of the paper, in which one impression of each type is expected (). So impressions arrive one at a time, with types drawn independently and uniformly from . On arrival an impression must be assigned at once and irrevocably to a still unassigned advertiser adjacent to its type, or discarded. is the number of impressions an algorithm assigns. is the size of a maximum matching of the realization graph, which has one node per arrival , joined to every advertiser with .
The two suggested matchings (TSM) algorithm works offline first. Its boosted flow graph has a source arc of capacity into every advertiser, a unit-capacity arc along every edge of , and an arc of capacity from every type to a sink. The algorithm takes the edge set of an integral maximum flow. Every vertex then has at most two edges of , so splits into vertex-disjoint paths and cycles. The algorithm colours each component blue and red:
Online, the first arrival of type tries the advertiser along 's blue edge, the second tries the one along its red edge, and later arrivals are discarded. A tried advertiser that is already taken is not reassigned. The advertisers fall into four classes by their coloured edges: (one blue, one red), (two blue), (one blue only) and (one red only).
Let
The goal has three parts. First, every maximum flow edge set admits a colouring that follows the rules. Second, for every and there are and such that, for every instance with , every maximum flow edge set and every rule-following colouring,
Third, .
The theorem separates the i.i.d. model from the adversarial one: knowing the distribution is worth a constant factor above . The suggested matching algorithm of the same paper (Theorem 4) shows that following a single offline matching gets exactly , so the second, red matching is what crosses the barrier. The paper's question started a line of work on the i.i.d. and random-order models, with later improvements to the constant by other authors under further assumptions.
The result has a written proof but, as far as the platform record shows, no machine-checked one. The mission formalizes the paper's own argument: the flow-and-colouring construction, the balls-in-bins concentration facts, the cut-based bound on OPT and the combinatorial Lemma 1. It also fixes two slips in the printed statements (see Formalization scope). The pieces are reusable beyond this paper. The occupancy concentration (Fact 1) and the satisfied-sequences bound (Fact 2) recur in analyses of online algorithms with stochastic input. The degree-capped flow encoding and its path/cycle decomposition are standard tools for 2-matchings.
The upper bound on OPT is the delicate part. A cut of the flow graph bounds the maximum matching of the realization graph only after a second surgery that depends on the random arrivals. Its size must then be compared with the colour classes, which are defined by a different structure (the components of ). Lemma 1 bridges the two, and it depends on the exact colouring rules: a colouring that only satisfies local degree conditions can put red edges at both ends of an even advertiser path, which breaks the inequality behind (2). On the probabilistic side, the advertisers of share impression types with each other, so the success events are dependent, and Fact 2 needs a bounded-differences argument in which one ball affects up to sequences.
All declarations live in the namespace OnlineStochMatching.TSM. Advertisers and types are finite types A I : Type, and is a Finset (A × I). Probabilities are counting ratios , so there are no measurability side conditions. OPT is a maximum over the finite, nonempty set of partial injective assignments. An integral flow of is its set of saturated middle edges, i.e. a subset of with at most two edges per vertex; is such a set of maximum cardinality. A colouring is given by a listing of the components of as vertex sequences. Every theorem quantifies over every maximum and every colouring the rules allow, since the paper fixes neither.
The paper's asymptotic phrases are replaced by explicit quantifiers that come from its own proofs:
Corrections to the printed statements:
The ratio is multiplied out, so no division by OPT occurs. A colouring condition that is unsatisfiable, or a flow set that is not maximum, would make the goal vacuous or false; part (a) of the goal rules out the first, and every statement requires maximality. Not included: the reduction to general integer (§4.2.4), the tightness sentence of Theorem 5 (§4.2.5), and footnote 7's variant of the algorithm.
Useful infrastructure: bounded-differences (McDiarmid/Azuma) inequalities for functions of i.i.d. uniform variables, which exist on the platform as separate theorems; path/cycle decomposition of graphs of maximum degree two; and max-flow min-cut for unit-capacity bipartite networks. Contributions are welcome on Facts 1 and 2 independently of the combinatorics, and on Lemma 1 and equations (1) and (3), which are deterministic.
A retailer that groups its products into categories (brands, store sections, flight classes) and decides which products to display in each faces the assortment problem: offering more products attracts more customers but also diverts sales away from the most profitable products. The nested logit model is the standard description of customer choice in this setting. A customer first selects a category (a nest), then a product within it. Choice-based models of this kind are the basis of revenue management under customer choice (Talluri and van Ryzin 2004).
Davis, Gallego and Topaloglu (DGT 2014) study the assortment problem under the nested logit model with two features that earlier work excluded: dissimilarity parameters larger than one, under which products in a nest act as complements rather than substitutes, and a no-purchase option inside each nest, under which a customer may enter a nest and still leave without buying. They show that the problem is NP-hard once either feature is present. For each regime they give a small linear program whose solution yields an assortment with a provable performance guarantee. This mission formalizes the guarantee for the most general instances, where both features occur together (§6.1, Theorem 11).
Timeline. Rusmevichientong, Shmoys and Topaloglu (2010) bound nested-by-revenue assortments under a multinomial logit mixture. [DGT 2014] prove that nested-by-revenue assortments are optimal for dissimilarity parameters at most one without within-nest no-purchase options (Theorem 4). They give factor-(6) guarantees with synergistic products, a factor-two guarantee via knapsack relaxations for partially-captured nests (Theorem 10), and the general factor (12) of Theorem 11. Li, Rusmevichientong and Topaloglu (2015) extend the nested-by-revenue result to -level nested logit models.
There are nests and, in each nest, products . Product of nest has revenue and preference weight , with . Nest has a no-purchase weight and a dissimilarity parameter , and is the weight of choosing no nest at all. For an assortment ,
A customer chooses nest with probability , and the expected revenue is
The optimal value of equals the optimal value of the linear program
which has constraints per nest. Problem (4) keeps only the constraints for a chosen candidate collection of assortments in each nest.
A nest is fully captured if () and partially captured if (). is the nested-by-revenue assortment. is the set of the highest-revenue products among the products of nest with the smallest preference weights, with and .
Let be an optimal solution of (4) when the candidate collection of every nest is , and let
Then is feasible for problem (3).
The theorem assumes , as all of §6 does. Otherwise it places no restriction on the or the .
Two companions follow the goal. One is the resulting guarantee , through Theorem 1. The other is the bound when the preference weights within a nest differ by at most a factor (p. 26).
Theorem 11, combined with Theorem 1 of the paper, gives a polynomial-size method for an NP-hard problem. The method solves one linear program with variables and constraints, then reads off an assortment whose expected revenue is within the factor of the optimum. This holds for every nested logit instance, including nests where customers may walk away and nests whose products are complements. When the weights inside each nest are within a factor of each other, the guarantee is at most .
The theorem is proved in the paper's appendix. No part of it is machine-checked. Formalizing it checks a case analysis that reuses, by reference, arguments from two other theorems: Theorem 7 (synergistic, fully-captured nests) and Theorem 10 (competitive, partially-captured nests). It makes precise what these arguments need when the two regimes are mixed in one instance. The formalization also fixes the boundary conventions the printed proof leaves implicit: fully-captured nests with , zero-weight denominators, and the sign of .
Each nest falls into one of three regimes, and a different argument controls each. With the nest behaves like a knapsack problem. Its guarantee of two needs the knapsack collection of §5 to sit inside . With and , the constraint must be extended from nested-by-revenue sets to every subset. This goes through a continuous relaxation whose optimum has a fractional coordinate, and it costs the ratio , which is where (12) comes from. With and , the scaling argument of Case 1 fails because multiplying by a factor at most one no longer preserves the inequality. The proof switches to the different objective (31), whose convexity in one coordinate forces an integral optimum.
The first idea, bounding every assortment by a nested-by-revenue one, is false here. With or , nested-by-revenue assortments are not optimal, and the loss is exactly the factor .
Products are Fin n; is nbr n j. Powers are Real.rpow, and , so . Problems (3) and (4) are stated in constraint form: LP4Optimal means feasible and with minimal among feasible points. is the greatest element of the finite set betaSet I, which contains and the ratios of (12). Fully-captured nests skip , as on the page. The collection is constructed: nestedPR breaks weight ties by index and revenue ties by index.
Standing assumptions, all disclosed:
A trivializing formalization is ruled out. The goal states only feasibility for (3), with the maximum of (12), not any upper bound. The collection is the page's, not an arbitrary family containing it. The goal mentions none of the cases or the relaxations.
A complete development needs continuous knapsack solutions (greedy optimality, fractional prefixes), convexity of on , and the factor-two argument of Theorem 10. The knapsack and fractional-prefix lemmas are reusable for the companion missions of this series. Proofs of individual cases, and proofs of milestones in greater generality, are welcome.
A processing network must decide which activities receive scarce processor capacity while jobs move among buffers. Such decisions matter in manufacturing, service systems, and switches: one activity can consume several processors at once, and a job can be routed to another buffer after processing. A policy that sees current buffer levels but does not need to know arrival or routing rates is easier to operate when those rates are difficult to estimate. Dai and Lin's 2005 paper studies whether a maximum pressure policy, which uses the buffer vector and an input-output matrix, can stabilize every network that is stabilizable in their model. Their Theorems 1 and 2 give, respectively, a necessary planning condition for any stabilizing policy and a sufficient condition for maximum pressure under the extreme-allocation-available assumption. Dai and Lin (2005)
Here pathwise stability means that each internal buffer grows sublinearly in time almost surely. This is a rate statement about sample paths. It does not assert positive recurrence of a Markov chain, nor does it require a stationary distribution. The paper allows general primitive processing and routing processes with almost-sure long-run averages. Dai and Lin (2005), §§2–4
There are internal buffers, activities, and processors. Buffer represents the outside world. The matrix records resource use: when activity requires processor . The matrix records which buffers an activity processes. An input activity processes Buffer ; a service activity does not. Input processors serve only input activities and must be fully used, while all processors have at most unit capacity.
For activity , the processing requirements have mean and the routing counts have long-run matrix . Write . The input-output matrix is
Positive means activity consumes net material from internal buffer ; negative means it produces net material there. An allocation assigns nonnegative activity levels subject to the processor capacity bounds and the equality for every input processor. The finite set consists of the extreme points of this allocation set. At buffer vector , allocation has network pressure . The maximum pressure rule chooses an allocation of greatest pressure among the currently feasible members of . Feasibility depends on jobs actually available to each constituent buffer. Dai and Lin (2005), §§2–3
The extreme-allocation-available assumption (EAA) says that for every nonnegative , a pressure maximizer in can be chosen whose constituent buffers all have positive levels. It links the static pressure maximization to the jobs that a policy can process. The static planning LP asks for activity fractions and a service-processor load such that , every input processor has load one, and every service processor has load at most . Dai and Lin (2005), p. 202
The goal is Theorem 2. For a network satisfying EAA and run by a preemptive, processor-splitting maximum pressure policy, LP feasibility with implies
The milestones follow the paper's route from stochastic paths to deterministic fluid limits. A fluid limit is a uniform-on-compact limit of along positive scales . The milestones state that fluid limits satisfy (14)–(18), weak stability of the corresponding fluid model transfers to pathwise stability (Theorem 3), maximum pressure adds (52)–(55) and (20) (Lemmas 5 and 4), quadratic fluid energy obeys (22)–(23), and LP feasibility with EAA makes the maximum-pressure fluid model weakly stable (Theorem 4). Dai and Lin (2005), pp. 203, 213–214
Theorem 2 identifies a policy whose almost-sure buffer growth rate vanishes whenever the planning LP permits load at most one and EAA holds. Together with the paper's necessary condition in Theorem 1, it characterizes the feasibility boundary for this policy class under EAA. Its scope includes networks in which an activity uses multiple processors and processes multiple buffers simultaneously. It does not claim that all such networks satisfy EAA. Dai and Lin (2005), Theorems 1–2
The result is proved in the 2005 article. This mission asks for a machine-checked proof of that known theorem and its selected intermediate claims. The Lean statements are open draft targets. Reusable outcomes include a model of cumulative routing and service counts, a uniform-on-compact fluid-limit interface, and the weak-fluid-stability transfer theorem for networks without a Markov assumption.
Maximizing pressure over the static allocation polytope does not by itself describe an executable service policy. An allocation can demand work from an empty buffer. EAA addresses the existence of a maximizing allocation supported by positive buffer levels, but the stochastic policy acts on actual jobs and completion times. The proof must connect those discrete, pathwise decisions to the limiting differential equation (20). At a regular fluid time, the maximum-pressure equation is decisive; away from regular times, derivatives need not exist. The fluid model therefore carries a time qualifier that cannot simply be dropped. Dai and Lin (2005), pp. 201–203, 214
The Lean model uses finite index types for buffers, activities, and processors. Internal buffers are Fin I; Buffer 0 is the zero index of Fin (I+1), and an internal buffer maps to its successor index. Activity and processor labels use zero-based Fin. Time is real but all network equations are asserted for nonnegative time. The shared Bell–Williams Paths definition supplies the renewal count in and uniform-on-compact distance using the norm. The completion count is required finite wherever the network equations convert it to a natural number; this prevents infinity from becoming a zero count. Bell and Williams (2001)
The network standing assumptions record binary incidence matrices, nonempty constituencies, processor coverage, activity types, and an input activity. Two refinements are explicit: each input processor has an activity, so its mandatory unit allocation is feasible, and , so is defined as the intended positive rate. Routing counts are cumulative and nonnegative. Their row sums are constrained only for buffers an activity processes: the printed sentence requiring the same sum for every buffer conflicts with its immediately preceding statement that the count vanishes when the activity does not process that buffer. The corresponding rows of sum to one for processed buffers and vanish for unprocessed buffers, as follows from (4). Dai and Lin (2005), pp. 199–200
The policy predicate records allocation-time decomposition (49)–(51) and the non-employment consequence of Definition 1 used in (56)–(58). It checks feasibility of a competing extreme allocation through the paper's threshold at every time of the interval. Individual job states and tie breaking are outside the pathwise interface. The goal retains EAA, the exact bound, and all network and policy equations, so an empty allocation set or an unconstrained service path cannot make the target automatic. Contributions formalizing the finite extreme-point set, fluid-limit compactness, Lemmas 4–5, and the weak-stability transfer are welcome.
Infinite-horizon dynamic programs, including discounted Markov decision processes, stochastic games and semi-Markov models, are usually analysed through a single equation: the optimal return solves the optimality equation , where maximizes the one-step return over decisions. Denardo's 1967 paper (SIAM Review 9(2), 165–177) separated the argument from the particular model. It isolated two properties of an abstract return , contraction and monotonicity, and showed that the standard conclusions follow from them alone. The examples of §8 of the paper cover Howard's discounted model, Shapley's stochastic games and Blackwell's, Jewell's and Fox's models.
The plain contraction assumption (each one-step operator shrinks distances by a factor ) fails in models where the process stops only from a subset of states, or where discounting acts only after several transitions. §5 of the paper handles these with the N-stage contraction assumption: only steps of a policy need to contract, while one step only needs to be nonexpansive. This mission formalizes that section. Its companion mission (part 1 of the series) formalizes the plain contraction case.
Timeline:
Let be a set of points. Each point has a decision set . A policy picks a decision at every point, so the policy space is . Let be the bounded real functions on with the metric ; is complete. Write when for every .
The return assigns a real number to each point , decision and . It defines two kinds of operators on :
and both are assumed to map into . An operator on has modulus or less when for all .
Under these assumptions is a contraction, so it has a unique fixed point , the return function of . The optimal return is . The auxiliary operator is .
Under the monotonicity and N-stage contraction assumptions:
The mission also contains two consequences that are not milestones: is optimal for the mathematical programs s.t. and s.t. (§6, p. 171), and a policy is optimal exactly when it attains at every point (§7, p. 173).
Theorem 4 lets models whose one-step operators are not contractions use the contraction-mapping theory of dynamic programming. Under its hypotheses the optimality equation has exactly one bounded solution, and that solution is the optimal return. Successive approximation converges geometrically from below (part (e)). Lemma 2 shows that is the least with and the greatest with . This gives the linear-programming formulation of finite Markov decision processes (Program I) and the policy-improvement argument of §6. The characterization reduces the search for optimal policies to the decisions that attain the maximum in the optimality equation.
The results are proved in the paper. The work of this mission is to formalize them, in the abstract form that Mathlib does not have: monotone operators on bounded functions that are contractive only after steps, with suprema taken over arbitrary, possibly infinite, decision and policy sets. No machine-checked proof of Theorem 4 or of Lemma 2 is known. The closest formal statements, Propositions 4.1–4.2 of Bertsekas and Shreve under their Assumption C, concern a different model (extended-real costs, nonstationary policies) and are themselves unproved formally.
The obvious argument would apply the Banach fixed-point theorem to . That does not work: under the N-stage assumption, need not be a contraction. The paper gives an example (p. 170) with , , where has modulus for every . The supremum over decisions does not commute with composition, so the contraction of each says nothing directly about . The paper therefore works through the auxiliary operator , which is a contraction. The hard step is to show that , the supremum of the policy returns, is a fixed point of . This is the second half of Lemma 2(a), an -argument that uses both monotonicity and the modulus- bound on .
Part (e) holds only for . It is not a contraction property of on all of .
lp (fun _ : Ω => ℝ) ⊤ (as BFun Ω), and its dist is . The order is pointwise (PLe).IsPolicyOperator, IsMaxOperator and IsNStageSupOperator. Every supremum, including (IsOptimalReturn), is a genuine least upper bound (IsLUB). sSup/⨆ are never used, so no junk value can make a statement trivial.ModulusLE B c. NStageContractionAssumption H N c holds , , ModulusLE (H δ)^[N] c and ModulusLE (H δ) 1, with and independent of .v with , the paper's §5 definition. is the conclusion (a), never a hypothesis.IsNStageSupOperator H N E. The milestone Theorem 4 (a)–(c) proves that such an operator exists. is never defined as a fixed point of or . The goal asserts that the pointwise least upper bound of exists in and is the unique fixed point of both.A complete development needs the Banach fixed-point theorem for iterates (Mathlib's ContractingWith, applied to ), suprema of families of real numbers, and induction on iterates. The §3 observation and Lemma 1 are reusable for any monotone operator family on bounded functions. Contributions to every milestone and to the two §6–§7 consequences are welcome.
A stochastic processing network (Harrison 2000) models a system in which processors carry out activities and each activity draws jobs from one or more buffers. Manufacturing lines, call centers with cross-trained agents, and data switches all fit this model. A central question is which scheduling policies are throughput optimal, meaning they stabilize the network whenever any policy can.
Dai and Lin (Oper. Res. 53(2), 2005) show that maximum pressure policies are throughput optimal. These policies generalize the back-pressure rule of Tassiulas and Ephremides (1992) for wireless and switch networks, and at each moment they choose the allocation that maximizes a linear "network pressure". Their main theorem (Theorem 2) has one structural hypothesis, the extreme-allocation-available (EAA) assumption (Assumption 1). It holds for many familiar networks and fails for some (§6.2 gives a counterexample). Theorem 6 identifies a broad class where it always holds: strict Leontief networks, in the sense of Bramson and Williams (2003). This mission formalizes that theorem.
A network has internal buffers , an outside Buffer , activities and processors .
The input-output matrix is
An allocation gives the level at which each activity runs. The allocation set consists of the allocations with for every processor and for every input processor. Write for the set of its extreme points, the extreme allocations. For a buffer-level vector the network pressure is . Buffer is a constituent buffer of if .
Assumption 1 (EAA). For every there is with such that for every constituent buffer of .
A network is strict Leontief if every service activity has exactly one buffer in its constituency, denoted .
The result. Theorem 2 of the paper states that, under EAA, a maximum pressure policy is pathwise stable whenever the static planning problem has a feasible solution with . Theorem 6 removes the EAA hypothesis for strict Leontief networks. In that class maximum pressure is therefore throughput optimal with no further structural condition. The class includes multiclass queueing networks with alternate routes and networks of input-queued data switches (§9), so Theorem 6 is the step that turns the abstract main theorem into a statement about these concrete systems.
Formalizing it. The theorem is proved in the paper and, to our knowledge, has no machine-checked proof. Formalizing it fixes the exact standing assumptions of the model, several of which the paper uses without stating (see below). It also yields a reusable Lean vocabulary for stochastic processing networks with input activities: from (5), the allocation polytope with the input-processor equality (2), extreme allocations, network pressure and EAA. The companion missions of this series on maximum pressure policies build on the same vocabulary.
The naive argument stops at "take a maximizing extreme allocation". A maximizer may run a service activity whose buffer is empty, in which case EAA fails at . Removing such activities gives , which has the right support and pressure but is in general not extreme. The pressure inequality depends on the sign pattern of , which holds only because every service activity has a single buffer. In the network of §6.2 this sign pattern fails and so does EAA. Returning from to an extreme allocation without losing the support property needs a convex-geometry argument about the polytope . In Lean this means relating Set.extremePoints of a compact polyhedron to maximizers of a linear functional and to supports.
Indexing. Internal buffers are Fin I. Buffers including Buffer 0 are Fin (I+1), with Buffer as 0 and internal buffer as i.succ. Activities and processors are 0-based.
Standing assumptions (§2), one predicate Network.Standing.
Disclosed additions to the page.
Conventions.
Set.extremePoints ℝ 𝒜.sSup. Without attainment the statement would be vacuous.Trivializing formalizations ruled out. EAA must not be weakened to a supremum over a possibly empty , and Buffer must not be counted as a constituent buffer. Either change would make the goal trivially true or impossible.
Infrastructure. Solvers need two results:
IsCompact.extremePoints_nonempty and Krein–Milman;Both are reusable beyond this mission. Contributions proving them as general Mathlib-style lemmas are welcome.
A seller with replenishable inventory must decide how much to order and what price to charge before demand is known. A price that increases current revenue can also change the inventory left for later periods; a fixed charge for placing any positive order adds a discontinuity to the decision. Chen and Simchi-Levi study this coordination problem over a finite horizon with backlogging and random, price-dependent demand. Their general-demand result characterizes an optimal order-and-price policy even when a conventional two-threshold ordering rule can fail. The paper gives explicit counterexamples to ordinary -concavity and to optimality of a standard policy in this setting (Chen and Simchi-Levi, 2004, §4, Lemmas 3–4).
There are periods . At the start of period , the firm has inventory , which may be negative because unmet demand is backlogged. It may order to any level . If , it pays a fixed ordering cost as well as a variable cost . After ordering it chooses an expected demand level in a closed interval . The corresponding price is , the inverse of the period's decreasing demand curve, and expected revenue is .
Actual demand is . The random pair has a period-dependent law , with and . No sign restriction is placed on in the paper's general model. The inventory after demand is , incurring a convex holding or backlog cost and entering the next period. The paper assumes the random perturbations are independent across periods. Its Bellman equation uses their individual period laws (Chen and Simchi-Levi, 2004, §2, Assumptions 1–5).
The profit-to-go starts with . For a post-order inventory and expected demand , write
The firm maximizes over admissible and then maximizes the resulting value, less the fixed ordering charge, over . This defines by equation (2) of the paper. A symmetrically -convex real function satisfies
for every and . A function is symmetrically -concave when its negative is symmetrically -convex. This is Definition 4.1, equation (8), and preserves the symmetry between the two endpoint inventories (Chen and Simchi-Levi, 2004, p. 891).
The goal is Theorem 4.1(c)–(d). If , then for every period
There are thresholds and a possibly empty set . An optimal policy orders to if or , and places no order otherwise. It chooses the maximizing expected demand for the resulting post-order level. In particular, all states that order to can use the same demand level and hence the same price .
The milestones state the preceding polynomial growth and continuity assertions from Theorem 4.1(a)–(b), the threshold structure of Lemma 5(d), and the named steps in the proof on p. 892. The link from the paper's earlier -convexity to symmetric -convexity is also included. These targets preserve the paper's general demand law rather than restricting it to the additive case.
The theorem describes an optimal decision at every inventory level under random price-dependent demand. The exceptional set records states where ordering to is optimal inside the interval where a single reorder threshold need not describe all optimal actions. Thus the result retains a concise policy description while allowing the behavior exhibited by the paper's counterexamples (Chen and Simchi-Levi, 2004, §4).
Formalizing the result requires a reusable account of symmetric -convexity, a fixed-cost ordering envelope, and a finite-horizon Bellman recursion with real-valued expectations. The source proves Theorem 4.1 on paper. This mission poses its statements as Lean goals; the theorem files currently contain sorry and therefore are not machine-checked proofs. The published platform definition BertsekasKConvex supplies the earlier notion from Definition 2.1, so the bridge to Definition 4.1 can be stated without duplicating it.
In the additive-demand case, a maximizing expected-demand choice can be selected so that post-demand inventory changes monotonically with the initial inventory. For general demand , that monotonicity can fail: the random multiplier changes how a pricing choice moves the next inventory state. The earlier ordered-chord -concavity argument therefore does not carry over unchanged. A second issue is the fixed ordering charge. It creates ties between ordering and not ordering, so the policy region can include isolated or noninterval states within . The statement must assert Bellman optimality at every , including those ties, rather than only the geometry of (Chen and Simchi-Levi, 2004, pp. 891–892).
The Lean model uses expected demand as the decision variable and obtains price from , matching the paper's reformulation after Assumption 5. The admissible demand interval is nonempty. Periods are natural numbers , with and terminal value . Random demand is integrated against a probability measure on . The first moments and the paper's demand moment condition are explicit; holding-cost and continuation integrability prevent a nonintegrable real integral from acquiring Lean's default zero value. The paper's statements are encoded by constants multiplying .
The formal assumptions include and , and set where the paper's Assumption 3 uses that otherwise undefined terminal coefficient. The latter two restrictions make the printed finite-horizon claim valid under its cost interpretation; they are stated rather than silently supplied. The paper assumes temporal independence, while the formal Bellman recursion starts from the marginal laws and so needs no separate joint process. The paper's in Theorem 4.1(b) is expressed as through the continuous one-to-one price–expected-demand correspondence. The model places no positivity condition on .
The optimized demand value and ordering value are real suprema. The statements include maximizing choices and Bellman attainment; a proof cannot rely on a default value for an empty or unbounded supremum. The goal requires an actual optimal action for every inventory state. Contributions that establish integrability, continuity, coercivity, symmetric convexity preservation, or the ordering-envelope structure are useful beyond this mission.
The simplex method solves linear programs quickly in practice, yet for most pivot rules there are inputs on which it takes exponentially many steps (Klee and Minty, 1972). Smoothed analysis, introduced by Spielman and Teng (JACM 2004), explains the gap: it measures the expected running time when every constraint row of a worst-case input is perturbed by a small random amount of size . For the shadow vertex pivot rule, the running time is controlled by a purely geometric quantity, the number of edges of a random polygon, and the smoothed complexity of the method is essentially an upper bound on that number.
Timeline (bounds on the expected shadow size of smoothed unit LPs, as surveyed in §1.1 of the paper). Borgwardt (1987) proved for rows drawn from a centered Gaussian, asymptotically as ; this is the case of the model below. Spielman and Teng (2004) gave the first smoothed bound, . Deshpande and Spielman (FOCS 2005) improved the dependence on to . Vershynin (SIAM J. Comput. 2009) reduced the dependence on to polylogarithmic, . Dadush and Huiberts (arXiv:1711.05667, STOC 2018, SIAM J. Comput. 2020) proved for Gaussian perturbations by a simpler argument, which also gives bounds for Laplace perturbations.
Fix dimensions and a shadow plane, a two-dimensional linear subspace , chosen independently of the randomness. The constraint vectors are independent, and is Gaussian with center , , and standard deviation in every coordinate, i.e. with density .
Let . The shadow polygon is . An edge of a convex set is a segment , , which is an extreme subset of ; is the number of edges. The number of pivots of the shadow vertex method on the unit LP between two objectives spanning is at most (the paper's Lemma 11 and Theorem 12).
The proof passes through general row distributions with density and mean , described by four parameters: the log-Lipschitz constant (); the line variance (the least variance of restricted to a line); the -th deviation (the least with for all unit ); and the cutoff radius (the least with ). The Gaussian is not log-Lipschitz; the Laplace–Gaussian distribution , whose density equals the Gaussian one inside the ball of radius around and decays like outside, replaces it.
The paper states ; the constant above is the one its proof produces (Theorem 22's proof, Lemma 45, Lemma 46).
The bound gives the best known smoothed complexity of a simplex method, with only dependence on the number of constraints. Section 4 of the paper turns it into a complete two-phase shadow vertex algorithm with expected pivots. The parametrized Theorem 22 applies to any perturbation family with bounded parameters, so it also yields shadow bounds for Laplace and other noise models.
The result is proved; it has not been machine-checked. A formalization adds a verified chain from four distributional parameters to a polygon edge count. The intermediate statements have independent value: an expected-perimeter bound for random polygons, the deterministic chord-length identity for simplices, and tail estimates for the Laplace–Gaussian distribution.
The expected number of edges is a sum, over all index sets, of the probability that their simplex meets in an edge; there are far too many terms for per-set estimates to give a bound polylogarithmic in . The paper's route (inspired by Kelner and Spielman) instead compares the expected perimeter with the expected length of an edge, and the hard part is a lower bound on the expected length of an edge conditioned on it appearing. That conditioning is on a probability-zero configuration (the simplex lying in a fixed hyperplane), and its analysis needs Blaschke's change of variables, the shape decomposition of the simplex, and log-Lipschitz shifts of densities. On the Gaussian side, the density is not log-Lipschitz, which forces the Laplace–Gaussian detour and a comparison of edge counts under two different laws.
is EuclideanSpace ℝ (Fin d), is Fin n, is the natural logarithm. The Gaussian is the published SmoothedSimplex.Shadow.gaussian, the edge relation is the published Hirsch.Adj, and the rows' joint law is Measure.pi. Edges are segments counted once; the perimeter is the sum of edge lengths. Expectations are lower Lebesgue integrals in , and every edge-count bound also asserts almost-everywhere measurability of the count, so the integral is a genuine expectation. Conditional expectations are stated multiplied out (no division by a probability), and the parameters of Definitions 15–18 are upper-bound predicates (lower bound for the line variance), which is how every statement of the paper uses them.
Hypotheses added relative to the page, each implicit there: ; and in Theorem 22; positivity of log-Lipschitz densities; the standing of §3 in Lemma 44. Lemmas 39 and 41 are stated on the explicit conditional densities that the paper derives in Lemma 37, instead of through regular conditional distributions; Lemma 39 takes the conclusion of Lemma 21 as a hypothesis, as its proof uses it. Two printed slips are corrected: Lemma 46's formula is stated for , as its sentence and proof have it, and Lemma 35 refers to Definition 33 (not 34).
The goal mentions only Gaussian rows, , and the edge count of . It cannot be trivialized by an unsatisfiable parameter hypothesis or a bound on edge lengths, since it has neither; and it counts edges of the polygon, not of the polytope .
A complete development needs: Gaussian and Laplace–Gaussian tail bounds; measurability of the edge count of a random polygon; the perimeter monotonicity of convex sets; Blaschke's change of variables (Theorem 7 of the paper, quoted from Blaschke 1935), which Mathlib does not have; and the regular conditioning of Lemmas 32, 37 and 38. The Blaschke formula, the perimeter facts for convex polygons, and the tail bounds are reusable well beyond this mission. Contributions to any milestone, or to these supporting results as separate theorems, are welcome.
Many design problems in control, finance and engineering are convex programs whose constraints depend on an uncertain parameter : a solution must satisfy for every in a possibly infinite set . Enforcing all constraints (robust optimization) is often intractable or overly conservative. The scenario approach draws independent samples of , solves the convex program with those constraints only, and asks how likely it is that the resulting solution violates a fresh constraint. The question matters wherever a randomized design is certified by a confidence statement, from robust control to chance-constrained portfolio selection.
Timeline.
Let be a probability space, with , and let and () be convex closed sets. The violation probability of a point is
For a multi-extraction , the program minimises over . It is assumed that every has a unique solution . A constraint is a support constraint of if its removal changes the solution. A convex has at most support constraints (Proposition 2.2). The problem is fully-supported if, for every , the program built from independent samples has exactly support constraints with -probability one.
Two further objects carry the argument. For of cardinality , is the set of multi-extractions whose support constraints have exactly the indexes in . The violation law is
the distribution of the violation of the solution built from samples.
For a fully-supported problem, every and every ,
The result. Equation (2.3) shows that the scenario bound (2.2) is tight: no bound that depends only on , and can be smaller, because a fully-supported problem attains it. The distribution of is then a Beta law, being the probability that a variable is at least , the same for every fully-supported problem. This is what fixes the sample sizes used in practice: is chosen so that the binomial tail is below a confidence level . Fact (3.2), that has distribution function whatever the problem, is a distribution-free statement of independent interest.
Formalizing it. The result is proved in the source. As far as is known it has no machine-checked proof. The goal statement is already posed on the platform, and this mission supplies the paper's proof structure as milestones. Two milestones are reusable outside the scenario approach: the uniqueness of a distribution on given the moments , and the incomplete-beta identity for binomial tails.
The obvious route would compute the law of directly, but it depends on the geometry of the constraints. The paper never computes it. It obtains the law of only implicitly, through the infinite family of identities (3.4), and recovers it by a uniqueness theorem for moment problems. Two points need care. First, full support holds only almost surely: duplicated samples, for instance, produce programs with fewer than support constraints, so every set identity holds only up to null sets. Second, the claim that removing a non-support constraint keeps the first constraints as the only support constraints uses Proposition 2.2. Two identical non-support constraints show that a constraint can become a support constraint after another is removed, unless the count is bounded by .
Goal. The goal is the already-posed platform statement ScenarioApproach.Generalization.violation_tail_eq_binomial_sum_of_fullySupported (theorem id cffaa932-832c-42ca-9e81-1848ffab7e34), referenced as it stands and not restated. Proposition 2.2 is the platform statement card_support_constraints_le_dim (f70e8aa3-…). This mission adds the PART 1 steps as milestones under ScenarioExact.PartOne.
Representation. Decisions are vectors in EuclideanSpace ℝ (Fin d). A multi-extraction is ω : Fin m → Δ, with 0-based indexes, so is and "" are the indexes . is Measure.pi (fun _ : Fin m => P). , the feasible set, solutions, support constraints and full support are the published definitions violation, feasibleSet, IsSolution, IsSupportConstraint and FullySupported. A support constraint is one whose removal admits a feasible point of strictly smaller cost, which under uniqueness is the paper's "its removal changes the solution". Full support is almost sure, not pointwise.
Hypotheses made explicit. Assumption 1 is entered as existence and uniqueness of the solution for every number of constraints and every sample, together with a family of solution maps θs k, each assumed to solve and to be measurable. Under uniqueness, θs N is the goal's solution map. The paper's "measurability ... is assumed for granted" (p. 4) is replaced by joint measurability of and measurability of the solution maps, the same two hypotheses as the goal. No set is assumed measurable. The nonempty-interior clause of Assumption 1 is unused in PART 1 and is not assumed, so the milestones compose with the goal.
Conventions. is the push-forward measure violationLaw on , with = violationLaw … (Set.Iic α). Integrals against are lower Lebesgue integrals of nonnegative integrands, as extended nonnegative reals: over for , and over for in the partition chain, since that integral comes from the event . The integration-by-parts identity is a real interval integral. Ranges are , , and .
Ruled out. A pointwise "exactly support constraints for every sample" would be unsatisfiable for many problems (repeated samples) and would trivialise the probabilistic content, so it is not used. Assuming measurability of the event or of , or the identity , as a hypothesis would assume part of the conclusion, so none of these is a hypothesis.
Infrastructure. A complete development needs: the support-constraint count (Proposition 2.2, a Helly-type argument), invariance of product measures under coordinate permutations, the change-of-variables formula for push-forward measures, the Hausdorff moment uniqueness theorem on , and the binomial–incomplete-beta identity. The last two are general results, and contributions of them are welcome independently.
MAXCUT asks for a partition of the vertices of a weighted graph into two sets that maximizes the total weight of the edges between them. It is one of Karp's original NP-hard problems, so no polynomial-time exact algorithm is expected, and the natural question is how close a polynomial-time algorithm can come to the optimum. Sampling a uniformly random partition already achieves, in expectation, half of the optimal value. For two decades this factor was essentially the best known.
Goemans and Williamson (J. ACM 42(6), 1995) replaced the combinatorial problem by a semidefinite relaxation, solvable in polynomial time by interior point methods, and rounded its solution with a random Gaussian hyperplane. They proved that the resulting cut has expected weight at least times the maximum. The technique founded the use of semidefinite programming in approximation algorithms. Khot, Kindler, Mossel and O'Donnell (SIAM J. Comput. 37(1), 2007) showed that, assuming the Unique Games Conjecture, no polynomial-time algorithm achieves a better constant. Nesterov (Optim. Methods Softw. 9, 1998) extended the rounding analysis to maximizing any positive semidefinite quadratic form over the hypercube, with the constant .
This mission formalizes the presentation of these results in §6.6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (arXiv:1405.4980v2), pp. 343–347.
Let and let be a symmetric matrix with non-negative entries; is the weight between points and . The graph Laplacian is , where is the diagonal matrix with entries . For the vector encodes a partition, and MAXCUT is (6.7)
Write for the Frobenius inner product and for the symmetric positive semidefinite matrices. Since and has unit diagonal, MAXCUT is bounded above by the SDP relaxation
A solution of the relaxation is any feasible matrix attaining this maximum. The rounding draws , a centered Gaussian vector with covariance , and outputs coordinatewise.
For symmetric with non-negative entries, , any solution of the relaxation, and :
The separately stated Laplacian identity on p. 346 is also included as a theorem item: if for all , then ; for , .
For , a solution of , and :
The result. Theorem 6.11 is a polynomial-time randomized -approximation for MAXCUT: the relaxation is a semidefinite program, and sampling a Gaussian vector and taking signs is cheap. Repeated sampling turns the bound in expectation into a cut of value close to times the optimum with high probability. The same scheme of relaxation followed by randomized rounding underlies approximation algorithms for MAX-2SAT, correlation clustering and quadratic programs over the hypercube, and Nesterov's Theorem 6.13 is the version for an arbitrary positive semidefinite objective.
Formalizing it. Both theorems were proved long ago. To our knowledge neither has a machine-checked proof in Mathlib. The platform has related statements from other books, in different forms: Grothendieck's identity for a standard Gaussian and two unit vectors, and the relaxation guarantee with a Grothendieck constant. This mission states the textbook's results for a Gaussian with a possibly singular covariance matrix, which is the form the rounding uses. A complete development needs Sheppard's formula for a degenerate bivariate Gaussian, an elementary but careful real-variable inequality, and a link between Mathlib's multivariate Gaussian and Gram factorizations of . All three are reusable.
The algebra (the Laplacian identity and milestone 4) is routine. The probabilistic core is Lemma 6.12. The textbook argument reduces it to the probability that a uniformly random direction separates two unit vectors, which is "a quick picture" on paper. In Lean this requires showing that the pair has the law of for a standard Gaussian , and then computing an angular measure in the plane, including the degenerate cases , where the pair is supported on a line. A density-based argument fails there, because has no density when is singular, and singular solutions of the relaxation occur (for instance ). Inequality (6.8) is a statement about a transcendental function on a closed interval with a tight constant ( against the true minimum ), so crude estimates do not suffice near the minimizer .
Matrix (Fin n) (Fin n) ℝ, vectors Fin n → ℝ. is Matrix.PosSemidef, which includes symmetry, and is trace (Mᵀ * X).ProbabilityTheory.multivariateGaussian 0 Σ on EuclideanSpace ℝ (Fin n), defined for every positive semidefinite , singular ones included. Expectations are Bochner integrals against it, and each theorem also asserts integrability of its (bounded) integrand.Real.sign would give , which takes out of ; the two agree almost surely because .Finset.sup') over the Boolean vectors read as vectors, so it is never a junk value. "The solution" of the relaxation means any maximizer, and maximizers exist since the feasible set is compact and contains the identity.When a problem has millions of variables, even one full gradient can be too expensive to compute, while a single partial derivative is often cheap: in regularized regression, support vector machines and many structured problems, updating one coordinate costs a small fraction of a full gradient step. Coordinate descent methods exploit this by moving along one coordinate at a time. They are among the oldest optimization schemes and were for a long time analysed only for cyclic orders and only asymptotically.
Nesterov (2012) showed that choosing the coordinate at random, with probabilities depending on the coordinate-wise smoothness constants, gives global, non-asymptotic rates that can beat full gradient descent in total work. This mission formalizes that analysis as presented in §6.4 of S. Bubeck, Convex Optimization: Algorithms and Complexity (arXiv:1405.4980v2), pp. 338–342, and in particular its linear rate for strongly convex functions (Theorem 6.8).
Let be differentiable, write and let be the -th standard basis vector. The function is directionally smooth with constants if
equivalently, each one-variable restriction is -smooth.
For a real exponent , the weighted norms are
For , is -strongly convex w.r.t. a norm if for all . The point is a minimizer of .
For , RCD() starts at and iterates
where are drawn independently from . The case is uniform sampling; samples proportionally to .
Let , let be -strongly convex w.r.t. and directionally smooth with constants , and let . Then for every
For convex and directionally smooth, and ,
Theorem 6.8 says random coordinate descent converges linearly, with a rate governed by instead of the global smoothness constant. For , directional smoothness implies is -smooth with , so for functions whose global smoothness constant is of the order of , RCD(1) attains the accuracy of gradient descent after the same number of iterations (book, p. 340, comparing Theorem 6.7 with Theorem 3.3), while each iteration touches a single coordinate. The same per-step inequalities underlie later accelerated and parallel coordinate methods.
These results are proved in the literature (Nesterov 2012; Bubeck 2015). Their contribution here is a machine-checked version. As far as a search of the Prove2Me catalogue shows, no coordinate descent rate of this kind has been formalized there; a Euclidean-norm special case of Lemma 6.9 exists on the platform as a separate result, but not the arbitrary-norm lemma or the weighted-norm instance used here.
The main obstacle is bookkeeping of the randomness: the per-step inequality holds for each fixed iterate, while the theorem is about the expectation over the whole sequence of draws , so the pointwise contraction has to be passed through the tower of conditional expectations. In the strongly convex case this is linear and exact; for Theorem 6.7 the recursion on is quadratic, and since is an expectation while the gradient norm at is random, the pointwise inequality does not transfer to verbatim. A second point is geometric: strong convexity, the dual norm and the sampling distribution must use matching weights ( against ), and a mismatch silently changes the constant.
EuclideanSpace ℝ (Fin n). The gradient is an explicit map with HasGradientAt f (g x) x, so . Lemma 6.9 is stated for a finite-dimensional real normed space with the Fréchet derivative and the operator norm as the dual norm.A complete development needs the one-dimensional descent lemma (3.5), weighted Cauchy–Schwarz for the dual pair , and a decomposition of the finite expectation over into the last draw and the first . The weighted-norm and finite-expectation lemmas are reusable for other randomized coordinate and sampling methods. Proofs of the milestones and of either theorem are welcome.
Many optimization problems in machine learning minimize an average of losses, one loss for each observation. A full gradient step examines every observation, while a stochastic gradient step examines one. The latter is cheaper per step, but its sampled gradient can remain noisy even near the optimum. Section 6.3 of Bubeck's monograph studies stochastic variance reduced gradient descent (SVRG), which periodically computes a full gradient at an anchor point and uses it to correct subsequent sampled gradients. The question for this mission is whether that correction gives a geometric reduction of the expected objective gap at the constants printed in Theorem 6.5.
Bubeck places this method alongside full gradient descent and stochastic gradient descent for finite sums. The section records that earlier stochastic average gradient and dual coordinate ascent methods attain a gradient-computation cost of order for the same regime, where is the number of components and is a condition number. The target here is the precise SVRG convergence statement in the book, rather than a comparison of implementation costs. The source's discussion on pp. 334–336 gives the context and the algorithm.
Let be differentiable convex functions, with , and define the finite-sum objective and its gradient by
Each component is -smooth when its gradient is -Lipschitz in the Euclidean norm: for all . The average is -strongly convex, meaning that for all it lies at least above its first-order affine approximation at . The constants and are positive, minimizes over , and .
An epoch begins at an anchor . Its first inner iterate is . For , draw uniformly from , independently across steps and epochs, and update
The next anchor is the average . In particular, this average uses through , while the last updated point is excluded. Starting from an arbitrary and repeating the epoch produces . The expectation of is over all sampled indices in the first epochs.
Theorem 6.5 sets and and asserts, for every ,
The epoch length is a count, so the statement takes and explicitly requires . The goal uses exactly the book's step size, epoch length, and contraction factor.
Lemma 6.4 bounds by . Equation (6.3) bounds the second moment of the corrected sampled direction by the objective gaps at the current point and the anchor. Equation (6.2), the unbiased-direction display, and the one-step display express how that direction changes squared distance to . The later display on p. 338 bounds one epoch for any positive step size with . Finally, equation (6.1) substitutes the stated constants to obtain the factor for one epoch. These seven source claims form the milestone list in reading order.
The theorem gives an explicit accuracy guarantee after a specified number of epochs: an initial gap falls below in expectation. Because each epoch uses a full gradient at its anchor as well as sampled component gradients, the result makes clear which quantity contracts and which operations are counted. It is a concrete linear-rate statement for a method whose individual stochastic gradients need not approach zero at the optimum. Bubeck, §6.3 discusses this issue when introducing the correction term.
The mathematical result is already proved in the monograph. The remaining task is to produce machine-checked proofs of its precise finite-sum model, the single-index estimates, the epoch inequality, and the full repeated-epoch guarantee. The mission drafts those statements and definitions; no proof is claimed for the open theorem items. The finite uniform-average representation and the separation between a conditional one-step average and the full multi-epoch average can be reused in other finite-sum stochastic algorithms.
The sampled component gradient need not be small when is near , so a bound using only its norm does not yield the desired fixed-step contraction. The correction has mean zero relative to the full gradient at the current iterate, but its second moment still depends on both and . The proof must control those two gaps while respecting the fact that depends on earlier samples. A single-index estimate with held fixed and an expectation over complete sample histories are different statements; confusing them would make the goal weaker or false.
The carrier is EuclideanSpace ℝ (Fin n) with its usual inner product and norm. The Fin m components and every sample array are finite. A real-valued uniform average is an ordinary finite sum divided by the number of arrays, and and prevent an empty average. Independent uniform sampling is represented by averaging over every function from step positions to component indices. The multi-epoch sample space has one such block for every epoch. There are no integrals or measurability side conditions.
The component assumptions include differentiability with an explicit gradient map, convexity on all of , and the book's gradient-Lipschitz version of smoothness. Strong convexity is imposed on the average objective alone, using the published OnlineConvexOpt.ConvexBasics.StronglyConvexOn definition on the whole space. The book's standing notation assumes a minimizing exists; this is explicit. Positivity of and , and integrality of , make the displayed divisions and epoch length meaningful. The general epoch bound also requires and . Dimension zero is allowed: the theorem remains a statement about the unique point of and its zero objective gap.
The direction always contains the sampled difference and the full anchor gradient . Replacing that direction with would define gradient descent and would not satisfy this mission's algorithm. Contributions are welcome for the finite averaging identities, the component-gradient estimate, the conditional one-step calculation, the epoch inequality, and the induction across epochs.
Many optimization problems in statistics and machine learning ask to minimize an expected loss , or an average over a large data set. Exact gradients of such an are unavailable or too expensive, but unbiased random estimates are cheap: the gradient of the loss at one sample, or of one randomly chosen summand. The observation that first-order methods still make progress when the gradients are only correct on average goes back to Robbins and Monro (1951) and underlies stochastic gradient descent.
Chapter 6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (2015), studies this setting through stochastic mirror descent (S-MD). Its Section 6.1 shows that in the non-smooth case a noisy oracle costs nothing in rate. Section 6.2 asks what smoothness buys: for a general stochastic oracle it cannot buy acceleration, but Theorem 6.3, whose proof the book takes from Dekel, Gilad-Bachrach, Shamir and Xiao (2012), shows that the rate splits into a noise term of order and a smoothness term of order . The book uses it to justify mini-batch SGD. This mission is the fourteenth of a series that formalizes the section capstones of the book.
Let be a finite-dimensional real vector space with an arbitrary norm . Gradients are linear forms on , the value of at is written , and the dual norm is . Let be compact and convex.
A mirror map is a function on an open convex set with and . It is strictly convex and differentiable on , its gradient takes every value, and as approaches the boundary of . Its Bregman divergence is . The map is 1-strongly convex on if there. A function is -smooth on if for .
A stochastic oracle returns, at a query point , a random linear form . When the query point is itself random, the book requires the conditional expectation given the query point, , to be a subgradient of at . In the smooth case it requires together with the variance bound .
S-MD with step starts at and, writing , iterates
Let , and let minimize on .
Let be convex and -smooth, and let the oracle have variance at most . Then for every , S-MD with step and satisfies
For points and , the smoothness step is
If is the S-MD step, the mirror step is
Combining the two gives a pathwise bound on with the cross term . Taking expectations gives the expected one-step bound
For a convex with , S-MD with satisfies
This rests on the deterministic regret bound (4.10) of mirror descent along arbitrary vectors :
Theorem 6.3 says exactly how much smoothness helps under noise. As it recovers the rate of deterministic smooth optimization. For large the noise term dominates; the book notes, citing Tsybakov (2003), that smoothness brings no acceleration for a general stochastic oracle. Averaging independent oracle answers divides the variance by , so the theorem quantifies the benefit of mini-batches: the noise term shrinks by while the smoothness term is unchanged. Theorem 6.1 is the matching non-smooth statement and the template for stochastic subgradient methods in any norm.
These are classical, proved results. None of them is known to be formalized in Lean, and the platform has no stochastic mirror descent statement. Its stochastic gradient items cover the Euclidean strongly convex case and the non-convex gradient-norm case. This mission adds a reusable stochastic-oracle layer in an arbitrary norm, with conditional expectations given random query points, on top of the mirror-map layer of Chapter 4.
The deterministic steps are short manipulations of Bregman divergences. The difficulty is in the passage to expectations. The query point is random, so unbiasedness enters only through the conditional expectation given . Making the cross term vanish requires pulling the -measurable vector out of a conditional expectation of a dual-valued random variable. Every expectation also has to exist. When blows up at the boundary of , the Bregman terms are not bounded a priori, and their integrability has to be derived from the recursion. A further obstacle is that the minimizer may lie on the boundary of , where is not part of the book's data. Treating informally, or assuming , skips exactly these points.
Φ' f' : E → (E →L[ℝ] ℝ), is g v, and is the operator norm. -smoothness is stated with derivatives relative to . is a total function, constrained only by the mirror-map axioms on .A variance hypothesis stated only at deterministic points would not control the random iterates, and is not used. Run predicates that let be an arbitrary point of would make the theorems false, and are not used either.
A complete development needs: first-order optimality over a convex set, the three-point identity of Bregman divergences, the descent lemma in an arbitrary norm, and continuity of the gradient of a differentiable convex function. On the probability side it needs pull-out and conditional Jensen properties for dual-valued conditional expectations. The probability layer is reusable for every stochastic first-order method in the book, including SVRG and random coordinate descent. Proofs of the milestones are welcome, and so are general lemmas about conditional expectations of continuous-linear-map-valued random variables.
First-order methods for constrained convex optimization are usually analysed in the Euclidean norm, where gradient descent and its projected and accelerated variants have well-understood rates. Many constraint sets of practical interest, such as the probability simplex, the ball and the spectrahedron, are poorly adapted to the Euclidean geometry: the Euclidean diameter and the Euclidean Lipschitz or smoothness constants grow with the dimension. Mirror descent, due to Nemirovski and Yudin, replaces the Euclidean step by a step taken in the dual space through a mirror map , so that the rate depends on constants measured in a norm matched to the set. For non-smooth Lipschitz functions it attains the rate (Theorem 4.2 of the source, the subject of the previous mission of this series).
For smooth functions, a rate of order is available in any geometry by an extragradient-type modification. Mirror prox was introduced by Nemirovski in 2004 (Prox-method with rate of convergence O(1/t)) for variational inequalities with Lipschitz monotone operators and convex–concave saddle-point problems. It is the basis of smoothing approaches to non-smooth optimization and of stochastic saddle-point methods. This mission formalizes the version for minimizing a single smooth convex function, Theorem 4.4 of S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015), §4.5.
Fix an arbitrary norm on a finite-dimensional real space . Gradients are linear functionals on ; for a functional write for its value at , and for the dual norm. Let be compact and convex.
Mirror prox with step size generates, from ,
The first half is a mirror descent step from to ; the second restarts from with the gradient evaluated at .
With , , , convex and -smooth and a minimizer of on , for every
The three-point identity (4.1), , is already posed on the platform as BeckTeboulleMD.EMDA.lemma_4_1 and is included by reference.
Theorem 4.4 shows that the rate of gradient descent on smooth functions survives in non-Euclidean geometries, with the dimension entering only through . With the negative entropy on the simplex, is of order for the norm, against a polynomial dependence for Euclidean methods. Beyond this single-function version, the same three-term argument is the core of the analysis of mirror prox for monotone variational inequalities and saddle-point problems (§4.6 and §5.2 of the source), where it gives the rate for smooth convex–concave games.
The result is proved in the source and in Nemirovski's paper. As far as this mission is aware it has no machine-checked proof; Mathlib has no Bregman divergences, mirror maps or mirror-descent-type algorithms. A formal proof would supply reusable infrastructure: the Bregman projection lemma (Lemma 4.1) and the three-point identity are used by every mirror-descent analysis, including the stochastic and online variants later in the source.
The obvious argument for mirror descent bounds by and leaves a stability term of size , which yields only . Smoothness has to be used to cancel that term, and a single gradient step does not do so in a general norm. Mirror prox evaluates the gradient at the extrapolated point ; the analysis must show that the error created by using for the first step is paid for by the strong convexity of , which requires splitting into three terms and bounding each with matching constants.
In Lean the difficulty is in the infrastructure: first-order optimality of a Bregman projection over , which need not be closed; the passage from to a minimizer that may lie on the boundary of ; and Jensen's inequality for the average of the .
E →L[ℝ] ℝ given by explicit maps Φ' and f'; the dual norm is the operator norm. Φ' is the Fréchet derivative of at each point of ; f' is the derivative of relative to at each point of .Contributions welcome: proofs of Lemma 4.1 and the three-term bounds, which are reusable for the stochastic mirror descent and saddle-point missions of this series, and the final telescoping and limit argument.
Many resource-allocation problems arrive one request at a time and must be answered immediately: a bandwidth request is admitted or refused when it appears, an advertiser's budget is charged when a query arrives, a job is accepted before later jobs are seen. Their linear-programming relaxations are packing problems: maximize a total profit subject to capacity constraints, where the variables are revealed online and each must be set irrevocably when it is revealed. A standard yardstick for such an online algorithm is its competitive ratio, the worst-case ratio between the offline optimum and the algorithm's value.
Buchbinder and Naor (Math. Oper. Res. 2009) gave a single online primal-dual scheme for the general online fractional packing problem, together with a matching scheme for covering. The scheme raises the newly revealed packing variable while increasing the dual covering variables along an exponential curve, and its analysis is a short primal-dual argument. Earlier online algorithms for throughput-competitive routing and for set cover (Alon et al. 2009) can be read as instances of it, and the same template later became the basis of a monograph on the primal-dual approach to online algorithms (Buchbinder, Naor 2009).
This mission formalizes the paper's headline result, Theorem 3.1, for the scheme exactly as the paper defines it.
Fix a finite set of packing constraints (equivalently, primal covering variables), with known capacities . Packing variables arrive one per round; in round the variable is revealed together with its non-negative column , . The offline problems form the primal-dual pair of Figure 1 of the paper:
The profit of every is normalized to . Every column is assumed to have a positive entry; otherwise the packing problem is unbounded. An online algorithm may set only in round and never changes it later.
The scheme with parameter keeps a primal vector (initially ) and the dual vector . In round it computes the prefix maximum . If the new covering constraint already holds, it sets . Otherwise it sets to the least at which the constraint holds after every is replaced by
After rounds, is the primal value and the dual value. For the analysis, and also denote the largest and the smallest non-zero coefficient of row over all columns.
For every , the scheme's dual solution is non-negative; after every round , every non-negative that satisfies the packing constraints restricted to the first columns has (the scheme is -competitive); and after all rounds, for every ,
The paper states the second part as ; the bound above is the one its proof establishes.
Theorem 3.1 says that a solution within factor of the optimum can be maintained online at the price of overloading each packing constraint by a factor of order . Scaling the output down by the overload gives a feasible online packing solution with competitive ratio , and Lemma 3.1 of the paper shows that no online algorithm does better up to constant factors. The same trade-off underlies the paper's online rounding results for routing (§5.2) and, through the covering counterpart, for set cover (§5.1).
The result is proved in the paper. As far as the platform's record shows, it is not formalized: the published OnlinePrimalDual.GeneralPacking.theorem14_1 (a restatement of the monograph's version) takes the inequality and primal feasibility as hypotheses on arbitrary vectors and derives competitiveness by weak duality; it does not mention the scheme and has no violation bound. The published OnlinePrimalDual.GeneralPacking.lemma14_2 is the matching lower bound (Lemma 3.1) and is not part of this mission. A formalization here would give the first machine-checked guarantee for the scheme itself and a reusable analysis pattern (a potential bound integrated along a monotone path) for the other schemes of the paper.
The paper's argument is a derivative comparison along a continuous process: while rises, . In the discrete formulation each round jumps directly to the least admissible , and each is a maximum of its old value and an exponential, so it is continuous but not differentiable where the maximum switches; the comparison must be turned into an integral inequality over for such functions. The prefix maximum changes between rounds, and the claim that this never lowers or raises the primal value needs an invariant ( is always at least the current increment value). The violation bound rests on a second invariant, , which holds because is the least admissible value; any formalization that loses minimality (for example by taking an arbitrary admissible ) loses claim (iii).
OnlinePrimalDual.GeneralPacking.GeneralInstance I (Fin m) (costs , coefficients ); with [Nonempty I]; columns are Fin m, arrive in index order, and are 0-based in Lean, so "the first columns" is (k : ℕ) < r. is [NeZero m].aMax and aMin. For a row with no non-zero coefficient aMin is and both sides of the violation bound are .stateAfter inst B r. The continuous loop of the paper is replaced by its discrete implementation, which the paper itself prescribes (p. 4): is the least restoring the new covering constraint, written as sInf. Every theorem assumes that every column has a positive entry (the paper's standing assumption, p. 4); this makes the infimum attained. If the prefix maximum is , Lean's gives increment , which agrees with the paper's bracket being .Real.log), since they invert Real.exp.