Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A global surface of section reduces a flow on a closed 3-manifold to an area-preserving map of a surface. It is a compact embedded surface whose boundary consists of periodic orbits, whose interior is transverse to the flow, and which every other trajectory hits infinitely often in forward and backward time. Poincaré introduced the idea for the restricted three-body problem. Once a section is a disk, results on area-preserving disk maps (Brouwer, Franks) give periodic orbits and other structure for the whole flow.
For Hamiltonian flows on star-shaped energy surfaces in , equivalently Reeb flows on the tight 3-sphere, it is natural to ask which periodic orbits bound such a disk. Hryniewicz's criterion answers this for dynamically convex flows, with no genericity assumption. The answer is purely topological: a periodic orbit bounds a disk-like global section exactly when it is unknotted with self-linking number . The criterion is used in celestial mechanics: Joung and van Koert apply it to validated periodic orbits of the restricted three-body problem (arXiv:2407.19159).
Timeline.
Use coordinates on , the Liouville form and the symplectic form .
Let be smooth and set . Assume that every ray from the origin meets exactly once, and that it crosses transversally:
Then is a strictly star-shaped hypersurface diffeomorphic to . Every contact form on that matters below arises this way, up to diffeomorphism (see Formalization scope).
The Hamiltonian vector field is defined by . With this sign, on . So is a positive multiple of the Reeb vector field of the contact form , and its orbits are the Reeb orbits reparametrized. A periodic orbit is a solution with and . It is prime when is its least positive period. The contact structure is .
that is, every nonzero transverse vector turns by more than one full turn.
the linking number in , with oriented as the boundary of the star-shaped domain it bounds. This agrees with Hryniewicz's Definition 1.5, which uses a section of over a spanning disk.
For every dynamically convex strictly star-shaped and every prime periodic orbit :
The statement fixes no constants and no non-degeneracy, and it covers every dynamically convex star-shaped surface.
If is unknotted with , then fibres smoothly over . Every fibre is the interior of a disk-like global surface of section whose oriented boundary is .
Let be any disk-like global section. Every periodic orbit through a fixed point of the first-return map of is unknotted, has self-linking number , and so bounds the page of an adapted open book.
The result. The criterion turns a dynamical question into a topological check. It does not depend on whether the orbit is degenerate, and degenerate orbits are what one meets at bifurcations and on symmetric levels. Every periodic orbit in a strictly convex energy surface that is unknotted with is a binding, so the flow is organised by many open books at once. Theorem 1.8 makes this concrete: the Hamiltonian flow twists around two different bindings, and . In applications, numerically validated orbits become analytic global sections without a separate non-degeneracy check (Joung–van Koert, Theorems 1.2 and 1.5).
Formalizing it. The theorem is proved, in a 50-page paper that relies on Hofer–Wysocki–Zehnder's theory of pseudo-holomorphic curves in symplectizations. It has no machine-checked proof. Mathlib has no Conley–Zehnder index, no self-linking number, no linking number of curves in , and no global surfaces of section. A Lean statement fixes every sign and orientation convention involved: the sign of , the orientation of , which push-off defines , and the index of degenerate orbits. Each of these is easy to get wrong in prose. Formal proofs of the parts that use no holomorphic curves are valuable on their own: the necessity direction, the description of the index by winding intervals, and the explicit ellipsoid examples.
The obvious route is to approximate the contact form by non-degenerate forms that keep as an orbit, and then apply the non-degenerate theorems. This fails. The need not be dynamically convex. They can have orbits of very high action with that are not linked with , so the Hryniewicz–Salomão criterion does not apply to (Hryniewicz, p. 4). The families of planes that would give the pages for have to be controlled directly as , and this is not a formal limit argument.
A second obstruction is genuinely global. A disk spanning and transverse to the flow in its interior is easy to produce when . Showing that every trajectory returns to it is the whole content of the theorem, and no local or perturbative argument gives it.
For the formalization, nothing in the proof of sufficiency avoids finite-energy pseudo-holomorphic planes: Fredholm theory, asymptotic analysis, bubbling-off and compactness all enter. None of this exists in Lean.
Fin 4 → ℝ with coordinates ordered . , and are defined explicitly, with the sign conventions above.ContDiff ℝ ⊤) functions with the ray condition and on . The Reeb flow of a general dynamically convex form on reduces to this case, up to diffeomorphism and positive time change: such a form is tight (Hofer–Wysocki–Zehnder), and every tight form on comes from a star-shaped hypersurface (Eliashberg 1992). That reduction is not part of the targets. Hryniewicz makes the same reduction (§3, first paragraph).A contact structure on a manifold of odd dimension is a field of hyperplanes that is as far from integrable as possible. Contact structures are the odd-dimensional counterpart of symplectic forms. They arise on every star-shaped energy level of a Hamiltonian system, on unit cotangent bundles (geodesic flows), and on links of singularities. They are the setting of Reeb dynamics and of the Weinstein conjecture.
Gray's stability theorem says that on a closed manifold contact structures have no local moduli. If , , is a smooth family of contact structures, there is an isotopy with . A contact structure can therefore be deformed only within its isotopy class, and every classification of contact structures (tight versus overtwisted, Eliashberg's classification on ) is a classification up to isotopy because of it.
Timeline.
The closed manifold is a compact submanifold of Euclidean space. Let be smooth, let be compact, and assume is surjective for every . Then is a closed smooth manifold of dimension with tangent spaces
A one-form is a smooth map , restricted to . Its exterior derivative is
This is the condition in the form of Geiges' Remark 2.3. It forces to be odd. The contact structure is . Contact structures are cooriented throughout, as in Geiges' standing assumption (§2).
For every smooth family of contact forms , , on there is an isotopy of with
stated pointwise: for , iff .
The goal concerns the contact structures. It fixes no normalization of the forms and no dimension.
The same isotopy can be chosen with smooth functions such that
Moreover, every point at which vanishes on for all stays fixed: .
The result. Gray stability is the basic rigidity statement of contact topology.
Formalizing it. The theorem is classical and has a short proof on paper. Mathlib, at the revision used here, has no differential forms on manifolds, no Lie derivative, no global flows of time-dependent vector fields on compact submanifolds, and no contact structures. The mission builds these concretely on submanifolds of :
All of these are reusable for Moser's theorem on volume and symplectic forms and for the Darboux and neighbourhood theorems.
The proof is soft, but two steps are not formal.
It has a unique solution at each point, but only because is non-degenerate on and the Reeb vector spans the kernel of . The solution must also depend smoothly on and be tangent to ; the ambient form is in general not contact off . 2. Integrating it. The isotopy is the flow of , which must exist for all and stay on . Compactness of enters exactly here. On open manifolds the statement is false (Remark 2.21(2)).
The tempting shortcut of asking for does not work. Contact forms themselves are not stable, as the Hopf family on shows (Remark 2.21(1)), and the conformal factor cannot be dropped.
Fin n → ℝ; is a compact regular level set of a smooth .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.
Whether the diameter of a polyhedron is bounded by a polynomial in its number of facets is one of the central open questions of convex geometry, and it bears directly on linear programming: the diameter of the graph of a polyhedron is a lower bound on the number of pivots of any simplex method that moves along edges. Write for the largest diameter of a -dimensional polyhedron with facets. The best known bounds are
due to Klee and Walkup (1967) and Kalai and Kleitman (1992), and the gap between them has stood for decades.
A recurring approach is to isolate a few purely combinatorial properties of polyhedra and to prove bounds for every object having them. Eisenbrand, Hähnle, Razborov and Rothvoß (2010) proposed a base abstraction defined by a single property, shared by all abstractions from which earlier bounds were derived. They showed that the known upper bounds survive in it, and, as their main result, that it admits almost-quadratic diameter. This mission formalizes that lower bound.
Timeline.
Let and let be the family of its -element subsets. Consider a graph whose vertex set is a nonempty subfamily of . The graph satisfies condition i) if
for each there exists a path connecting and whose intermediate vertices all contain .
The base abstraction is the class of all such graphs; is called the dimension and the number of facets. Write for the length of a shortest – path, and
The geometry behind the definition: in a non-degenerate polyhedron every vertex lies on exactly facets, so labelling vertices by their facets gives distinct -subsets of ; and two vertices can be joined without leaving the smallest face containing both, i.e. through vertices lying on every facet common to and . Hence (the subject of a separate mission of this series).
In the Lean development, EHRR10.LowerBound.CondI V G is condition i), and EHRR10.LowerBound.InB d n V G says that is nonempty, all its members have elements, and condition i) holds.
Explicitly, there are and such that for every with there is a graph and two vertices of with . The constants and are left unfixed, so the goal survives any improvement in the constant.
There are no milestones: the source is an extended abstract that states the result without a proof and names no intermediate lemma.
The result. Since , any proof of a bound on bounds the diameter of all non-degenerate polyhedra. The paper shows that the Kalai–Kleitman and Larman bounds are of this kind. The lower bound shows the limits of the approach: an argument that uses only condition i) cannot prove a linear (Hirsch-type) bound, because grows almost quadratically in . Any proof of a linear bound must use further geometric properties of polyhedra. A polynomial, even quadratic, upper bound for is not excluded by the result.
Formalizing it. The result is proved in the literature (Math. Oper. Res. 35 (2010) 786–794); it has no machine-checked proof. A formal proof requires an explicit combinatorial construction of graphs in the base abstraction with large diameter and a probabilistic existence argument, neither of which is currently on the platform. The platform's Hirsch campaign has the same abstraction in its layer-family form (Hirsch_clf, whose description mentions the families in prose) and the proved upper bound Hirsch.clf_saturated_quadratic_bound, , on a subclass that contains the constructions of this paper; neither states the lower bound.
A long path through all of has exponential length but violates condition i): two vertices of the path generally share elements that some intermediate vertex lacks. Condition i) must hold for every pair of vertices simultaneously, which forces the vertices containing any fixed set to induce a connected subgraph. Building a long graph means arranging many -sets so that each of these exponentially many connectivity constraints holds at once while the graph distance between two vertices stays large. The authors announce that their construction relies on disjoint covering designs, and that the existence of such designs with the required parameters is obtained from the Lovász Local Lemma.
Fin n; vertices are the -sets themselves, V : Finset (Finset (Fin n)) and G : SimpleGraph V. Distinct vertices carry distinct labels.Real.log); the base only rescales .SimpleGraph.dist at least ; is not defined as a supremum, so no junk value enters. SimpleGraph.dist returns for unreachable pairs, which could only make the statement harder.The goal cannot be trivialized by a non-injective labelling (vertices are the sets), by checking condition i) only on adjacent pairs (it is required for all pairs, with kept along the whole walk), or by a zero constant ( is required).
Infrastructure that a solution needs and that is reusable beyond this mission: covering designs and disjoint covering designs over Finset (Fin n), the Lovász Local Lemma (posed on the platform as AppliedComb.ManyFaces.local_lemma_symmetric), and a toolkit for proving condition i) for graphs assembled from blocks. Contributions of any of these as separate theorems are welcome.
Stochastic and online subgradient methods are the workhorse of large-scale learning: each step touches one example, costs time linear in the dimension, and needs no line search. Their weak point is the step size. A single global step size treats every coordinate alike, while in high-dimensional, sparse problems (text, click-through data, bag-of-words features) most coordinates are zero in most examples, and the few informative rare features receive vanishingly small updates.
AdaGrad (Duchi, Hazan and Singer, JMLR 2011; McMahan and Streeter, COLT 2010, independently) chooses a separate step size per coordinate from the gradients observed so far. Its diagonal version is the ancestor of RMSProp and Adam and is one of the most widely used optimizers in machine learning. This mission targets the paper's regret guarantee for diagonal AdaGrad, which explains when per-coordinate adaptation pays off.
Timeline. Zinkevich (2003) proved regret for online projected gradient descent. Nesterov (2009) and Xiao (2010) analysed dual averaging with a regularizer; Duchi, Shalev-Shwartz, Singer and Tewari (2010) analysed composite mirror descent. Auer and Gentile (2000) proved the scalar inequality that makes adaptive step sizes work. Duchi, Hazan and Singer (2011) combined these into adaptive proximal functions with data-dependent regret bounds.
Work in with the Euclidean inner product and . A closed convex set with is fixed, together with a convex regularizer (for example ). In rounds a learner plays , a convex loss is revealed, and the learner observes a subgradient of at : for all . The regret against a comparator is
For each coordinate , let and . Diagonal AdaGrad (Figure 1 of the paper) has parameters , , starts at , and in round uses the proximal function . It updates by one of two rules:
For the primal-dual update with , and every ,
For the composite mirror descent update with , and every ,
Lemma 16 and Propositions 2 and 3 are stated in the paper for general proximal functions; here they are specialised to diagonal quadratic ones, .
The result. The quantity is never larger than and can be far smaller when gradients are sparse or coordinate scales differ. Theorem 5 shows that diagonal AdaGrad does as well as the best fixed diagonal preconditioner chosen in hindsight, up to a constant, without knowing the gradients in advance (Corollary 1 and Corollary 6 of the paper). Through online-to-batch conversion the same bound gives convergence rates for stochastic convex optimization with sparse data. The theorem underpins the theoretical case for per-coordinate adaptive step sizes.
Formalizing it. The result is proved on paper; to our knowledge no machine-checked proof of AdaGrad's regret bound exists, in Lean or elsewhere. The formalization produces checked versions of the two regret templates (composite mirror descent and dual averaging with changing proximal functions), which are reused by most later analyses of adaptive methods, and of the Auer–Gentile inequality. The formal statements also make precise two hypotheses the printed theorem leaves implicit (see Formalization scope).
The obvious argument fixes one proximal function and applies the classical mirror-descent or dual-averaging bound. That fails because AdaGrad's changes every round and depends on the very subgradients whose norms are being bounded: the classical bounds assume a fixed , and with changing new drift terms appear that must be shown to be small. The gradient term has denominators that grow with the data, so it is not bounded term by term; it has to be bounded as a whole sum. For dual averaging there is an additional index shift: round 's subgradient is measured in the dual norm of , which has not yet seen .
Vectors live in EuclideanSpace ℝ (Fin d), so ‖·‖ is the Euclidean norm; is a separate definition supNorm. Rounds are 1-based, with sums over Finset.Icc 1 T; . Losses and the regularizer are real-valued convex functions on all of , so extended-valued regularizers (indicator functions) are excluded, and the constraint is carried by . The subgradient relation is the published platform definition ShorNonsmooth.AlmostDiff.IsSubgradient. Each update is a predicate ( and minimizes the update objective over ), since the minimizer need not be unique; the theorems hold for every run. The factor in follows Figure 1. Dual norms use Lean's division, where is the paper's . The losses are a fixed sequence, which also covers adaptive adversaries because the run is determined by the losses.
Two restrictions relative to the printed Theorem 5, both forced by the paper's own proof:
Proposition 2 is stated with strictly positive weights. The primal-dual part of the goal with is a degenerate case in which every vanishes.
A run predicate without the subgradient link , an argmin without , a comparator outside , or computed without round would each make the statement trivial or different. The definitions rule all of these out.
Needed infrastructure: elementary convex analysis on (first-order optimality of a convex objective over a convex set), finite sums and square roots. Nothing beyond Mathlib is required. The two regret templates (Propositions 2 and 3) and inequality (24) are reusable beyond this mission. Proofs of any milestone, and of the full-matrix analogues, are welcome.
Markovian decision processes with the long-run average cost criterion model systems run indefinitely: inventories, queues, maintenance schedules, communication links. For a finite state space the theory was settled by the early 1960s. Howard's policy improvement (policy iteration) procedure (1960) finds an optimal stationary rule in finitely many steps, and Gillette (1957) and Derman (1962) showed that a stationary deterministic rule is optimal over all rules, history-dependent and randomized included (Derman 1962).
Many models of interest, such as queues with unbounded buffers and inventories with unbounded backlog, have a denumerable state space, and there the finite theory breaks down. Derman's paper (Ann. Math. Statist. 37 (1966) 1545–1553) gives two counterexamples in §2, both under bounded costs and finitely many decisions per state. In the first, due to Maitra, no optimal rule exists. In the second, a randomized stationary rule beats every deterministic one. It then gives sufficient conditions under which a stationary deterministic optimal rule exists and policy improvement finds it.
Timeline:
The system is observed at times in a state of a denumerable set . At state one of decisions is made (condition (A)). It costs , and the next state is with probability . The costs are bounded (condition (B)) and may have either sign. A rule chooses the decision at each time with probabilities that may depend on the whole history. The class of all rules is , and is the class of stationary deterministic rules ("make decision at state "). The average cost of from is
A rule is optimal over if for every and every .
The optimality equation (1) asks for a number and a bounded with
and equation (2) is its version for one rule , with in place of the minimum. Condition (C): every induces an irreducible Markov chain all of whose states are positive recurrent. Condition (E): every has a solution of (2), bounded uniformly in and . Condition (F): for every the Cesàro limits of satisfy . One policy improvement iteration replaces by a rule whose decisions minimize at every state.
Under (A), (B), (C), (E) and (F), let be any sequence of policy improvement iterations from an arbitrary . Then the sequence has a limit point , and every limit point satisfies
with .
Theorem 1 is the countable-state verification theorem. It is the template for all later average-cost theory on infinite state spaces, which replaces boundedness of by growth or Lyapunov conditions. Theorem 4 extends policy improvement, the standard algorithm for finite average-cost problems, to denumerable state spaces, under conditions that do not reduce the problem to a finite one.
Derman proved these results in 1966. None of them has been machine-checked: the platform has finite-state average-cost policy iteration and finite-state verification theorems, but no countable-state result of this kind. A formal development checks the analytic steps that the paper treats briefly. These are the interchange of limits and infinite sums in (3), (9) and (11), and the identification of the Cesàro limits of a positive recurrent chain with its steady-state probabilities.
On a finite state space, policy improvement terminates because there are finitely many rules and the average cost strictly decreases. On a denumerable state space is uncountable, so neither step works. The sequence need not terminate. With ties in the minimization it need not converge either. A strict decrease of does not force the gaps to vanish. That needs (F), a uniform positive lower bound on the long-run occupation of each state. Passing to the limit in (2) along a subsequence requires a limit interchange in an infinite sum, which works only because is uniformly bounded. Finally, comparing with history-dependent randomized rules needs the finite-horizon argument behind (6). A stationary-rule comparison is not enough.
The model is the published Markov decision chain SennottDP.AvgFinite.MDC: a countable state type, a finite nonempty Finset of decisions at each state (so (A) is built in), and transition probabilities in summing to one. History-dependent randomized rules are Policy M, and is StationaryPolicy M. The chain notions (irreducibility, positive recurrence, steady state ) come from the published SennottDP.MarkovCost.Chain. The conventions are as follows.
w with (B). The nonnegative cost field of MDC is unused, and is not assumed.limsup with the paper's normalization .Two trivializing formalizations are ruled out: optimality is over all history-dependent randomized rules, never only over , and is computed from the process law, never defined through (2).
A complete development needs Cesàro convergence of -step probabilities to for positive recurrent chains, dominated convergence for bounded functions against stochastic kernels, the finite-horizon dynamic programming principle for history-dependent rules, and a diagonal (Tychonoff) argument in . The first and third are reusable well beyond this paper. Contributions of these lemmas as separate theorems are welcome.
Stochastic programs often optimize a decision that changes several random outcomes at once. A reference outcome may be acceptable even when no fixed threshold captures its risk: one wants the new outcome to be preferable under every increasing concave assessment of gains. Second order stochastic dominance expresses that comparison. Dentcheva and Ruszczyński study optimization with several such constraints, each imposed on a nonlinear outcome operator, and show how the constraint multipliers can be represented by utility functions rather than scalar penalties (Dentcheva–Ruszczyński, 2004). Their earlier paper, Optimization with stochastic dominance constraints, treats the pure dominance case without the nonlinear decision map; the present result adds decision dependent outcomes, multiple constraints, and split variables. Ogryczak and Ruszczyński's second performance function supplies the stochastic order used here (Ogryczak–Ruszczyński, 2002).
The utility interpretation matters when a modeler wants a certificate explaining why a solution satisfies a risk preference expressed by dominance. The theorem identifies a concave utility for each binding dominance constraint and an essentially bounded multiplier for each comparison between the split outcome and the outcome produced by the decision. The source is a revised April 2003 author manuscript, later published in Mathematical Programming in 2004; the page and equation numbers below follow that manuscript (author manuscript).
Work on a probability space . An integrable random outcome is a measurable real function with finite expected absolute value; denotes these outcomes, and denotes essentially bounded ones. The decisions lie in a convex set inside a separable locally convex Hausdorff real vector space . An integrable objective outcome and integrable constraint outcomes depend continuously in the norm on . Almost every realized map and is concave and continuous on all of . Fixed integrable outcomes serve as references; the th comparison is required over a bounded interval .
For an outcome , its second performance function is the area below its distribution function:
The split program (11)–(14) chooses and to maximize , subject to for every , and almost surely. Larger outcomes are preferred, so a dominating has the smaller curve. The split variables expose the dominance and decision coupling as separate constraints (manuscript, pp. 3–4).
The utility cone consists of concave nondecreasing functions that vanish for and are affine with a nonnegative slope for . Given in these cones and , the Lagrangian is
Uniform dominance means one decision makes every dominance inequality uniformly strict on its interval: for each , has a positive lower bound over (Definition 1, p. 7).
Theorem 2 is the goal. Under uniform dominance, every optimum of the split program admits and nonnegative with
Conversely, an attained Lagrangian maximum satisfying the split constraints and these complementarity equations is a primal optimum. The milestone list follows the source's measure multiplier equations (23)–(24), the measure to utility identity (25), Theorem 1's expected concave subgradient characterization, and the converse's weak duality inequality (manuscript, pp. 5, 8–10).
The result gives a concrete optimality certificate in a program whose constraints compare entire outcome distributions. Each utility multiplier represents the active part of one dominance constraint. Each accounts for the almost sure inequality linking a split outcome to the decision. The equalities show exactly where those constraints are complementary, while the Lagrangian maximum compares the proposed solution with all integrable split outcomes. The paper derives a dual problem from the same Lagrangian in its following section (manuscript, p. 11).
The mathematical theorem is proved in the paper. This mission seeks a machine checked version of its definitions, measure identity, subgradient statement, and both directions of Theorem 2. The published second performance definition is reused as a reference; the nonlinear split program and its utility and measure Lagrangians require a development specific to this paper. The 2003 pure dominance mission contains related local drafts, but those items are not published and cannot currently be imported as platform theorems.
The dominance inequality contains a continuum of thresholds for each outcome. A scalar multiplier at one threshold cannot capture the whole constraint, while the dual object for continuous functions on is a measure. The split inequality lives in , where the nonnegative cone has empty interior, so an ordinary interior point argument applied to all constraints at once does not match the paper's setting. The source also needs a subgradient of expected concave utility represented by an almost surely selected, essentially bounded random vector; the conclusion is stronger than merely knowing that the expected objective has a deterministic supporting functional (manuscript, pp. 5–9).
The Lean development keeps the general separable locally convex Hausdorff decision space, the convex set , and a finite index type for the dominance constraints. Operators are function representatives with explicit integrability, continuity in , and samplewise concavity and continuity. Almost sure comparisons use the probability measure ; the null set for each realization condition precedes the quantifier over decisions. Split outcomes range only over integrable functions, and utility multipliers range over the exact cone . The condition includes almost sure strong measurability and essential boundedness. Maxima in Theorems 1 and 2 are attained maxima, expressed by membership and comparison against every competitor, never a real supremum with a default value.
The source prints a strictly positive affine slope in its definition of , but immediately calls this class a cone and later uses the zero measure. The formalization uses ; with , Theorem 2 is false for a slack dominance constraint. Uniform dominance is expressed as a positive lower bound rather than a real infimum. The measure milestone uses finite nonnegative measures supported on closed intervals, including endpoint atoms. These conditions exclude default zero integrals, an empty interval disguised by an infimum, and a vacuous utility class. Contributions to the measure to utility correspondence, integration identities, and expected concave subgradient infrastructure can be reused beyond this program.
Regularized least squares (RLS) in a reproducing kernel Hilbert space is a basic estimator of nonparametric regression and of kernel-based learning. Its learning rate is the speed at which the expected excess risk goes to zero as the sample size grows. A rate is useful only if it is known to be optimal, and optimality is a lower-bound statement about all learning algorithms.
Caponnetto and De Vito (Found. Comput. Math. 7 (2007)) prove two kinds of lower bound. The first is a minimax lower rate (their Theorem 2): for every algorithm and every , some distribution in the prior is hard. Their Section 2 (p. 6) points out a weakness of this notion: the bad distribution may change with . A practitioner, however, faces one fixed unknown distribution and asks how the error decreases as data accumulate. The individual lower rate answers that question. It asks for a single distribution, chosen against the algorithm but not depending on , on which the expected excess risk stays above along infinitely many .
The notion comes from nonparametric regression. Györfi, Kohler, Krzyżak and Walk (A Distribution-Free Theory of Nonparametric Regression, Springer 2002, §3, Theorem 3.3) proved individual lower rates for classes of smooth regression functions. Theorem 3 of Caponnetto–De Vito carries the result to vector-valued RKHS with the spectral priors . Theorem 1 of the same paper shows that these priors are learned by RLS at rate .
The input space is Polish. The output space is a real Hilbert space of finite dimension . The hypothesis space is a separable real Hilbert space of functions in which evaluation is continuous, so that for bounded operators . Hypothesis 1 asks that be measurable and that for every .
A distribution on has marginal and conditional distributions . The risk of is
Hypothesis 2 asks for square-integrable outputs, a minimizer of over , and a Bernstein-type moment bound on the noise with constants .
The operator on satisfies . Its nonzero eigenvalues are , with orthonormal eigenvectors .
For positive constants and parameters , , the prior (Definition 1) is the set of probability measures satisfying three conditions:
A learning algorithm is a sequence of maps , and is its output on a sample of size drawn from .
For every ,
Equivalently, there is such that every algorithm admits one with expected excess risk at least for infinitely many . The constant may depend on the prior and on , but not on the algorithm.
with and . Every such distribution belongs to the prior. 3. (63) (p. 27). Under these distributions, with . 4. (68) (p. 28, corrected). for , where . 5. (67) (pp. 28–30). Averaged over independent fair signs , the expected number of sign errors over , weighted by , is at least .
Theorem 3 shows that no algorithm, RLS included, converges on every fixed distribution of faster than , for any . For this exponent is arbitrarily close to the exponent of the upper rate of Theorem 1, so RLS with the regularization parameter of Theorem 1 is near-optimal even in the individual sense. The paper notes (p. 6) that full individual optimality would still need an upper rate in expectation or an individual lower rate in probability; that question is outside this mission.
The theorem is proved on paper and has been cited widely. To our knowledge no part of it has been machine-checked. A formalization would produce:
A minimax argument picks a hard distribution for each , and that is not allowed here: the distribution must be fixed before varies. The obvious repair, taking the worst distribution for one and keeping it, fails, because a distribution that is hard at sample size can be easy at sample size .
What has to be shown is a lower bound that holds for one distribution simultaneously along infinitely many sample sizes. Bounds that hold separately at each , with a distribution that may depend on , do not combine into such a bound.
A second difficulty arises in any reduction to a coordinatewise testing problem: each observation depends on all spectral coordinates of the regression function at once, so testing one coordinate is not literally the problem of Proposition 7.
is Mathlib's RKHS ℝ H X Y, with = RKHS.kerFun H x and finite-dimensional. The paper's is written Sig.
t (n-1).InPrior encodes , including "probability measure".lintegrals of nonnegative quantities, and samples are Fin ℓ → X × Y under the product measure.stdGaussian Y.Two parts of the print are corrected, and both corrections are stated in the items.
The goal mentions none of , , or . It is the lower rate (3) for the full prior with . A formalization that fixed the algorithm, let the distribution depend on , or let the constant depend on the algorithm would prove a different, weaker statement.
A complete development needs:
Reusable pieces include Proposition 7, the Bayes-error monotonicity argument on p. 29, and the identification of the risk minimizer of a Gaussian-noise model. Contributions on any milestone are welcome, as are proofs of the measurability facts (elements of are measurable under Hypothesis 1).
In online routing of virtual circuits, connection requests between pairs of nodes of a capacitated network arrive one at a time. Each request must be accepted and routed on a single path with bandwidth , or rejected, immediately and irrevocably, and no edge may carry more than its capacity. The goal is to maximize the number of accepted requests (the throughput). The model goes back to Awerbuch, Azar and Plotkin (FOCS 1993), whose deterministic algorithm has a logarithmic competitive ratio when edge capacities are at least logarithmic in the size of the network, and it underlies the analysis of admission control in circuit-switched and bandwidth-reserved networks.
Buchbinder and Naor (Math. Oper. Res. 2009) recover an algorithm with the same competitive factor from a general recipe: an online primal–dual scheme first produces a feasible fractional routing online, and an online version of Raghavan's pessimistic estimator (J. Comput. Syst. Sci. 1988) then rounds it, also online. This mission formalizes that construction and its guarantee (Section 5.2 of the paper, with the Section 3 scheme it uses).
Timeline:
Let be a finite set of edges with capacities , and . Requests arrive online; request comes with a finite list of admissible paths, each a set of edges, all of size at most .
A fractional routing assigns flows ; it is feasible when for every request and the load of every edge is at most . Its value is ; is the largest value of a feasible routing of the arrived requests, an upper bound on the integral optimum.
The fractional scheme. The covering LP paired with the routing LP (the paper's primal, Fig. 3) has variables (cost ) and (cost ) with constraints . When arrives, its paths are visited in order; for each path whose constraint fails, is raised from to the least value restoring it, while for and follow the flow ( the load of , the flow of ). The parameters are and .
The rounding. With the rounding scale , the integral edge usage and the number of served requests, the potential is ,
After the fractional round of , the algorithm serves on a path (adding to for ) if this gives potential at most the potential before the round; otherwise it rejects .
For every request sequence, the algorithm never exceeds a capacity, and for every feasible fractional routing ,
The fractional scheme's flows are feasible and for every feasible .
initially, always, and whenever the flows of a request are raised by a non-negative amount of total at most , serving the request on some path or rejecting it does not increase .
The result shows that a deterministic online algorithm for throughput-competitive routing, previously designed by hand, falls out of two generic components: an online fractional packing scheme and an online pessimistic estimator. A side product is that the fractional phase alone produces, online, a near-optimal routing that respects all capacities exactly, independently of their size. When the rounding loses only a constant factor and the algorithm is -competitive, as in Awerbuch–Azar–Plotkin.
The results are proved in the paper; none is machine-checked. A formalization supplies a checked instance of the online primal–dual method together with derandomized online rounding, and fixes the constants the paper leaves inside . Related platform content: the monograph's OnlinePrimalDual.Routing.per_copy_guarantee and routing_competitive concern the Buchbinder–Naor -competitive algorithm with copies of the graph, a different scheme.
The fractional guarantee is argued in the paper continuously (rates of change of the primal and dual values), while the scheme as formalized is discrete: each flow is the least value restoring a constraint, and every primal variable is a maximum whose branch may switch during the increase. The continuous argument does not transfer verbatim, and feasibility depends on the least value restoring the constraint with equality.
The rounding is a derandomization. The existence of a good path or a good rejection is established in the paper as an expectation over a random trial; a deterministic statement about finitely many alternatives is what the mission asks for, with all exponential terms of under control at once. A frequent first attempt compares with the potential after the fractional round; the rule compares with , before the flow increase, and the guarantee is stated for that comparison.
Fintype E; capacities are real and positive. A request is a List (Finset E) of paths; the request sequence is a list. Simple paths of a graph are a special case; nothing in the argument uses graph structure. is a parameter with every path of size at most .List (List ℝ) of the shape of the request sequence. is quantified as "every feasible fractional routing".sInf). Ties among good paths are broken by list order; only paths that received flow in the current round are candidates for serving, so a request whose flow was not increased is rejected.Contributions welcome: proofs of the milestones, a reusable lemma "convex combination value some outcome value" for derandomization, and the discrete-to-continuous bridge for the Section 3 scheme.
Regularized least squares (RLS), also called kernel ridge regression, is one of the standard estimators of statistical learning: given a sample of input–output pairs, it fits a function from a reproducing kernel Hilbert space by minimizing the empirical squared error plus a multiple of the squared norm. Caponnetto and De Vito (FoCM 2007) proved that, over a class of distributions described by two parameters — the decay of the eigenvalues of the kernel's covariance operator and the smoothness of the regression function relative to it — RLS with a well-chosen regularization parameter converges at the rate in the sample size (their Theorem 1). An upper rate on its own does not say whether another method could do better. This mission formalizes the matching minimax lower rate (their Theorem 2): when the output space is finite dimensional, no learning algorithm whatsoever converges faster than uniformly over the class. Together the two theorems say that RLS is rate-optimal, and they are the reference point for later work on spectral regularization, early stopping and distributed kernel methods.
The paper's lower bound adapts the minimax analysis of DeVore, Kerkyacharian, Picard and Temlyakov (FoCM 2006) to the vector-valued RKHS setting.
Inputs lie in a Polish space and outputs in a real Hilbert space of finite dimension . The hypothesis space is a separable Hilbert space of functions in which evaluation is continuous; is the adjoint of evaluation at , so . Hypothesis 1 asks that be measurable and that for every .
A distribution on has risk . Hypothesis 2 asks that , that the risk has a minimizer (taken of minimal norm), and that the noise satisfies a Bernstein moment condition with constants . With the marginal of , the operator on has the quadratic form and a spectral decomposition .
The prior (Definition 1, with fixed positive , and ) is the set of probability measures satisfying Hypothesis 2 with such that
the infimum over all learning algorithms . The constant in front of the rate is left free, so the goal asserts only the exponent.
The result. Theorem 2 shows that the exponent attained by RLS cannot be improved by any estimator over when ; for RLS is optimal up to a logarithmic factor. It separates what is a property of the problem class from what is a property of the algorithm: improvements to kernel methods must change the class (stronger assumptions) rather than the rate. The construction — a packing of the source class measured in the -norm, combined with a KL bound for an explicit noise model — is the template reused in many later lower bounds for kernel and inverse-problem estimators.
Formalizing it. The result has been proved since 2007; no machine-checked version exists. A formal proof needs the information-theoretic lower-bound machinery (a Fano-type inequality for many hypotheses), a Varshamov–Gilbert-type packing of the Hamming cube, KL divergence between explicit mixtures, and the spectral description of the covariance operator of a vector-valued RKHS. Each of these is reusable well beyond this paper. The mission also makes precise the paper's implicit conventions (see below), which a pen-and-paper reader fills in silently.
The upper half of the argument is not the hard part; the hard part is that the lower bound is uniform over all measurable algorithms, which no direct computation reaches. The step that does not follow from the paper alone is Theorem 5: its proof invokes Lemma 3.3 and Eq. 3.12 of DeVore et al., a Fano-type inequality bounding the probability of correct identification among hypotheses with pairwise KL divergence at most a given level. That lemma is not stated in the paper and is not in Mathlib; it must be formalized. A second obstacle is the packing (Proposition 6), whose proof is a probabilistic union bound with Hoeffding's inequality. A naive attempt to prove Theorem 2 by exhibiting a single bad distribution fails: for any fixed some algorithm (the constant one returning ) has zero excess risk, so the bad distribution must depend on the algorithm, and the order of quantifiers is essential.
Mathlib's RKHS ℝ H X Y provides the function space with continuous evaluation, RKHS.kerFun is , and InformationTheory.klDiv is the Kullback–Leibler information. The operator is never built as an operator-valued Bochner integral: it is recorded through its quadratic form and an eigen-system indexed by from (the paper's is t (n-1)). The trace in Hypothesis 1 is a series over a Hilbert basis of ; the conditional law in Hypothesis 2 is Measure.condKernel, and the moment integral there is a lintegral. in the goal is .
Conventions and added hypotheses, each implicit on the page:
The goal is the –– unfolding of the limit and mentions neither , the KL bound nor the packing, so it cannot be discharged by any of the milestones' constructions in isolation; the distribution is chosen after the algorithm, never before it.
Contributions welcome: a general Fano/DeVore-type lemma for finitely many hypotheses, the Varshamov–Gilbert bound, KL ≤ χ² for finite mixtures, and lemmas relating covForm to the excess risk.
Regularized least squares (RLS, also called kernel ridge regression or Tikhonov regularization) is the simplest learning algorithm built on a reproducing kernel Hilbert space. Given examples drawn independently from an unknown distribution , it returns the function in a hypothesis space that minimizes the empirical squared error plus times the squared norm. It is used in regression, in multi-task learning with vector-valued outputs, and as the reference case for spectral regularization methods.
The basic statistical question is how fast the excess risk of the RLS estimator goes to zero as grows, and how to choose to get that speed. Caponnetto and De Vito (FoCM 2007) answered it for a family of priors described by two numbers: the decay rate of the eigenvalues of the covariance operator of the input distribution and the regularity of the target function. Their Theorem 1 gives the upper rate ; Theorems 2 and 3 show that no algorithm does better when the output space is finite dimensional. This mission formalizes the upper rate.
Timeline. Cucker and Smale (2002) and De Vito, Caponnetto and Rosasco (2005) gave rates for RLS that did not depend on the eigenvalue decay of . Zhang (2005) introduced the effective dimension as the complexity measure. Caponnetto and De Vito (authors' copy dated 2006, published 2007) combined it with a source condition to obtain rates that are optimal over , for vector-valued outputs. Steinwart, Hush and Scovel (2009) and Fischer and Steinwart (2020) later extended the analysis to other norms and to .
The input space is a Polish space and the output space is a real separable Hilbert space. The hypothesis space is a real separable Hilbert space of functions in which evaluation at each point is continuous. For , is the adjoint of evaluation at , so . Hypothesis 1 adds a measurability condition and a uniform trace bound .
A distribution on has marginal and conditional laws . The expected risk of is . Hypothesis 2 asks that , that attains its infimum over at some (the minimizer of minimal norm is used), and that the noise satisfies a Bernstein moment condition with constants .
The covariance operator is positive and trace class, with and eigen-decomposition , . The prior , for and , consists of the satisfying Hypothesis 2, with for some (source condition), and with for all (eigenvalue decay).
The RLS estimator minimizes over .
With and for , and for ,
The statement fixes the rate, not the constants: the threshold absorbs every constant of the prior.
provided and , where , , and . 4. Proposition 3: on , , and .
The result. Theorem 1 says that RLS with chosen from achieves the rate uniformly over the prior, and the companion lower bounds show this is the minimax rate for and finite-dimensional . The rate interpolates between the parametric rate (fast eigenvalue decay, smooth target) and slower nonparametric rates, and it identifies the effective dimension, rather than the dimension of , as the quantity that governs complexity. Theorem 4 is a non-asymptotic bound of independent use; it is the template for later analyses of spectral regularization, gradient descent with early stopping, and random-feature approximations of kernel methods.
The formalization. The result is proved on paper; no machine-checked proof of a kernel ridge regression rate is known to exist. A formal development requires a Bernstein inequality in Hilbert spaces, spectral calculus for a trace-class operator defined from a measure, and the operator-perturbation argument of Theorem 4. Two printed constants are corrected here: Theorem 4's proof yields , not , and Proposition 3's bound on has in place of . The paper also states Theorem 1 for ; that branch fails for and is not posed.
The obvious argument bounds by uniform concentration of around and multiplies by . That gives a variance term that ignores the eigenvalue decay of , and hence a rate that does not improve with . The optimal rate needs the variance measured through , which requires controlling in operator norm with high probability. This in turn needs concentration of in Hilbert–Schmidt norm, and the condition under which the empirical operator is close enough to . The noise is unbounded, so only the moment condition (9) is available, and the concentration step must use moment bounds rather than boundedness.
is Mathlib's RKHS ℝ H X Y, and is RKHS.kerFun H x. The trace in Hypothesis 1 is computed in a fixed Hilbert basis of . is the first marginal and is condKernel. The operator is not built as an operator-valued integral. It enters through its quadratic form and through an eigen-system , indexed from , so (17) reads . The effective dimension is . Samples are Fin ℓ → X × Y under the product measure, and probabilities of events are outer measures. "With probability at least " is stated as "the bad event has measure at most ". The noise condition and the moments of Proposition 2 are integrals of nonnegative functions with values in .
The hypotheses the paper uses but does not display are added: positivity of , and integrability of the random variable in Proposition 2. The RLS estimator of the goal is any family of minimizers of (18) for ; at and the parameter is degenerate. The goal quantifies uniformly: is chosen before , and the estimator is fixed before . The goal must not be replaced by a statement about or by Theorem 4's event: it is the uniform rate for the estimator itself.
Reusable infrastructure: Hilbert-space Bernstein inequalities (Proposition 2 alone is a valuable target), spectral calculus for compact positive operators given by a quadratic form, and the representer/normal equation for vector-valued RLS. Contributions of proofs for any milestone, and of supporting lemmas about trace-class operators and effective dimension, are welcome.
Many statistical parameters are defined implicitly, as the root of an estimating equation : a mean, a quantile, a regression coefficient, the minimizer of an expected loss. Owen's empirical likelihood builds confidence regions for such parameters by asking how far the empirical distribution of the data must be reweighted before the equation holds, and the profile of that distance has a chi-squared limit (Owen, Empirical Likelihood, 2001).
Blanchet, Kang and Murthy replace reweighting by transport: they measure how much the data must be moved, in the sense of optimal transport, before the equation holds. The resulting Robust Wasserstein Profile (RWP) function plays the role of the empirical-likelihood profile, and its value at the true parameter is exactly the smallest radius of a Wasserstein ball around the data that contains a distribution satisfying the estimating equation. Its asymptotic law is therefore what is needed to choose the radius of Wasserstein distributionally robust estimators, such as the square-root LASSO and regularized logistic regression, in a data-driven way (arXiv:1610.05627, §§1, 3, 4). This mission formalizes the paper's main limit theorem, Theorem 3.
Let be a cost. The optimal transport cost between probability laws and on is
the infimum over all joint laws of a pair with the given marginals (Eq. (7)). In this mission with and , and denotes the conjugate exponent, .
Let be an estimating function, and let be i.i.d. random vectors in with . With the empirical distribution of , the RWP function is
Write for the Jacobian of , and for the norm of the row vector , . The assumptions are:
A sequence is asymptotically stochastically bounded by , written , if for every continuous, bounded, non-decreasing .
Let . Under A1)–A4),
where for
and for
The formal goal also asserts that is finite and measurable and that both maxima are attained; these are facts the paper's statement presupposes.
Theorem 3 gives the rate at which the RWP function at the true parameter vanishes and an explicit random variable bounding its rescaled limit. The -quantile of yields a radius for which the Wasserstein ball around contains, with asymptotic probability at least , a law satisfying the estimating equation at (§3.1, (19)); this is the paper's prescription for the regularization parameter of square-root LASSO and of regularized logistic regression (§4). Example 3 (p. 14) shows the bound is sharp for the mean: . Matching lower bounds (Propositions 4 and 5) need further assumptions and are not part of this mission.
The result is proved in the paper; no machine-checked version of it, or of any RWP or empirical-likelihood limit theorem, is known to exist. A formalization would check the duality argument for the problem of moments, the passage from the dual representation to a localized maximization, and the continuous-mapping step, and would produce reusable statements: strong duality for transport-cost moment problems, the closed form of the conjugate of , and a uniform law of large numbers over a compact parameter set.
The obvious route is to apply the central limit theorem to and pass to the limit inside the dual representation (31). This fails as stated, for two reasons. First, the supremum in (31) is over all of , and convergence of the objective on compact sets does not control the supremum; Lemma 2 is needed, and it uses A4) through a lower bound on that is uniform over the unit sphere. Second, the penalty involves the derivative of at points that are not localized, with no moment assumption on ; the proof must truncate to and to a specific near-optimal , and then remove the truncation. The case differs: the inner supremum is or , and the limit becomes a maximization over a constraint set.
Vectors are Fin k → ℝ; and norms are Mathlib's PiLp norms, so is allowed, with and p.HolderConjugate q. The samples are a sequence W : ℕ → Ω → (Fin m → ℝ), mutually independent (iIndepFun) and identically distributed with W 0, which plays the role of ; uses through the published empiricalDistribution. Distinct samples are not assumed in Theorem 3; Proposition 3 and (31) keep the §3.1 assumption of distinct samples. Transport costs and are -valued lower Lebesgue integrals and infima; is computed in the extended reals with the moment in . 's law is multivariateGaussian 0 Cov on EuclideanSpace ℝ (Fin r).
The goal is a conjunction: finiteness of for , its a.e.-measurability, attainment of the maxima in , and the limsup bound. Without the first three, a real-valued formalization could hold for the wrong reason (an infinite converted to , a non-measurable integrand integrated to , or an unbounded supremum replaced by ); the conjunction rules this out.
Readings of the page recorded in the items: A1) says while (17) and the proof of Lemma 2 use , and is used; Proposition 3 is stated for a cost that is finite everywhere, the setting of §3, because for a cost that is infinite on part of the space the interior condition on does not imply the Slater condition used in App. B; Lemmas 2 and 3 state the standing assumptions A1), A3) and i.i.d. sampling that their statements leave implicit. The localized weak limit (45) is not a milestone: its penalty depends on a -dependent near-optimal direction that is not stated precisely enough on the page.
Needed infrastructure: the multivariate central limit theorem (Mathlib has the real-valued one), Hölder duality for PiLp norms, a strong-duality theorem for moment problems (Proposition 7, quoted from Isii and Karlin–Studden), and a uniform law of large numbers. The duality results and the conjugate formula (42) are reusable beyond this mission. Proofs of any milestone, and lemmas that serve them, are welcome.
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.Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's earlier values ( down to ) came from Schnirelmann's method with every constant written out, using only weak Chebyshev lower bounds for . This entry keeps the same machinery as the entry but feeds it Chebyshev's sharper lower bound with , obtained from the weights at . No zeta-zero input is used.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in.
Let and . We show , then conclude with Mann's theorem as in the entry. Write for the scale.
PrimeNumberTheoremAnd library with explicit bounds for and ). Since , this gives . On its own it covers through .The argument stays elementary: no prime number theorem and no zeros of or -functions. New reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Already proved on the platform: Schnir.sieve_ineq, Schnir.G_lower, Schnir.basis_of_density. Mathlib supplies the Chebyshev function with and the Λ² sieve framework.
PrimeNumberTheoremAnd (PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean).In binary classification the VC dimension decides PAC learnability: a class of -valued functions is learnable from finitely many examples exactly when its VC dimension is finite. Multiclass classification, where a predictor outputs one of many labels, arises whenever the label set is large: language models choosing a next token, image recognition over open vocabularies, structured prediction. For finitely many labels the Natarajan dimension plays the role of the VC dimension (Natarajan 1989; Ben-David, Cesa-Bianchi, Haussler and Long 1995). Whether it still characterizes learnability when the label set is infinite stayed open for three decades.
Brukhim, Carmon, Dinur, Moran and Yehudayoff (arXiv:2203.01550, FOCS 2022) settled both directions. Their Theorem A shows that the DS dimension of Daniely and Shalev-Shwartz (COLT 2014, PMLR 35) characterizes multiclass PAC learnability for every label set. Their Theorem 2, the goal of this mission, shows that the Natarajan dimension does not: there is a class whose Natarajan dimension is and whose DS dimension is infinite.
Timeline:
A concept class is a set of functions from a domain to a label set , with no finiteness assumption on either. For a sequence , the projection is the set of words , .
Every Boolean cube is a pseudo-cube, so . The hexagon is a 2-dimensional pseudo-cube that contains no Boolean square.
The milestones pass through simplicial complexes: downward-closed families of finite sets. A complex is good if it is finite, pure, has a proper coloring of its vertices with colors, and satisfies replacement (every vertex of every face can be exchanged for a new vertex). A good complex with coloring defines the class of its top faces, each written as the word listing its vertices by color. A square is a 4-cycle of distinct vertices in the 1-skeleton; it is empty if neither diagonal is an edge. The coset complex of subgroups of a group has the cosets as vertices and the sets of cosets with a common point as faces.
Theorem 2 shows that the classical generalization of the VC dimension to many labels is the wrong invariant once the label set is infinite: a class can contain no Boolean square at all and still be unlearnable, because it contains pseudo-cubes of every dimension. Combined with the necessity of finite DS dimension, it gives a class that is not PAC learnable although its Natarajan dimension is , and it identifies pseudo-cubes, not Boolean cubes, as the relevant combinatorial obstruction. It also links learning theory to a problem studied in geometric group theory, finite "flag-no-square" complexes.
The paper's proof is complete modulo Theorem 45, which it imports from Januszkiewicz–Świątkowski 2003. None of these results is formalized. A formalization would give machine-checked versions of the dictionary between concept classes and properly colored complexes (Propositions 42–44), of the coset-complex translation (Proposition 46), and of the final disjoint-union argument; Theorem 45 itself, which rests on Coxeter-group and topological arguments, is a separate and substantial formalization target.
Infinite complexes that are pure, properly colored, satisfy replacement and have no empty squares are easy to build: grow a tree of faces indefinitely. The definition of a pseudo-cube demands finiteness, and the difficulty is entirely there: one must "fold" such an infinite object into a finite one without creating an empty square. The obvious finite candidate, the group with its coordinate subgroups, produces the Boolean cube, whose complex is full of empty squares. Theorem 45 is the input that resolves this, and it is far beyond the rest of the argument.
All declarations live in the namespace MulticlassDS.NatGap.
Set (X → Y) with arbitrary types; is Fin n (0-based), and shattering is defined for sequences Fin n → X, as in the paper.ℕ∞-valued suprema, so "infinite DS dimension" is dsDim H = ⊤. An ℕ-valued supremum would silently return on an unbounded family and would trivialize the goal.Set (Finset V). The dimension is the predicate HasDim C d, not a natural-number subtraction, and colors are Fin (d + 1).Welcome contributions: proofs of Propositions 42–44 and 46 and of the goal from the milestones, which need only finite combinatorics and elementary group theory; and, separately, a formalization of the Januszkiewicz–Świątkowski construction behind Theorem 45. The definitions of pseudo-cubes, the DS dimension and good complexes are reusable by the companion mission on sample compression and by any later work on multiclass learnability.
Controlled Markov processes with the average cost criterion model systems that run indefinitely, such as queues, inventories, maintenance and communication networks, where only the long-run cost per unit time matters. The standard route to an optimal stationary policy goes through the average cost optimality equation (ACOE). The ACOE is usually obtained by the vanishing discount method: solve the discounted problem for each discount factor and let . The method works only when the differences of discounted values stay bounded as . Conditions that guarantee this are therefore central in the survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993), §5).
This mission formalizes one such condition, due to Ross: if the mean return time to a fixed state is bounded uniformly over all stationary policies and initial states, the differential discounted value functions are bounded uniformly in the discount factor and the state.
Timeline. Derman (Management Sci. 9 (1962); survey reference [38]) and Derman–Veinott (Ann. Math. Statist. 38 (1967); survey reference [43]) introduced recurrence conditions of this kind for countable-state processes. Ross (Ann. Math. Statist. 39 (1968), survey reference [147]; Introduction to Stochastic Dynamic Programming, 1983, survey reference [150]) showed, for bounded costs, that under a Derman–Veinott type recurrence condition is bounded uniformly in , and obtained a bounded solution of the ACOE by letting (survey, pp. 291 and 301). Later work replaced the condition with weaker ones (survey Assumptions 5.1–5.3) and with Sennott's conditions (survey Theorem 5.9).
The state space is . In each state , an action is chosen from a nonempty compact set of a metric space . The one-stage cost is nonnegative and the next state is drawn from the transition law . For fixed , the maps and are continuous on . A policy chooses the action at time at random, given the whole history, and must choose from . A stationary deterministic policy is a map with . and denote the law and the expectation of the controlled process started at .
For a discount factor , the discounted cost and the optimal discounted cost are
A policy is -discount optimal if for all . The differential discounted value function is
measured relative to the fixed state . The return time to is
with if the process never returns. Throughout, as in §5.1 of the survey, the cost is bounded: on admissible pairs.
If there is a constant with
then there is a constant such that
This is the theorem as printed: it asserts only uniform boundedness and fixes no constant.
The result. Theorem 5.3 verifies the hypothesis of the vanishing discount theorem (Theorem 5.2 of the survey) from a condition on the uncontrolled dynamics of stationary policies. Theorem 5.2 then gives a bounded solution of the ACOE, an average optimal stationary policy, and the limit . Mean return times can often be estimated directly, for instance through Foster–Lyapunov drift arguments on queues, which makes (5.7) checkable in applications. The explicit bound also controls the span of the relative value function.
Formalizing it. The result is proved in the literature; to our knowledge it has not been machine-checked. A formal proof needs discounted dynamic programming on a countable state space with compact action sets, the existence of optimal stationary policies (Theorem 2.1 (iii), which the survey cites without proof), and the strong Markov property of the controlled chain at a return time. All of these are reusable well beyond this mission.
The estimates (5.9) and (5.10) are elementary once (5.8) and the existence of are available. The weight lies elsewhere.
ℕ; the action space is a metric space with its Borel -algebra. The model CMP carries compact nonempty , a nonnegative measurable cost, and continuity of and on , the standing assumptions of §5.Kernel.trajMeasure. is an infimum over all such policies, not over Markov or stationary policies only.trajMeasure, and return-time estimates.The problem asks for a single-machine sequence of jobs, respecting precedence constraints, that minimizes the weighted sum of completion times. It has been known to be strongly NP-hard since Lawler (1978) and Lenstra and Rinnooy Kan (1978), several different 2-approximation algorithms are known, and closing the approximability gap is listed by Schuurman and Woeginger (1999) as one of ten outstanding open problems in scheduling theory. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) give the first inapproximability result for this problem: under a widely believed complexity assumption it has no polynomial-time approximation scheme (PTAS). The bridge to that result is a quantitative link, Lemma 9.1, between the optimal value of a special bipartite scheduling instance and the maximum edge biclique of a bipartite graph, a problem whose hardness of approximation was established by Ambühl, Mastrolilli and Svensson (FOCS 2007). This mission formalizes that link.
A schedule of a finite job set is a sequence listing every job once; the machine processes the jobs in that order from time without idle time or pre-emption. Job has a processing time and a weight ; its completion time is the sum of the processing times of the jobs up to and including , and the value of is . Precedence constraints are a relation on jobs: with means job must be completed before job starts. A schedule respecting all of them is feasible, and a feasible schedule of least value is optimal.
Let be an -by- bipartite graph: and . An edge biclique is a pair , with , of value ; the maximum edge biclique problem (Definition 9.1) asks for one of largest value. The bipartite scheduling instance has jobs and precedence constraints
so must precede exactly when is not an edge. Jobs of have , ; jobs of have , . Thus , where is the number of -jobs scheduled before . For , denotes the number of -jobs scheduled before jobs of have been scheduled.
In the Lean development these are weightedCompletion, IsOptimalSchedule, IsEdgeBiclique, maxBicliqueValue, precSG, procSG, weightSG, valSG, IsOptimalSG and vBefore in the namespace SingleMachinePrec.Biclique.
If a maximum edge biclique of has value with , then has an optimal schedule and every optimal schedule satisfies
Lemma 9.1 shows that the optimal value of determines the maximum edge biclique of up to a factor of order in the "area above the work line" . Combined with the hardness of approximating maximum edge biclique (Theorem 9.1, cited from Ambühl, Mastrolilli and Svensson 2007) it yields Theorem 9.2: has no PTAS unless SAT can be decided by a probabilistic algorithm in time for every . It also makes precise the two-dimensional Gantt chart picture of Eastman, Even and Isaacs (1964) and of Goemans and Williamson (2000), in which every point on the work line of a schedule defines an edge biclique.
The lemma is proved in the paper; it is not formalized anywhere to our knowledge. A formal proof certifies the combinatorial core of the no-PTAS result independently of the complexity-theoretic layer, and its definitions (the bipartite instance , edge bicliques, the profile ) are reusable for the gap inequality behind Theorem 9.2.
The upper bound is a direct computation on one explicit schedule. The lower bound is a statement about every feasible schedule, of which there are exponentially many, and it must hold with the explicit constant and the factor for every . The printed argument splits the sum at and uses , treating as an integer; for general (for example , value , ) the split point is not an integer, so the printed estimate does not apply verbatim and the constant has to be re-checked for non-integral . On the formal side, the value identity requires relating completion times in a list to counting -jobs before each -job, with ties among zero-length jobs.
Jobs are the disjoint union U ⊕ V of two finite types with Fintype.card U = Fintype.card V = n; is a relation U → V → Prop. A schedule is a duplicate-free list containing every job; feasibility is the published LawlerPrec.MinMax.IsFeasible and completion times are the published MooreLateJobs.Shared.completionTime (time start, no idle time). Processing times and weights are reals, here in . The maximum edge biclique value is the maximum of over all edge bicliques, the empty ones included, so the hypothesis means . The logarithm is natural (Real.log).
Conventions and readings committed to:
Not formalized: Theorem 9.1 (cited hardness of maximum edge biclique) and Theorem 9.2 (no PTAS under a complexity assumption); no polynomial-time or complexity-theoretic statement appears in the mission. Contributions welcome: proofs of the three milestones and of the goal; Mathlib's bounds on harmonic numbers (Mathlib/NumberTheory/Harmonic/Bounds.lean) are the relevant library.
A controller acting over an indefinite horizon must decide whether a lower cost today is worth a higher cost later. Average cost measures the expected expenditure per stage as the horizon grows. It is appropriate when operation has no natural terminal date, but its limiting definition makes it difficult to compute an optimal policy directly. Discounted cost assigns less weight to distant stages and has a more direct optimality equation. Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus survey these criteria for controlled Markov processes and state a condition under which solving one discounted problem yields a solution to an average-cost problem (Arapostathis et al., 1993, §5.1).
The condition is a common lower bound on the one-step probability of moving to a distinguished state. Ross's reduction, reported as Theorem 5.6 of the survey, uses that bound to define a new transition law and a specific discount factor. The survey's theorem states the reduction informally; its proof specifies the transformed law, the optimality equation and the resulting average-cost policy. Those claims are the targets of this mission (Arapostathis et al., 1993, pp. 303–304).
The state space is . In state , the controller may choose an action from a nonempty compact set in a metric action space. Choosing incurs the one-stage cost and moves the state to with probability . The cost is measurable, and for each fixed its value and vary continuously with on . Section 5 imposes these state and continuity conventions; §5.1 additionally assumes the costs are bounded (Arapostathis et al., 1993, pp. 284–288, 299, 301).
An admissible policy chooses a probability law for the next action from the entire observed history, and assigns probability one to admissible actions. A stationary deterministic policy is a map with ; it always takes action in state . These are distinct classes. Let be expected cost over the first stages from , and let be expected cost when stage is weighted by , where . The average-cost criterion is . The optimal values and are infima over all admissible policies, including randomized and history-dependent ones (Arapostathis et al., 1993, pp. 285–287).
The average cost optimality equation, or ACOE, asks for a scalar and a real function such that, for each state ,
The minimum is attained. The survey's verification theorem identifies with the optimal average cost when the terminal contribution of vanishes after division by (Arapostathis et al., 1993, p. 299, (5.1), Theorem 5.1).
Assume that on every admissible state-action pair for a single constant . The transformed process has the same admissible actions and costs and has transition probabilities
Write for its discounted value at discount factor . The goal states that this value is finite, a stationary deterministic discounted-optimal policy exists, and every such policy is average-cost optimal for the original process. It also identifies a constant optimal average cost for every initial state:
The goal does not assume the average optimality that it asserts. It requires the transformed law to satisfy the displayed formula at every admissible state-action pair (Arapostathis et al., 1993, Theorem 5.6 and proof, pp. 303–304).
The milestones establish that the transformed law gives a controlled Markov process, that the discounted problem has an optimal stationary deterministic policy, and that the transformed discounted value satisfies the original ACOE with . The final milestone is the ACOE verification theorem needed to identify the average cost. The source gives the first two discounted claims through Theorem 2.1 and writes out the transformed equation in the proof of Theorem 5.6 (Arapostathis et al., 1993, pp. 289, 299, 304).
The theorem replaces an average-cost optimization problem by one discounted problem with a prescribed discount factor and transition law. It yields a stationary deterministic policy that is optimal even when compared with every history-dependent randomized policy, and it shows that the optimal average cost is independent of the initial state. Without the common return probability, neither this particular law nor this fixed discount factor follows from the survey's argument (Arapostathis et al., 1993, Theorem 5.6).
The survey reports this as a known result of Ross rather than an open conjecture. The formalization work is to give the path measures, value functions, transformed process and verification result machine-checkable meanings. The Lean declarations here are open theorem statements awaiting proofs; compiling a statement with sorry does not establish the mathematical theorem. The policy and cost definitions can also support the other countable-state missions drawn from §5.
The transformed probabilities have to form a measurable stochastic kernel, preserve the action continuity assumptions and yield a controlled process with the original feasible actions and costs. The discounted value must be finite and uniformly bounded before its real form can enter the ACOE. A simple comparison of numerical optimal values is insufficient: a policy chosen in the transformed model must be shown optimal for the original model against the full policy class. The verification theorem also requires control of the terminal expectation of for arbitrary admissible policies, rather than only the stationary policies named in its printed condition (Arapostathis et al., 1993, pp. 299–300, 304).
Lean uses for the countable state space and Mathlib probability kernels for the transition and randomized decision rules. Strategic path measures are constructed from those kernels. Nonnegative expected costs and their infima live in , so an unbounded integral cannot silently become a finite real value. The transformed discounted value is converted to a real only in conclusions that also assert its finiteness. The ACOE uses real sums with explicit summability and an attained minimum. The model requires a Borel metric action space, nonempty compact action sets, measurable costs, and coordinatewise action continuity of the transition probabilities.
The source's §5.1 bounded-cost assumption is explicit in the goal and its discounted milestones. The displayed transformation needs ; the paper's theorem sentence gives only , so the case is excluded from this version. The paper prints (5.2) for stationary deterministic policies, but the proof uses it for all admissible policies to compare with ; the verification milestone takes the stronger, proof-supported hypothesis. Expectations in that condition are explicitly integrable. The converse part of Theorem 5.1 is not used and is outside this mission.
The transformed process is represented by another CMP constrained to have exactly the source's action sets, admissible costs and transition formula. A milestone poses its existence. This representation keeps the definition layer free of an unproved stochastic-kernel construction. The discount-optimal policy conclusion ranges over every stationary deterministic policy attaining the transformed discounted value, while the values themselves take infima over all admissible policies. Definitions of admissible path laws and the verification theorem are reusable contributions; proofs of the transformed kernel, stationary discounted existence and ACOE identity are welcome.
In the single-machine scheduling problem , a set of jobs, each with a processing time and a weight , is processed on one machine without interruption, subject to precedence constraints given by a partial order on . The aim is to minimize the weighted sum of completion times . The problem is strongly NP-hard for general precedence constraints (Lawler 1978; Lenstra and Rinnooy Kan 1978), and its approximability was a recurring open question in scheduling theory (Schuurman and Woeginger 1999).
A line of work by Chudak and Hochbaum, Correa and Schulz, and Ambühl and Mastrolilli showed that the problem is a special case of minimum weighted vertex cover in a graph built from the instance. Many problems on partial orders become polynomial when the order is an interval order, so it is natural to ask whether this one does too. Section 7 of Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 2011) answers no: the problem stays NP-hard on interval orders. The proof is a reduction from vertex cover in connected graphs of maximum degree 3. This mission formalizes the correctness of that reduction.
A poset is read as a reflexive relation: means . Jobs are incomparable if neither nor is in , and is the set of ordered incomparable pairs. The vertex cover graph has one node for each incomparable pair, weighted . Two nodes and are adjacent if and , or and , or and . Write for the minimum weight of a vertex cover of .
A poset is an interval order if each element can be assigned a closed real interval such that if and only if .
The reduction starts from a graph with vertices and a spanning tree rooted at , numbered so that each parent comes before its children. The paper uses a breadth-first search tree.
For every connected graph of maximum degree at most , every parent-first spanning tree and every , the precedence constraints of form an interval order, and
The result. Interval orders are a standard tractable class: several scheduling and order-theoretic problems that are hard in general become polynomial on them (Papadimitriou and Yannakakis 1979). Theorem 7.1 puts outside this pattern. Section 6 of the same paper shows that the problem nonetheless has a -approximation on interval orders, so hardness and approximability are separated on this class. The paper also remarks that the proof makes weighted vertex cover NP-hard to approximate within some factor on the graphs arising from interval orders.
Formalizing it. The theorem is proved in the paper. Nothing in this mission is open, and none of it has been machine-checked before. The work splits into the following parts:
The definitions of and of minimum-weight vertex covers are shared with the other missions of this series.
The construction is explicit, and each step is elementary. The work is in the bookkeeping. Claim 2 requires classifying every incomparable pair of jobs, including pairs of different kinds such as , by comparing ceilings of interval endpoints. Half-integer endpoints (, ) are exactly what separates weight-one pairs from comparable ones. Claim 3 requires checking adjacency in for all pairs of nodes of in both directions. The paper writes out two cases in each direction and calls the rest similar.
Claim 1 has a direction that is not simply local. A vertex cover of that misses both endpoints of a non-tree edge has to be repaired by swapping gadget vertices, and the repair must be repeated without increasing the size.
A natural first idea is to treat the light nodes (weight at most ) as negligible one at a time. This does not suffice: the argument needs their total weight to stay below , which is what forces to grow with .
SimpleGraph (Fin N); vertex is i, and the root is index 0. The tree is a TreeLayout: a parent function returning none exactly at the root, with each parent of smaller index and adjacent in . The statements hold for every such layout. This is stronger than the paper's breadth-first tree, and the proof uses only "parent before child".(G.neighborSet v).ncard ≤ 3) are kept as in the paper. They matter only for the NP-completeness of the source problem.PartialOrder instance: iff or . Processing times and weights are real numbers. Section 1 of the paper asks for nonnegative integers, but the instance uses and the formalization follows the instance as printed.SimpleGraph.vertexCoverNum. The floor is Nat.floor, which agrees with the integer floor because .The problem asks for an order in which to process jobs on one machine, respecting precedence constraints, so as to minimize the weighted sum of completion times. It is strongly NP-hard, and for decades the best approximation ratio known has been , achieved by several unrelated algorithms (LP relaxations, Sidney decompositions, primal–dual methods).
Correa and Schulz (2005) and Ambühl and Mastrolilli (2009) showed that the problem is a special case of weighted vertex cover: its objective splits into a fixed cost, the same for every feasible solution, and a variable cost, which equals the weight of a vertex cover in an auxiliary graph . Approximating vertex cover in within a factor therefore approximates the scheduling problem within . Uhan observed that the classical 2-approximations owe their guarantee to the fixed cost and can be arbitrarily bad on the variable cost alone.
Section 8 of Ambühl, Mastrolilli, Mutsanas and Svensson, Math. Oper. Res. 36(4) (2011) (DOI), proves the converse: approximating the variable cost is as hard as approximating vertex cover itself. A better-than-2 algorithm for must therefore either exploit the fixed cost or improve on the best known approximation for vertex cover, a long-standing open question.
Scheduling instance. A finite set of jobs, a partial order (reflexive; , , means precedes ), processing times and weights .
Incomparable pairs. Jobs are incomparable, , if neither nor lies in . The set consists of the ordered pairs with .
The vertex cover graph . One node per incomparable pair , of weight . Distinct nodes and are adjacent when, in one of the two orders, and , or and , or . For a set of nodes, ; for a vertex cover this is the variable cost, and is its minimum over all vertex covers.
The instance . Given a graph with and , the instance has jobs (processing time , weight ) and (processing time , weight ), and precedence constraints and for each edge , plus for all . The nodes of have weight and are called heavy; all others are light. For a set of nodes, . The vertex cover number of is .
For every graph on vertices, every , and every with : if is a vertex cover of for with , then is a vertex cover of ,
and, when ,
The paper words the theorem as "approximating the variable cost of is as hard as approximating vertex cover"; the statement above is the mathematical content its proof establishes.
The result. Theorem 8.1 is one half of an equivalence: by Theorem 2.1 (Correa–Schulz, Ambühl–Mastrolilli), minimizing the variable cost is a special case of weighted vertex cover; by Theorem 8.1, it is also as hard to approximate. Any hardness of approximation for vertex cover (NP-hardness of factor by Dinur and Safra; factor under the unique games conjecture by Khot and Regev) transfers to the variable cost. It also explains why the known 2-approximations must rely on the fixed cost, and it frames the later result of Bansal and Khot that the full objective is hard to approximate within under a variant of the unique games conjecture.
Formalizing it. The theorem is proved in the paper; no machine-checked version exists. The mission produces a checked account of the reduction: the vertex cover graph of an arbitrary precedence-constrained instance, the adjacency-poset instance built from a graph, and the quantitative transfer of approximation ratios. The definition of is shared with the other missions of this series.
The construction is short; the care is in the bookkeeping. One must check that the precedence relation is a partial order, determine exactly which ordered pairs are incomparable, verify that two heavy nodes are adjacent only through the third clause of the adjacency rule and only when the corresponding vertices are adjacent in , and bound the weights of all remaining nodes, including the many nodes of weight . The transfer then compares an approximate cover of with an optimal one whose heavy part comes from an optimal cover of ; the additive error must be converted into a multiplicative one, which requires .
A first reading of the page suggests that has at most nodes; it does not. The pairs and with are incomparable nodes of weight , so there can be up to nodes. Only nodes of positive weight are few.
P : N → N → Prop. Processing times and weights are nonnegative reals. The vertex cover graph is a SimpleGraph on the subtype of incomparable ordered pairs, using the symmetric closure of the printed adjacency rule without loops. Vertex covers are Mathlib's SimpleGraph.IsVertexCover; is Mathlib's vertexCoverNum, finite for a finite graph and converted with toNat; is a minimum over finite vertex covers.SimpleGraph (Fin n); i : Fin n stands for , so exponents are and the order is that of Fin n. Jobs are Fin n ⊕ Fin n ( left, right). The parameter is in .Most stochastic programs of practical size, such as two-stage recourse models in energy, finance or supply-chain planning, cannot be solved exactly: the expectation in the objective is a high-dimensional integral. The standard remedy is sample average approximation (SAA): replace the expectation by an average over a Monte Carlo sample and solve the resulting deterministic problem. This produces a candidate solution but says nothing about how good it is. A decision maker needs a statistical certificate: an interval that contains the candidate's optimality gap with a prescribed probability.
Mak, Morton and Wood (Oper. Res. Lett. 24, 1999) built such a certificate from independent SAA replications, which requires solving at least 30 optimization problems. Bayraksan and Morton (preprint January 2005, published in Math. Program. 108, 2006) showed that a single replication suffices asymptotically, and gave two variants that use two replications. This mission formalizes their validity theorems.
Let be a random vector with distribution on a measurable space , let be a set of decisions, and let be a cost. The stochastic program is
Its optimal set is , and the optimality gap of a candidate is . The paper assumes throughout:
Let be i.i.d. copies of , and write . The SAA problem is (SP), with an optimal solution . The gap estimator is (display (2)), and the sample variance of the differences is
with population counterpart . Finally is defined by .
The single replication procedure (SRP) solves (SP) once and reports the one-sided interval (display (5)). The I2RP takes the variance from a second, independent sample and its own minimizer . The A2RP runs the SRP on both halves of a sample of size , averages the gaps and the variances as in (10), and scales by .
Under (A1)–(A3), for and , provided or (see Formalization scope),
The milestones follow the paper's own proof:
Theorem 3 (p. 9) and Theorem 4 (p. 10) are the same coverage statement for the I2RP and the A2RP. Three further statements are included: the negative bias of display (1), the pathwise bound for , and the consistency of the pooled variance.
Theorem 2 makes a single SAA solve enough for an asymptotically valid upper confidence bound on the optimality gap. It cuts the computational cost of the multiple-replication procedure by a factor of about thirty, and it needs no asymptotic normality of , which typically fails when (SP) has several optimal solutions. The two-replication variants lessen the small-sample under-coverage of the SRP. The single- and two-replication estimators were later reused in sequential sampling procedures for SAA.
As far as is known, none of these results has been machine-checked. A complete formalization needs a uniform strong law of large numbers over a compact parameter set, which is a reusable result in its own right, together with the SAA consistency theory and a central-limit argument for a statistic that is not itself asymptotically normal.
The obvious route would be to show that is asymptotically normal and apply a standard confidence-interval argument. That fails: is a minimum of sample averages, and when is not a singleton its limit law is the law of a minimum of correlated Gaussians, not a Gaussian. The paper's argument has to bound the coverage from below without that limit law. It also needs to control the sample variance at a random, non-convergent minimizer , which only accumulates on . The uniform strong law (Rubinstein–Shapiro, Lemma A1) on which both consistency statements rest is not in Mathlib.
The Lean development uses these conventions:
EuclideanSpace ℝ (Fin d). The paper's is renamed because is the sample size.ξ : ℕ → Ω → Ξ on a probability space , 0-based: is ξ (i-1). The second sample of Theorems 3–4 is ξ n, …, ξ (2n-1), exactly as printed, and the A2RP's "random" partition is this fixed one, which has the same joint law.ℝ≥0∞-valued, so the liminf in (6) is genuine. Proposition 1 (iii) is stated in its equivalent -form, which avoids real liminf/limsup junk values.cdf (gaussianReal 0 1) zα = 1 - α.Standing assumptions and pins. Every goal-level statement carries (A1)–(A3) and the i.i.d. hypothesis. Three hypotheses are made explicit that the paper leaves implicit:
At the factors , and evaluate to Lean's ; every coverage statement is a liminf and ignores them.
Several encodings would trivialize the statement, and all are ruled out. The minimizer must minimize the SAA problem of its own sample: a free , or one fitted to the other sample, would change the theorem. The second sample must not be replaced by an independent sequence. The quantile must not be pinned through an sInf. Positivity of is a hypothesis only of the -bound, as on p. 8.
One correction of the paper. Theorems 2 and 4 are stated for every , but for the paper's argument (replace by ) needs , and without it both statements are false: for , , , and , the SRP coverage tends to about and the A2RP coverage to , both below . The Lean goal and Theorem 4 therefore carry the hypothesis ", or for some ". Theorem 3 is stated as printed.
Contributions are welcome at every level. The most reusable one is the uniform strong law of large numbers for Carathéodory integrands on a compact set with an integrable envelope, which also serves other SAA consistency results.
Large call centers route several types of customers to a common pool of agents. When the pool is large and highly utilized, the relevant asymptotic regime is the quality-and-efficiency-driven (QED) or Halfin–Whitt regime (Halfin & Whitt 1981). The number of servers grows while the offered load stays within of . Waiting is then neither negligible nor overwhelming (Gans, Koole & Mandelbaum 2003).
Which class should a freed agent serve next? Exact optimization of a multi-class many-server queue with abandonment is intractable. The standard route is to solve a limiting diffusion control problem and translate its optimal control back into a policy for the queue. Atar, Mandelbaum and Reiman (Ann. Appl. Probab. 2004) carried this out for customer classes, exponential service and abandonment, general renewal arrivals and general convex-type holding costs. They proved that the translated policy is asymptotically optimal. This mission formalizes that result for the preemptive policy.
Context:
There are customer classes and identical servers.
Primitives.
State. is the number of class- customers in the system, the number in service and the number waiting. The dynamics are
Policies.
Scaling and cost. In the QED scaling with . With the centred processes are , and . The cost is
The limiting control problem. It controls
where the control takes values in the simplex and is a -dimensional Brownian motion. The data are and . Its value is the infimum of , with .
HJB equation and the proposed policy. The HJB equation is with . Let be a measurable selection of its minimizers. The proposed preemptive policy (P-SCP) sets the queue vector to , an integer rounding, and falls back to a static priority rule when that is infeasible.
For a solution of the HJB equation, a measurable minimizer selection , and initial states with :
This holds for every sequence of work-conserving admissible SCPs, and the left-hand limit exists and is finite. No constants are hard-coded.
The milestones follow the proof:
The result. Theorem 2(i) justifies using the diffusion control problem as a design tool for multi-class many-server systems. The policy is explicit given , and it is optimal in the limit against all non-anticipating work-conserving policies, including those that use the full history and the time of the next arrival. The proof also identifies the limit cost with .
Formalizing it. The result is proved on paper, with some steps (Proposition 1, the principle of optimality, the time-change and martingale limit theorems) given as sketches or citations. No part of it is machine-checked. A formalization requires:
Each of these is reusable well beyond this paper.
The obvious argument would show that converges to the controlled diffusion and pass the costs to the limit. This fails for two reasons:
The proof instead compares every policy with the HJB solution through Itô's formula on the prelimit processes. This needs:
Existence of a classical HJB solution on all of , with only Hölder-continuous costs and polynomial growth, rests on a bounded-domain existence theorem for fully nonlinear elliptic equations.
The Lean development commits to the following conventions.
Fin k with ; paper class is index , so "class " (highest priority, rounding remainder of ) is the last index. Vectors are Fin k → ℝ and is the paper's norm; the paper's on vectors is read the same way.Ω : Type (universe 0). "Complete filtered probability space" means complete with all null sets in . Brownian motion is Mathlib's IsBrownianReal per coordinate, with independence and the -Brownian property stated explicitly. is the infimum over systems and their controlled processes.CouplingConverges of the published BellWilliams2001.ThresholdPolicy.Paths; convergence to a deterministic limit is UocInProb.The goal hypothesizes and with the pointwise identity for all . An arbitrary "optimal Markov control policy" may differ from a minimizer selection on the Lebesgue-null lattice where lives, and that formalization would make the goal false. Restricting the comparators to feedback, Markov or nonpreemptive policies, fixing , dropping abandonment, specializing to Poisson arrivals or linear costs, or imposing a common initial split would each trivialize or weaken the statement and is ruled out.
Not formalized:
Contributions are welcome on any milestone, and especially on infrastructure: Poisson and renewal processes, functional central limit theorems in Skorokhod space, classical solvability of elliptic HJB equations, and measurable selection of minimizers.
Distribution systems often move stock in two stages. A depot orders from an outside supplier and ships to a retail outlet, where customer demand arrives and unmet demand is backordered. Stock held anywhere costs money, a shortage at the outlet costs more, and each order carries a fixed charge. The basic question is what ordering and shipping rule minimizes total cost.
Clark and Scarf (Management Science 6, 1960) showed that over a finite planning horizon this two-echelon problem decomposes. The outlet solves its own single-location problem, and the depot solves a second single-location problem in which the outlet's shortfall is charged through an induced penalty cost. Federgruen and Zipkin (Operations Research 32(4), 1984) carried the decomposition to the infinite horizon. In the infinite-horizon problems the induced penalty becomes stationary and explicit, which makes the system computable with single-location tools. This mission covers the discounted-cost half of that paper (§§1–2).
Timeline:
Time is discrete. The cost data are a fixed order cost , an order cost rate , a shipment cost rate , a holding cost rate on all system stock, an extra holding cost rate at the outlet, and a backorder penalty rate ; all are positive. The discount factor satisfies , shipments take periods and orders take periods. One-period demands are independent copies of a nonnegative continuous random variable with mean , and denotes the sum of copies.
The state is :
An action is an order and a shipment with . With demand , the next state is . The one-period cost is
where for , , and
is the expected total discounted cost of a policy from state .
The critical number minimizes . The stationary induced penalty is for and otherwise. The depot problem has state , action and one-period cost . The policy orders by an optimal stationary policy of and ships : up to the critical number when the depot has the stock, otherwise as much as it has.
Assume . For every state with and , and every admissible policy ,
The goal leaves the form of open: any optimal stationary depot policy will do, and no structure is assumed.
The milestones follow the paper's own route. Write , , , for the -period optimal costs of the system, of the outlet, of the depot with penalties , and of the depot with penalty .
The theorem shows that, under discounting, the infinite-horizon two-echelon problem is solved by two single-location problems, with a penalty that is written in terms of alone. Computing does not require the outlet's optimal cost functions. The rest of the paper relies on this: its computational sections evaluate in closed form for normal demand, and they treat several outlets by relaxation. A machine-checked version also gives an infinite-horizon decomposition theorem against which future multi-echelon formalizations can be checked.
The result was proved in 1984 and is not open. It has not been formalized. The paper's proof is short only because it cites Iglehart's convergence results and Propositions 9.12 and 9.16 of Bertsekas and Shreve (1978) for its last step, so a formal proof must also supply these.
The obvious argument passes to the limit in the finite-horizon decomposition (4). That fails as stated, because the depot program (3) has nonstationary penalties , built from the outlet's optimal costs , and its value functions are not those of any stationary problem. The comparison of with needs uniform control over the whole real line. The first few are in fact unbounded, since has the wrong slope. The uniform control therefore holds only for large , and the error has to be propagated through the depot recursion.
The second obstacle is that the one-period costs are unbounded in both directions: is negative for negative . Contraction arguments for bounded costs therefore do not apply. Lower boundedness on the feasible set needs the cost relation , and passing from the optimality equation to optimality of a policy needs the theory of models with costs bounded below.
Everything lives in the namespace FZEchelon.Discounted.
Model. The pipeline is a vector indexed by , whose index is the paper's . For the current order arrives at once.StandingAssumptions: positive costs, , demand nonnegative, atomless and of finite mean. The §2 statements add and the cost relation, which the paper names in the proof of Theorem 1. The critical numbers and enter as minimizers. The depot policy enters as a measurable, nonnegative stationary policy that is optimal for ; that is the paper's definition of , and its existence is Iglehart's.Many supply chains move stock through a central warehouse to the retail locations that face customer demand. Deciding how much the warehouse should order from outside, and how much it should ship to each retailer and when, is a stochastic dynamic program whose state contains every stock level and every outstanding order. Exact solution is out of reach except for the smallest systems, so structural results that reduce such a problem to single-location problems matter in practice.
Timeline.
Time is divided into periods. A depot orders from an outside supplier with lead time and supplies a retail outlet with shipment lead time . The demand in each period is a nonnegative random variable with law and finite mean ; demands in different periods are independent and identically distributed. Unmet demand at the outlet is backordered.
The state is :
In each period the decision is an order and a shipment with , where is the order arriving now. The state then moves to .
Costs are a fixed order cost , proportional order and shipment rates and , a holding rate on system inventory, an extra holding rate at the outlet and a backorder penalty rate . After the paper's accounting transformation, the one-period cost is
with for and , , and, at ,
where is the demand over periods. The critical number is a minimizer of . The stationary induced penalty is for and otherwise.
For a policy and initial state , is the expected cost of the first periods and is the average cost. Problem IH asks for a policy minimizing from every state. The depot problem IH has states , orders and one-period cost . Its minimal average cost is . The outlet problem has states , shipments and one-period cost . The policy orders by an optimal stationary policy of IH and ships : up to the critical number if the depot has the stock, otherwise as much as it has.
With and , the policy is measurable and feasible from every physical state, and for every such state and every measurable feasible policy ,
The result. Theorem 2 reduces an average-cost problem with a multidimensional state to two problems with smaller states: a single-location -type problem for the depot with a known convex penalty , and a myopic critical-number rule for the outlet. The optimal system cost is the sum of their optimal costs. The paper uses this to compute optimal policies with standard single-location software, and its §5 builds heuristics for several outlets on the same decomposition.
Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of it has been machine-checked. A formal proof has to make precise what the paper leaves to "standard arguments":
The obvious argument would identify the average-cost optimal value through an average-cost optimality equation on the full state space and verify that attains it. No such equation is available here. The state space is unbounded, the one-period costs are unbounded both above and below in the state, and the depot's fixed cost makes its value functions -convex rather than convex.
The paper's route avoids that equation but needs three separate facts: