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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Gradient descent goes back to Cauchy (1847). It is the simplest method for minimizing a differentiable function, and most of the first-order methods in large-scale optimization and machine learning are variants of it. Its appeal in high dimension is that its oracle complexity, the number of gradient evaluations needed to reach a given accuracy, can be bounded independently of the dimension. For a merely Lipschitz convex function the projected subgradient method needs on the order of steps to reach accuracy (Theorem 3.2 of the book). Under a smoothness assumption gradient descent does much better, because the gradients shrink near the optimum and the steps adapt automatically.
This mission formalizes the basic result of that kind: Theorem 3.3 of S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015; arXiv:1405.4980v2). It states that gradient descent with step size on a convex -smooth function on has optimality gap after steps. The result and its proof are standard; versions appear in Nesterov's Introductory Lectures on Convex Optimization (2004, §2.1.5). It is the fourth mission in a series that formalizes the capstone results of Bubeck's monograph.
Write for Euclidean space with inner product and norm . Let be differentiable with gradient .
The optimality gaps are .
If is convex and -smooth with , is a minimizer, and is gradient descent with , then for every
These are the statements the book's proof uses, in the book's order:
Under the same hypotheses, for every .
Theorem 3.3 is the reference rate for first-order methods on smooth convex problems. Several later results in the book are measured against it. Nesterov's accelerated gradient descent (§3.7) improves to , the lower bounds of §3.5 show that cannot be beaten by any black-box first-order method, and adding strong convexity (§3.4) upgrades to a linear rate. Its ingredients are reused throughout the book and the optimization literature: the descent lemma (Lemma 3.4), the one-step improvement (3.5) and co-coercivity (3.6). Co-coercivity is the finite-dimensional case of the Baillon–Haddad theorem.
The result is classical and fully proved on paper. To our knowledge Mathlib does not contain this rate for gradient descent on convex smooth functions, and no published Prove2Me theorem states it. The mission provides it, together with Lemma 3.4 and co-coercivity as reusable statements on EuclideanSpace ℝ (Fin n). These are the facts that later missions of the series on projected gradient descent, strong convexity and acceleration need. Formalizing the improved constant of footnote 4 is a welcome addition.
Two steps are not routine. The first is Lemma 3.4, where the book integrates the gradient along a segment. In Lean this needs a mean-value or fundamental-theorem-of-calculus argument for a function on a Euclidean space, together with a Cauchy–Schwarz estimate, and Mathlib's HasGradientAt interface has to be connected to one-variable derivatives along lines.
The second is the monotonicity of . The natural first attempt is to telescope the one-step improvement (3.5) together with the convexity bound . That gives a recursion involving , which is not controlled by without further work. Making the recursion uniform requires co-coercivity (3.6), which comes from Lemma 3.5. That lemma's hypothesis is the two-sided inequality (3.4), not smoothness directly. The final numerical step divides by the gaps , so zero gaps need separate handling.
EuclideanSpace ℝ (Fin n), and is ⟪x, y⟫_ℝ.∀ x, HasGradientAt f (g x) x.IsBetaSmooth f g β) is the book's definition: , the gradient-existence hypothesis, and the Lipschitz bound . The book's "continuously differentiable" follows from it.ConvexOn ℝ Set.univ f. A minimizer is a point xstar with ∀ y, f xstar ≤ f y; its existence is the book's standing assumption, and is derived, not assumed.IsGDRun g η x) is a sequence x : ℕ → ℝⁿ with and for every . The book's is x 1, and index is unused. Every theorem quantifies over all runs with .Disclosed side conditions:
A trivializing formalization is ruled out. Smoothness is the Lipschitz condition on the gradient, so Lemma 3.4 and (3.4) are not restatements of the definition, as they would be if the quadratic upper bound (3.4) were taken as the definition of smoothness. The run predicate also fixes the step size .
A complete development needs:
HasGradientAt functions;Lemma 3.4, Lemma 3.5 and (3.6) are reusable well beyond this mission. Proofs of any milestone are welcome independently.
Finding the quickest route between two points of a road network is among the oldest problems of operations research. It is the subproblem inside vehicle routing, network flow and many dynamic programs. Richard Bellman's four-page note On a routing problem (Quarterly of Applied Mathematics, 1958) treats it as a dynamic program. The minimal travel times satisfy a nonlinear system of equations, and that system can be solved by successive approximations that terminate after a number of steps bounded in advance. The iteration is now known as the Bellman–Ford method. A footnote added in proof records that Max Woodbury and George Dantzig had obtained the same scheme independently, and Ford's RAND report of 1956 describes a closely related labelling procedure.
Timeline.
There are cities, numbered . Every two of them are linked by a direct road, and city is the destination. The travel time from to is a real number ; the matrix need not be symmetric. Throughout, for .
A route from to is a sequence of cities in which consecutive cities differ. Its stops are , and its time is . The minimal time (3.1) is the least time of a route from to , and .
The routing equation (3.2) is the system
Approximation in policy space (§5) starts from the direct-route policy (5.2), , and iterates (5.1):
The second scheme (§7, (7.1)) starts instead from and uses the same step.
For every the following hold. Each is the minimal time from to , attained by a route. The vector solves (3.2). Every real solution of (3.2) equals :
This is the claim of the Summary ("converges after at most iterations") and of the last sentence of §5. The paper's bound is kept, although also suffices.
The result. The note turns an enumeration over exponentially many paths into rounds of minimisations each, with a bound fixed before the computation starts. The uniqueness theorem makes the routing equation a characterisation of the minimal times, not merely a property of them. This is the template for later correctness proofs of shortest-path and value-iteration algorithms. The monotone decrease (5.5) is the first instance of policy improvement: every iterate is the value of an actual routing policy.
Formalizing it. The results are classical and proved. What this mission adds is a machine-checked development against the paper's own objects. Routes, their times and minimal times are defined from scratch. The iteration is stated exactly as printed, apart from the corrected initial value at the destination. The (N − 1)-step termination is asserted as an equality, not a limit. Related platform items treat other methods and do not cover these statements. One is the label-correcting method (BertsekasDP.label_correcting_correctness_of_nonneg_arcs, BertsekasDP.label_correcting_terminates). Another is the stochastic shortest path problem under a termination assumption that fails for deterministic routing (BertsekasDP.ssp_main_theorem). There are also the generic candidate-list algorithm (BertsekasNetwork.generic_shortest_path_algorithm), Floyd's Algorithm 97 and Dijkstra's method.
The minimum in (3.2) may be attained at a whose own optimal route passes back through . The routing equation is a fixed-point equation for an operator that is monotone but not a contraction in any fixed norm. The standard contraction argument for discounted dynamic programs therefore does not apply. Uniqueness has to use to exclude zero-time cycles: with , the system (3.2) has infinitely many solutions. The bound depends on the at-most--stops reading of and on the fact that an optimal route never needs to revisit a city. Neither is visible from the recursion alone. For the scheme of §7, the page gives no bound on the number of iterations, and none holds uniformly in .
Cities are Fin (n + 1), so , with standing hypothesis . City is Fin.last n, and travel times are t : Fin (n + 1) → Fin (n + 1) → ℝ with for . Diagonal entries are unconstrained and never used. No symmetry, triangle inequality or integrality is assumed. A route is a list of cities with distinct consecutive entries ending at . Repeated cities are allowed; with positive times this changes no minimum. Minimal times are attained minima over routes (IsMinTime, IsMinTimeWithin), not real infima. The minimum in (3.2) is a Finset.inf' over all , the destination included.
The paper's loose phrases are made explicit as follows.
Two printed slips are corrected. (5.2) is printed for , which would set , and with statements (5.4), (5.5) and the goal would be false. The formalization uses , the value the paper's own justification needs. (7.1) prints "" for . Section 6 (computational aspects) and the closing expectation of §7 that the first method converges faster are not formalized.
The goal cannot be satisfied trivially. The minimal times are defined from routes, not as a solution of (3.2) or as a limit of the iteration, so the goal connects the recursion to the routing problem itself.
The development needs only finite minima, lists and induction; nothing beyond core Mathlib. The route and minimal-time layer is reusable for other deterministic shortest-path results. Proofs of any milestone are welcome, as are proofs of the sharper bound .
An airline sells the seats of one flight leg at several fares. Cheaper fares are booked earlier, so the airline must decide, while low-fare requests arrive, how many seats to hold back for later and more valuable passengers. In nested booking control a seat that could be sold at a low fare is always available to a higher fare. The airline therefore chooses protection levels: seats are reserved for the most expensive classes together, and a request of class is accepted only while more than seats remain.
For two classes the optimal protection level was found by Littlewood (1972): protect seats, where . For more classes the industry used the EMSRa heuristic of Belobaba (1987, 1989), which applies Littlewood's rule to each pair of classes separately and adds the results. Brumelle and McGill (1993) gave the exact optimality conditions for any number of nested classes and showed that EMSRa is in general not optimal. Their conditions are part of the standard theory of single-leg revenue management, as presented in Talluri and van Ryzin (2004).
There are fare classes , numbered from the highest fare. Class has fare and random demand . The standing assumptions (pp. 128–129) are: the demands are mutually independent random variables on a probability space , and the fares are strictly decreasing, . Demands arrive in order of increasing fare: all of class before any of class . There are no cancellations or no-shows, and the decision to close a class depends only on the number of current bookings.
A protection-level policy is a vector with ; the dummy . The revenue of the highest classes with seats available and demand vector is defined recursively by (8)–(9), p. 130:
The expected revenue is . A policy is optimal if for every policy , every and every .
For , and denote the right and left derivatives, and the subdifferential is the interval , with (p. 131).
If the protection levels satisfy
then is optimal.
Theorem 3 turns the optimal nested protection levels into a sequence of equations in the joint distribution of the cumulative demands . For it is Littlewood's rule. For it identifies exactly what EMSRa approximates: EMSRa replaces the joint event in (31) by separate pairwise comparisons, and the paper shows (§4) that EMSRa can both over- and underestimate the optimal protection levels. The conditions are also the input of numerical methods: given demand forecasts, the levels are found one after another by solving (31), and §3.3 notes that a continuous joint demand distribution guarantees a solution exists.
The results are proved in the paper. As far as is known they have no machine-checked proof. Related platform items cover the two-class, integer-seat case from Belobaba (1987) (SeatInventory.Nested.emsr_protection_level_optimal) and the integer marginal-seat-revenue analogue of (27). They use a different model: two classes, natural-number seats and first differences. This mission formalizes the multi-class statement with real-valued seats and one-sided derivatives. A sister mission of the series proves the existence of optimal integer policies for integer-valued demand (Theorem 2).
The expected revenue is not differentiable: for discrete demand it is piecewise linear, so first-order conditions must be stated with one-sided derivatives and subdifferentials. The natural approach, to optimize each protection level separately with the others fixed, fails without concavity, and concavity of in is not automatic. It holds only when the lower protection levels already satisfy the first-order conditions. Concavity and optimality must therefore be carried through one joint induction over the classes. Passing from (31) to (20) requires computing the right derivative of the expected revenue in closed form for every . This involves exchanging differentiation with expectation and conditioning on one class's demand at a time.
iIndepFun), strictly decreasing fares.HasDerivWithinAt on half-lines and must exist; derivWithin, which returns where no derivative exists, is not used. is encoded as a disjunct.The goal assumes only the standing assumptions, , and (31). It does not assume concavity, condition (20) or any derivative formula: those are milestones. A formalization that quantified optimality over one level, one value of , or policies differing from in one coordinate would be weaker than the paper and is excluded.
A complete development needs one-sided derivatives of integrals of piecewise-linear functions (dominated convergence for difference quotients), concavity of piecewise functions glued at points where the slopes decrease, and the independence calculus that turns into an iterated integral. These pieces are reusable for other newsvendor-type and revenue-management models. Proofs of any milestone, and alternative arguments for Theorem 1, are welcome.
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.
Many controlled queueing, inventory and maintenance systems are modelled as controlled Markov processes (CMPs) on a countable state space whose one-stage cost grows without bound: the holding cost of a queue grows with its length. For such systems the natural performance measure is the long-run average cost, and the basic question is whether some simple policy, one that looks only at the current state and never randomizes, is optimal among all policies, including those that use the whole history.
When the cost is bounded, the classical answer goes through a bounded solution of the average cost optimality equation (ACOE). For unbounded costs, bounded solutions are rare: in many queueing models the relative value function grows with the state, and growth conditions such as (5.2) of the survey may fail (Arapostathis et al. 1993, p. 307). Sennott (1986; 1989) replaced boundedness by one-sided conditions on the discounted value functions, which are often easy to verify for queueing models because the relative values are bounded below. This mission formalizes Sennott's existence theorem in the form given in the survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus, Theorem 5.9.
Timeline. For bounded costs, Ross (1983, the survey's Theorem 5.2) obtained a bounded ACOE solution, and with it an optimal stationary policy, when the differential discounted values are uniformly bounded. Federgruen, Hordijk and Tijms (1979) treated unbounded costs under Lyapunov-type recurrence conditions, which restrict how fast the cost may grow (survey, Remark 5.7). Sennott (1986, 1989) replaced these by a uniform lower bound and a pointwise, one-step integrable upper bound on the differential discounted values. The survey (1993, Theorem 5.9) states the result with compact action sets and continuous data, and Sennott's 1999 book (§7.2) gives the finite-action version in textbook form.
The state space is . For each state the set of admissible actions is a nonempty compact subset of a metric space . Choosing in state costs , and the next state is with probability . For fixed , the maps and are continuous on .
An admissible policy chooses the action at time according to a probability distribution concentrated on , where is the history; it may use the whole history and may randomize. A stationary deterministic policy is a map with , applied at every step. Given an initial state and a policy , the states and actions form a stochastic process with law and expectation .
For , the discounted cost and the average cost of from are
both in . The optimal values are and , and the differential discounted value is . A policy is AC-optimal if for every .
Sennott's conditions (Assumptions 5.14–5.16) are:
The goal asserts only existence. It does not fix the optimal cost, and it does not claim that the optimal cost is constant or that an optimality equation holds.
The result. Theorem 5.9 is the standard existence theorem for average-optimal stationary policies with unbounded costs on countable state spaces. Its conditions are verified routinely for controlled queues, where relative values are monotone in the queue length and hence bounded below. It shows that randomization and memory do not reduce the long-run average cost, and the ACOI it produces is the starting point for value and policy iteration and for structural results such as threshold policies.
Formalizing it. The theorem is proved in the literature (Sennott 1989; Sennott 1999, Theorem 7.2.3; survey, p. 308). It has no machine-checked proof. The finite-action version, SennottDP.SEN.thm_7_2_3_sen_acoi, is posed on Prove2Me and still open; this mission poses the compact-action version, which needs continuity and compactness arguments that the finite case avoids. A formal proof also requires a general theory of history-dependent policies on path space (Ionescu-Tulcea), the discounted optimality equation with unbounded costs, and the passage from Abel to Cesàro means. All three are reusable well beyond this paper.
The obvious argument lets in the discounted optimality equation (5.6). Two steps fail without more structure. First, need not converge, and with unbounded costs it is not uniformly bounded, so the limit has to be taken pointwise along a subsequence, with only a lower bound uniform in the state. Second, the limit cannot be passed through the infinite sum by dominated convergence, because no integrable dominating function exists for every action. Only an inequality survives (Fatou), so the limit is an ACOI, not an equation. The inequality then has to be turned into optimality against all of , which includes history-dependent randomized policies whose costs are not described by any optimality equation. The lower bound for these comes from comparing Cesàro and Abel means, not from dynamic programming.
The Lean development uses the following representation and conventions.
ℕ. The action space is a metric space with its Borel σ-algebra. U i is nonempty and compact, c is measurable and nonnegative on admissible pairs, P is a Markov kernel, and , are continuous on .limsup in .A trivializing formalization is excluded. Sennott's conditions are satisfiable (a one-action, zero-cost model satisfies all three), and AC-optimality is measured against all admissible policies, so the goal cannot hold vacuously or by a junk value.
Welcome contributions: the Markov property of the path measure for history-dependent policies; the discounted optimality equation for nonnegative unbounded costs; a measurable-selection or compactness argument for minimizing actions on compact ; Fatou's lemma for series with converging weights; and the Abelian inequalities in a form applied to expected costs.
In multiclass classification a learner sees examples with in a domain and a label in a set , and must predict labels of new points. When is finite, the Natarajan dimension characterizes PAC learnability, extending the role of the VC dimension in binary classification (Natarajan 1989; Ben-David, Cesa-Bianchi, Haussler, Long 1995). Label sets in practice are often unbounded: structured prediction, ranking, and language modelling all predict from very large or infinite label spaces. For infinite the Natarajan dimension fails to characterize learnability, and the question of which combinatorial parameter does was left open by Daniely and Shalev-Shwartz.
Timeline:
A concept class is a set of functions. For a sequence the projection is the set of label words , . A finite non-empty set is a pseudo-cube if every has, in every coordinate , a neighbour that differs from exactly in coordinate . The sequence is DS-shattered if contains an -dimensional pseudo-cube, and the DS dimension is the maximum length of a DS-shattered sequence. The Natarajan dimension is the same with Boolean cubes , , in place of pseudo-cubes.
A sample is -realizable if some is consistent with it. An sample compression scheme for (Littlestone and Warmuth 1986) is a single reconstruction function such that every realizable sample of size contains of its examples with consistent with the whole sample. Logarithms are base throughout.
For with and , and all integers , there is an sample compression scheme, , with
The scheme combines two components, each with its own chain of results:
Theorem 36 is the algorithmic heart of the characterization: by the standard "compression implies generalization" argument it gives PAC learnability of every class of finite DS dimension, with sample complexity in the realizable case (), and with the agnostic case following by known reductions. It also exhibits sample compression schemes of size polylogarithmic in for multiclass classes with infinitely many labels, in contrast to the constant-size schemes known for finite VC classes.
The result is proved in the paper; none of it is formalized. The formalization would produce a machine-checked theory of one-inclusion graphs and their orientations, multiclass shifting, the exponential dimension, list learning, and sample compression schemes for arbitrary label sets. These objects recur throughout learning theory (one-inclusion graphs in optimal PAC learning, shifting in VC theory), so the infrastructure is reusable beyond this mission.
The natural first idea, running empirical risk minimization or bounding the Natarajan dimension, fails: classes with Natarajan dimension and infinitely many labels can be unlearnable, and ERM can fail even for learnable classes. The DS dimension gives only a weak guarantee: by Claim 16, among leave-one-out runs, one is correct. Turning this into a learner requires a list learner whose menus are still of unbounded total size, and then learning with a menu of size , where the obstacle is controlling one-inclusion graph orientations over by the Natarajan dimension. Multiclass shifting does not preserve the average degree (Example 20), so the binary argument breaks down, and a new potential () and a new dimension () are needed. Lemma 13 for infinite classes needs a compactness argument.
Lean conventions:
H : Set (X → Y) with arbitrary types X, Y; sequences and samples are functions on Fin n ( is 0-based).ℕ∞, so unbounded families give ⊤; hypotheses are written dsDim H = dDS with dDS : ℕ. A pseudo-cube is required to be finite.Real.logb 2. Menu sizes use Set.encard.∃ ρ, ∀ S, ∃ S'); a subsample may repeat and reorder examples. Theorem 36 states explicitly.Fin p; the shifting condition becomes .PMF), and i.i.d. probabilities are sums over . The measure-theoretic generality of the paper is not attempted.A trivial formalization is ruled out by these choices. Placing the reconstruction function after the sample would let it output the consistent hypothesis. A dimension in ℕ defined by sSup would be for infinite dimension. Pseudo-cubes without finiteness would change the dimension (Example 8).
Contributions welcome: proofs of any milestone, in particular the shifting results of §3 (self-contained combinatorics on finite classes), Fact 14 (pure discrete probability), and Lemma 13; general-purpose lemmas about one-inclusion graphs, orientations and sample compression schemes are reusable by other learning-theory missions.
A seller with a fixed stock of a single product and a finite selling season must post prices without knowing how demand responds to price. Revenue management treats this as a constrained stochastic control problem; with the demand curve known, the problem was solved by Gallego and van Ryzin (Management Science, 1994). When the curve is unknown, every price posted also serves as an experiment, so the seller faces an exploration–exploitation trade-off. Unlike a multi-armed bandit, this problem has a continuum of actions and a hard inventory constraint.
Besbes and Zeevi (Operations Research, 2009) measure a pricing policy by its worst-case relative revenue loss against a full-information benchmark, in an asymptotic regime where inventory and demand grow together. They give three upper bounds. This mission takes the third, Proposition 5: when the demand model has a single unknown scalar parameter, a policy that keeps re-estimating that parameter in stages of growing length has regret . The paper's lower bound for parametric families (Proposition 4) is of order , so the rate is optimal up to logarithmic factors.
Market. Prices lie in with . Posting the off price stops demand. The seller starts with inventory and sells over the horizon , .
Demand. A demand function maps a price to a demand rate. The class consists of the functions that are non-increasing with an inverse on , have a concave revenue rate , are bounded by , are -Lipschitz with a -Lipschitz inverse, and attain a revenue rate . The parametric family is , , with every member in the class (Assumption 1). Assumption 2 adds a test price , differentiability of and the Lipschitz bound . Assumption 3 requires and an -Lipschitz solution map of the equation .
Demand process. Let be a unit-rate Poisson process. Under a price path and parameter , the cumulative demand up to time is . Sales stop when the inventory runs out.
Benchmark and regret. The deterministic relaxation is the supremum of over price paths with . In the market of size the inventory is and the demand . If is the expected revenue of a policy , its regret is .
Algorithm 3. Start from and use stages of lengths summing to . Stage applies , estimates the demand rate from the stage's demand, solves for , and sets . Here maximizes and minimizes . The tuning (19)–(20) is stages with and .
The constants are uniform in and . This is the paper's (21): .
Milestones 6–8 hold in the case , the only case the paper's proof treats in detail.
Proposition 5 shows that with one unknown parameter, learning while earning reaches the rate, up to logarithms. The learn-then-price policies of Propositions 1 and 3 stop learning after an initial phase and reach only and . The paper leaves open whether the multi-parameter case attains the lower bound.
The analysis combines a continuous-time controlled Poisson model, an inventory constraint and a staged estimator, which also appear in later work on dynamic pricing with learning. A formal development would provide a time-changed Poisson demand model with random stage boundaries, a deterministic-relaxation benchmark, and concentration bounds stated for the scales this literature uses.
The result is proved in the paper, but parts of the proof are only sketched. The case is dismissed with "a similar result holds". The per-stage gap is obtained "by parallel reasoning". Display (A-30) has a typographical error in its threshold. To our knowledge, none of these results has been machine-checked.
The naive argument conditions each stage on its start time, as if that time were deterministic. It is not: the stage boundaries depend on all earlier observations, so every per-stage estimate needs the strong Markov property of the Poisson process at a random time. The inventory constraint makes the revenue a nonlinear function of the whole demand path. Bounding the loss therefore means controlling estimation error and overflow at the same time. The geometric stage lengths (20) are chosen so that the stage losses are all of the same order. That balance has to be checked exactly, including the rounding of to an integer.
Function.invFunOn. is a nonempty closed interval of .Contributions are welcome on every milestone. The Poisson process structure, its strong Markov property at stage boundaries, and Lemma 2 can be reused in other Poisson-demand pricing and queueing missions. Lemma 1 and Fact 1 are deterministic, and the rate estimate already has a local proof.
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 seller with a fixed inventory must choose prices before knowing how customers respond to them. A price that earns a high margin can sell too slowly; a price that sells quickly can exhaust stock before the selling season ends. Learning demand uses time and inventory, so the seller must account for the cost of its own experiments. This mission formalizes the parametric policy and regret bound of Besbes and Zeevi (2009), Proposition 3. Their setting differs from a finite-arm bandit: the permitted ordinary prices form an interval, customer arrivals are random, and the available stock caps total sales.
The paper first analyzes a nonparametric class with a slower upper bound in Proposition 1, then imposes a known finite-dimensional form on the unknown demand curve in Section 5. Proposition 3 shows how that additional information improves the regret rate for its Algorithm 2. The authors also prove a lower bound for a suitable parametric family in Proposition 4; that result is outside this mission's capstone, which concerns the performance guarantee of the concrete policy.
The selling horizon has length , and the initial stock is . An ordinary price lies in , with . The special price stops demand. At parameter , the demand rate is . The parameter set is nonempty, compact, and convex; is positive. The seller knows the family but does not know the true parameter .
For each parameter, demand is nonincreasing in the price and has an inverse on the attainable rate interval. The rate revenue is , a concave function of the rate. Every member of the family satisfies Assumption 1 with the same positive constants : demand is at most , its price variation is at most times the price difference, its inverse is -Lipschitz, and some ordinary price earns revenue rate at least . These conditions define the class in which the bound is uniform. See §§3–4.2 of the source.
Customer requests follow a unit-rate Poisson process run on a demand-dependent clock. Under price , cumulative requests at time equal . The market of size has stock and rate . Sales stop when stock runs out. The deterministic relaxation is the best integrated rate revenue over measurable price paths satisfying the expected-demand stock constraint, with the same scaling. The policy revenue is its expected sales revenue, and its relative regret is . Fact 1 states and gives a positive uniform lower bound on .
Assumption 2 selects distinct ordinary test prices. Their mean rates identify the parameter through a Lipschitz inverse map , and demand changes at most as the parameter varies. The square root of each test-price rate is differentiable on . Algorithm 2 spends time units testing these prices in equal subintervals, estimates each rate from its Poisson count increment, and sets . It then posts , where maximizes revenue rate and minimizes the distance of demand to . It keeps that price until time or stock-out. See §5.1–5.2.
The capstone is the uniform bound in Proposition 3, equation (17). With , the mission asks for one constant , independent of , , the optimizer choices, and the probability space, such that
The intermediate quantitative target is equation (A-25), which retains the learning time:
The milestone list also carries Fact 1, the optimal deterministic price path and value from the first assertion of Lemma 1, both Poisson tails of Lemma 2, the pricing-phase revenue bound (A-17), the deterministic stability bounds (A-19), (A-22), and (A-23), and the parameter-estimation bound of Lemma 6. The paper's assertion that the policy is “asymptotically optimal” follows from the displayed regret estimate together with nonnegative regret; the displayed numerical estimate is the formal goal.
A finite-dimensional demand model lets the seller learn from a fixed set of prices rather than probing an increasingly fine price grid. Proposition 3 quantifies the resulting revenue loss at , compared with the paper's upper bound for its nonparametric learn-then-price policy. Both guarantees compare actual expected revenue with the full-information deterministic benchmark, including stock-out. These rates are proved in the article; the mission seeks machine-checked Lean proofs of the stated model, auxiliary bounds, and capstone. No such proof is claimed here.
The formalization would also provide reusable interfaces for a unit-rate Poisson counting process, deterministic inventory-constrained revenue optimization, measurable price selectors, and a random price chosen from normalized count observations. The later single-parameter policy in the paper uses related ideas but is a separate mission with different stages and a different rate.
A rate estimate can be close to the true rate while the selected price changes between two different optimizers: the unconstrained revenue maximizer and the price that matches inventory to expected demand. A bound for only one optimizer does not control the maximum of the two. The learning price is random, and the number of requests in the pricing phase is evaluated at a random Poisson clock. Stock-out further couples the learning phase to the amount available for later sales. These features prevent a direct substitution of an ordinary parameter-estimation bound into the final revenue formula.
Lean uses with its sup norm for parameter vectors, a finite positive off price, and a Poisson process on an arbitrary probability space. Each demand curve is defined on all real prices but is constrained on and at ; the inverse and concavity conditions apply on the attainable rate interval. The deterministic benchmark is a real supremum over measurable, integrable admissible price paths. The class assumptions make its value nonempty and bounded. Policy revenue uses a nonnegative integral of pathwise revenue, avoiding a default zero from a nonintegrable signed expectation.
Inventory is measured in whole units, so the cap is , equal to the paper's when that quantity is integral. Test-price observations remain uncapped in the formula for ; if stock runs out during learning, capped later sales are already zero. The continuous optimizer choices are measurable selections satisfying the actual max/min properties for every member of . The bound is uniform over these choices and over all unit-rate Poisson processes.
The printed Assumption 2(i)b asks for a solution to the test-rate equations for every vector in . Such a solution cannot always lie in compact , although the proof applies Assumption 2(ii) to . Here is a Lipschitz map into that recovers each true parameter from its test-rate vector; it can be viewed as the unconstrained inverse followed by a nonexpansive projection in the paper's box example. This explicit convention is required to make the estimate and subsequent use of Assumption 2(ii) coherent. It is an interpretive repair of the printed condition.
The paper prints the regret bound for , where . The exploration policy can lose revenue at , so the formal theorem starts at . The comparison is encoded by positive lower and upper multipliers after a fixed threshold, with for all relevant market sizes. This admits the usual finite initial adjustments and leaves the bound uniform over the sequence. No fixed demand curve, known parameter, finite price grid, or uncapped sales model can satisfy this target by substitution.
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 .Multistage robust optimization chooses decisions over time while an adversary picks the uncertain data from a known set; every later decision may react to what has been observed. The exact problem is a nested min-max over functions of the past, and is intractable in general. The standard workaround, proposed by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 2004), restricts every decision to an affine function of the observed disturbances. The restricted problem is a single convex (often linear) program, which is why disturbance-affine policies are used throughout robust control, inventory management and model predictive control. The price is suboptimality, and before this paper there was no nontrivial multistage problem in which that price was known to be zero.
Bertsimas, Iancu and Parrilo (arXiv:0904.3986, 2009; Math. Oper. Res. 35(2), 2010) proved that for one-dimensional linear dynamics with box constraints on controls and disturbances, linear control costs and convex state costs, disturbance-affine policies are exactly optimal. Their companion paper (Bertsimas & Goyal, Math. Program. 2012) shows how poorly affine policies can perform in other settings, so the one-dimensional result marks one side of the boundary between models where affine policies are exact and models where they are not.
Fix a horizon and an initial state . For each stage there are a per-unit control cost , control bounds , disturbance bounds , and a state cost that is convex and coercive. The state evolves as
The controller chooses after seeing ; the adversary then chooses . The min-max value is the value of the nested problem , computed by the Bellman recursion with :
An affine control policy and an affine running cost at stage are
so sees the disturbances before stage and those up to stage . Under these policies the state after stage is .
There exist affine policies and affine costs such that, for every ,
At this says that affine policies are robustly feasible and attain the min-max value.
The theorem is one of the few exact optimality results for affine policies in multistage robust optimization. Combined with linear programming duality it has a computational corollary: when the are piecewise affine, an optimal policy for the full min-max problem is obtained from a single linear program (the affinely adjustable robust counterpart, p. 5), instead of a dynamic program over a continuous state. The construction also shows what is special about one dimension: the relevant uncertainty enters only through a planar zonogon, whose right side has at most vertices, matching the coefficients of an affine policy.
The result is proved in the literature, not formalized; no machine-checked proof of it, or of the zonogon lemmas it uses, is known. The formalization adds a checked proof of the main theorem and of the planar convexity facts (Lemma 4.1, Corollary 4.1) that are reusable for other zonotope arguments. It also closes the gaps the preprint leaves to the reader: Assumption 2 is removed by an infinitesimal perturbation argument, footnote 4 assumes a unique minimizer of , and Lemma 4.3 is proved in one sub-case only.
Dynamic programming gives the optimal control as a function of the current state, , which is piecewise affine in with up to three pieces. Since is affine in past disturbances, the obvious idea is to substitute; but the composition is piecewise affine, not affine, in the disturbances, and no single affine function reproduces it. An affine policy is necessarily suboptimal at some disturbance sequences. The theorem asserts only that it is never suboptimal at the worst case, and that the excess cost it causes can be absorbed into an affine cost that still dominates . Establishing this requires controlling where a convex objective is maximized over a zonogon, and showing that the affine controller and the affine cost can be chosen to reproduce exactly the right-side vertices that matter, at every stage, while staying feasible. A naive matching of all vertices of the disturbance box is overdetermined.
Stages are indexed by Fin T (0-based). The model is the reduced form (DP) of §2, with dynamics coefficients equal to 1; the paper notes that this is without loss of generality. The standing hypotheses are those of Problem 1.1 (, convex and coercive) plus two disclosed additions, and : the page writes both as intervals but does not say they are nonempty. is defined by the Bellman recursion with sSup/sInf over images of nonempty compact intervals of continuous functions, so the values are attained maxima and minima. The max in (14) is stated with IsGreatest, which asserts attainment.
The goal carries none of the proof's normalizations (Assumptions 1–3 of p. 10, the unique minimizer of footnote 4). The milestones of §4 are stated in the paper's simplified notation: the unit hypercube, generators ordered as in (32) (cross-multiplied), the clamp form of the optimal control law (the printed (8) has misprinted thresholds), and, where the paper divides by , the hypothesis . Lemma 4.4 takes Lemma 4.3's conclusions as hypotheses; Lemmas 4.8–4.9 take system (51)–(53) (with two misprints of (53) corrected) as hypotheses instead of "computed by Algorithm 2". Every fraction in a system is cross-multiplied.
Trivializing formalizations are ruled out. (14) uses a maximum over a nonempty box of a continuous function, with the true . The policies read only past disturbances (sums over , resp. ). is the Bellman value over all state-feedback controls, not the value of the affine problem.
The development needs convexity of value functions under partial minimization and maximization, extreme points of planar polygons, and maxima of convex functions over polytopes. Contributions of independent planar-geometry lemmas are welcome, as are proofs of Lemma 4.3 (not stated here) and of the remaining construction lemmas 4.5–4.7.
A retailer, an airline or an online platform decides which products to show a customer. Showing more is not always better: a customer who would have bought an expensive product may switch to a cheap one once it is offered. The assortment problem asks for the set of products that maximises expected revenue, given a model of how customers choose. It is a central problem of revenue management (Talluri and van Ryzin, 2004), and it is NP-hard even for mixtures of two multinomial logit models (Rusmevichientong, Shmoys, Tong and Topaloglu, 2014).
The standard heuristic in practice is revenue-ordered assortments: sort the products by price and only consider the sets consisting of the most expensive products down to some threshold. It is optimal under the multinomial logit model (Talluri and van Ryzin, 2004), but not in general. Berbeglia and Joret (arXiv:1606.01371) ask how much revenue the heuristic can lose under every reasonable choice model, and answer with guarantees that depend only on the prices.
Timeline:
There is a finite nonempty set of products. For a choice set , is the probability that a customer offered buys product , and is the probability that the customer buys nothing. The system is a regular discrete choice model if
Axiom 4, regularity, says that adding products never makes a given product, or leaving without buying, more likely. Every random utility model is regular.
Each product has a positive price . The revenue of is , and . Let be the distinct prices, so counts price levels and not products, and set . The revenue-ordered assortments are , , and the heuristic earns
The goal fixes no constant beyond the paper's own quantities. Both parts are required: the sum form is the sharper bound, and the paper shows it is attained (Theorem 3.4, a later mission of this series).
The theorem shows that a pricing-only quantity controls the loss of the most common heuristic in revenue management, uniformly over all regular choice models, including every random utility model, mixtures of logits and Markov chain models. Combined with the hardness result of Aouad et al., it shows that revenue-ordered assortments achieve essentially the best ratio, as a function of or of , that an efficient algorithm can achieve. The same analysis transfers to the envy-free pricing and Stackelberg problems studied in the later sections of the paper.
The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a Lean formalization of regular choice models, the revenue-ordered heuristic and its two guarantees, on which the paper's tightness examples, the purchase-probability bound (Theorem 3.3) and the applications to pricing can build.
The argument is short, but two points are easy to get wrong. First, revenues of and of an optimal involve choice probabilities evaluated at different sets, so the comparison must pass through , using regularity once for products and once for the no-purchase option. A model that only assumes regularity for products does not satisfy the theorem. Second, the bound runs over distinct price levels, not products, and the first summand uses the convention ; indexing by products or dropping gives a different quantity. The comparison of the sum with is a Riemann-sum estimate for and needs a real-analysis lemma not phrased this way in Mathlib.
C with decidable equality; choice sets are Finset C. The choice probabilities are P : C → Finset C → ℝ, defined on all pairs. The no-purchase option is not a product: is the derived quantity noPurchase P S = 1 - ∑ x ∈ S, P x S.IsRegular P carries axioms (i)–(iv), with (i) and (iv) each split into a product case and a no-purchase case. The no-purchase case of (i) is redundant with (iii) and is kept to match the page.r : C → ℝ with the hypothesis ∀ x, 0 < r x. revenue P r S is and opt P r is the maximum over all Finset C (Finset.sup'), including the empty set.level r i is for and level r 0 = 0; numVals r is , the number of distinct values. roSet r i is ; roValue P r is the maximum over only.Real.log, applied to .Needed infrastructure: finite sums over price levels and summation by parts, the comparison of with , and the sorted enumeration of a finite set of reals (Finset.orderEmbOfFin). The regular model and the revenue-ordered sets are shared with the other missions of this series. Contributions of any milestone, alternative proofs of the logarithmic bound, and proofs that specific choice models are regular are welcome.
A retailer holding a fixed stock of a perishable or seasonal good (fashion items, airline seats, hotel rooms, concert tickets) must sell it before a deadline, after which unsold units are worthless. Demand is random and depends on the posted price, and the firm may change its price at any time. Dynamic pricing asks how the price should depend on the remaining stock and the remaining time.
Gallego and van Ryzin (Management Science 40(8), 1994) posed this problem as a continuous-time intensity control problem and established its basic structure. Their Theorem 1 says that the optimal expected revenue is strictly increasing and strictly concave in both the stock and the time remaining, and that the optimal price falls as stock grows and rises with the time left to sell. The paper is a standard reference of revenue management; the structural result is the continuous-time counterpart of the monotonicity of marginal values in discrete-time models (Talluri and van Ryzin, The Theory and Practice of Revenue Management, 2004, Proposition 5.2), and it is what makes the optimal policy computable by restricting attention to monotone policies. The paper credits a slightly weaker version to Kincaid and Darling (1963). The source formalized here is the published 1994 article.
The firm chooses a demand rate from a set of allowable rates, an interval containing ; the market then sets the price , where is the inverse demand function, strictly decreasing and nonnegative on the positive rates. The rate corresponds to the null price at which nothing sells. The revenue rate is
The demand function is regular when is continuous, bounded and concave on and has a least maximizer . The exponential demand , with , and , is the running example.
With units in stock and time remaining , write for the optimal expected revenue. The paper derives the Hamilton–Jacobi system
with and . The difference is the marginal value of an item; a rate attaining the supremum is an optimal intensity , and is the optimal price .
For the solution of (8), with strictly concave, differentiable on the interior of , and interior:
Theorem 1 is the qualitative backbone of single-product dynamic pricing. Concavity of in means that each additional unit is worth less than the previous one, which is the basis of bid-price and marginal-value reasoning in revenue management; the monotone price path justifies markdown practice as the deadline approaches and reduces the policy search to monotone policies. Proposition 3 answers, for exponential demand, a question raised by Mills (1959): the stochastic optimal price is never below the deterministic one. The closed form (9)–(10) is one of the few exactly solvable intensity control problems in pricing.
The results are proved in the paper; none of them has a machine-checked proof. Formalizing them requires the comparison and monotonicity theory of a countable system of coupled ordinary differential equations whose right-hand side is a convex conjugate, a theory that Mathlib does not package. A complete development would also certify the corrected hypotheses of Theorem 1 described below.
The value functions are defined only implicitly by (8), a triangular infinite system of ODEs in which each is driven by through the nonsmooth map . Monotonicity of the optimal intensity in is a statement about the time derivative of a marginal value, and the paper establishes it by an induction on combined with an argument by contradiction on the first interval where monotonicity could fail. The obvious approach of differentiating (8) twice in needs second derivatives of and of that the hypotheses do not provide, and the paper's own proof of Proposition 1 assumes that is nondecreasing in , which is only established in Theorem 1; a rigorous development must break this circularity.
A regular demand function is a Lean structure (GVRPricing.Structure.Model) holding , and with the paper's standing assumptions of §2.1: an interval, strictly decreasing and nonnegative on , continuous, concave and bounded on , and the least maximizer. The definition IsHJBSolution encodes (8) for , with the second argument the time remaining, the two-sided derivative at each , continuity on , the boundary conditions, and the requirement that the set inside the supremum be bounded above, so that the real supremum is never a default value. An optimal intensity at is any maximizing over .
All theorems are about solutions of (8), on which the paper's proofs operate. The identification of the solution of (8) with the supremum of expected revenue over non-anticipating pricing policies is Brémaud's verification theorem, which the paper cites and does not prove; it is not part of this mission.
Added hypotheses and corrected statements.
A formalization that defines by a formula, or postulates a monotone function as the optimal intensity, would trivialize the goal: the goal quantifies over every solution of (8), and the optimal intensity it asserts must maximize the right-hand side of (8) at every .
A complete development needs comparison principles for scalar ODEs with Lipschitz right-hand sides, properties of the concave conjugate (monotonicity, Lipschitz continuity, envelope theorem), and monotone comparative statics of maximizers. These are reusable well beyond this mission; contributions of any of them, or of the milestones in any order, are welcome.
Hassler Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets of elements carrying an abstract notion of dependence that captures what linearly dependent columns of a matrix and cycles of a graph have in common. A distinctive feature of the paper is that it gives several independent axiom systems for the same structure: one in terms of rank, one in terms of independent sets, one in terms of bases, and one in terms of circuits (minimal dependent sets). It then proves they are interchangeable. These equivalences, now called cryptomorphisms, are what allow matroid theory to move freely between the algebraic picture (rank of a set of vectors) and the combinatorial one (cycles of a graph, minimal dependent column sets). Every textbook on the subject relies on them, for example J. Oxley, Matroid Theory, Chapter 1.
This mission treats one of them: the equivalence of Whitney's rank postulates (§2) and circuit postulates (§8). The circuit side is the one used in combinatorial optimization, where circuits appear as cycles in network flows, as minimal infeasible subsystems, and in the exchange arguments behind the greedy algorithm.
Let be a finite set of elements. For subsets we write for and for .
Rank system. A function assigning an integer to each satisfies the rank postulates if
With the number of elements of , the nullity is . An element is dependent on if . A circuit of is a minimal dependent set: a subset with such that for every proper subset of . In Lean these are IsRankSystem r, nullity r N, IsDependentOn r e N and circuitsOfRank r P.
Circuit system. A family of subsets, called circuits, satisfies the circuit postulates (§8, p. 516) if
(C₁) No proper subset of a circuit is a circuit.
(C₂) If P₁ and P₂ are circuits, e₁ is in both P₁ and P₂, and e₂ is in P₁ but not in P₂, then there is a circuit P₃ in P₁ + P₂ containing e₂ but not e₁.
In Lean this is IsCircuitSystem C for a predicate C : Finset α → Prop.
Rank from circuits. Whitney defines (p. 516):
Let e₁, ⋯, e_p be any ordered set of elements of M. Set Γᵢ = 0 if there is a circuit in e₁ + ⋯ + eᵢ containing eᵢ, and set Γᵢ = 1 otherwise (compare Theorem 5). Let the "rank" of (e₁, ⋯, e_p) be r(e₁, ⋯, e_p) = Σ_{i=1}^{p} Γᵢ.
In Lean, rankSeq C l is this sum for a list l, and rankOfCircuits C N is its value on the enumeration N.toList of a subset .
For every finite set :
where is the family of circuits of and is the rank defined from . This is Whitney's closing sentence of §8 (p. 517): "The definitions of rank and of circuits under the two systems (R), (C) agree, and hence the systems are equivalent."
The equivalence makes the circuit postulates a complete description of a matroid: everything stated about rank, nullity, independence and bases can be phrased through circuits and back. Downstream in the same paper, the fundamental sets of circuits of §9 (Theorem 9) and the binary-matroid characterization of the Appendix are stated in terms of circuits, and they depend on circuits and rank being interchangeable. Theorem 5, read on its own, expresses the nullity of a set as a count of circuit-closing steps. This is the abstract form of the fact that the cycle space of a graph has dimension equal to the number of non-tree edges.
On the formal side, Mathlib's Matroid is built on the base axioms and proves circuit elimination (Matroid.IsCircuit.strong_elimination) as a theorem about that structure. Whitney's own route is different: rank defined from circuits by an ordered sum of , with order-independence (Lemmas 7 and 8) as the central step. That route has no machine-checked version that we know of, on Prove2Me or elsewhere. This mission formalizes the 1935 argument as stated: the rank and circuit systems as Whitney wrote them, and the two translations between them.
The obvious definition of the rank of a set from its circuits enumerates the set and counts the elements that do not close a circuit with their predecessors. This definition depends on the enumeration, and nothing in , obviously prevents two orderings from giving different counts. Lemma 7, the swap of two adjacent elements, is where does real work, through a case analysis on which of the two swapped elements closes a circuit. In the other direction, for circuits of a rank function requires turning the local postulate into a statement about unions of two circuits. Defining the circuit rank as a maximum over orderings, or as the size of a largest circuit-free subset, sidesteps exactly the step the paper proves and is not this mission.
α with [Fintype α] [DecidableEq α]. The ground set is all of α, and subsets are Finset α. Whitney's matroid is a finite set .ℤ), so that is a true difference.N.toList. Its independence from the enumeration is Lemma 8, and the definition does not build it in.Matroid in the statements. Doing so would turn the equivalence into a library lemma. The statements are about Whitney's postulates on bare functions and predicates.The development needs only finite sets, lists and permutations from Mathlib. The definitions IsRankSystem and IsCircuitSystem can be reused for the other cryptomorphisms of the paper. Contributions are welcome on any milestone, and so are local helper lemmas, such as monotonicity of rank under – or invariance of rankSeq under prefix-preserving changes.
Mathlib/Combinatorics/Matroid/Circuit.lean (circuits of Mathlib's Matroid). https://github.com/leanprover-community/mathlib4Distribution 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:
Least-squares regression fitted by stochastic gradient descent — the least-mean-square (LMS) algorithm — is the basic large-scale learning procedure: each observation is touched once, at a cost linear in the dimension. Classical analyses of stochastic approximation give the rate for non-strongly-convex objectives, and when the objective is -strongly convex. For least squares, is the smallest eigenvalue of the input covariance, which in high-dimensional problems is close to zero, so the strongly convex rate is often worse than the non-strongly-convex one.
F. Bach and E. Moulines (arXiv:1306.2119, NeurIPS 2013) showed that for the square loss this dichotomy disappears: averaged LMS with a constant step size reaches the rate with no strong-convexity assumption, and with a constant that does not involve the smallest eigenvalue. Averaging of stochastic approximation iterates goes back to Polyak and Juditsky (SIAM J. Control Optim. 1992), whose guarantees are asymptotic and use decreasing step sizes. The proof technique for the expansion of the noise process is adapted from Aguech, Moulines and Priouret (SIAM J. Control Optim. 2000). This mission formalizes the non-asymptotic bound in expectation (Theorem 1 of the paper) and the chain of lemmas of its Appendix A.
Let with , inner product and norm . For , is the operator . For self-adjoint operators, means that is positive semi-definite.
The data are independent and identically distributed pairs , , with finite second moments. The covariance operator is , assumed invertible (its eigenvalues may be arbitrarily small). The least-squares objective
attains its global minimum at , and is the residual. The model need not be well specified: need not vanish. Two constants satisfy
These are assumptions (A1)–(A6) of §2.1. The LMS recursion with constant step size , started at , is
and its average is .
For every step size and every ,
The constants are the paper's. A companion item states the case , where the bound reads .
The result. Theorem 1 gives a finite-sample, dimension-explicit bound with two terms: a variance term , which matches the minimax rate for least-squares regression, and a bias term . Neither involves the smallest eigenvalue of , so the guarantee survives ill-conditioning, which is the regime of high-dimensional learning. The bound is the basis for the paper's later results: the high-probability bound (Theorem 2) and the constant-step algorithm for logistic regression (Theorem 3), whose analysis invokes Theorem 1 for the quadratic approximations.
Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge no part of it has been machine-checked. A formalization yields a reusable layer for linear stochastic approximation in finite dimension: martingale-difference noise in , second-moment bounds for linear recursions driven by random operators, Loewner-order arguments, and averaging. The lemmas are stated for an abstract filtration and an abstract operator , so they apply beyond this model. The mission also records the corrections the appendix needs (an "" that should be "" in (13), an index in (16), and the exponent of in A.5).
Two steps resist the naive approach. First, the obvious one-step analysis — expand and take expectations — yields the bias part and Lemma 1, but on the noise it gives only , which does not decrease with . The rate requires averaging to cancel the noise, and this cancellation is visible only for the recursion with replaced by its mean . The random recursion is therefore expanded in powers of around the mean recursion, and each term needs its own covariance bound, by induction on , using the independence of from . Second, the induction relies on Loewner-order bookkeeping: sums of must be bounded uniformly in without dividing by small eigenvalues.
The space is EuclideanSpace ℝ (Fin d). Operators are continuous linear maps, and is an explicit two-sided inverse. Observations are indexed from . Averages are , with in every statement that uses them. The covariance operator is defined by its bilinear form, . Every Loewner inequality whose sides are expectations is an inequality of quadratic forms (for example for all ), which is the same order for self-adjoint operators.
Lean's Bochner integral is on non-integrable functions, so every moment assumption carries the integrability of its integrand, and every bounded expectation in a conclusion is paired with an integrability conjunct. Without these, a heavy-tailed would satisfy (A6) vacuously and a conclusion could hold through the value ; neither formalization is acceptable. Independence is of the pairs , not of and separately. (A4) is attainment of the minimum, not a gradient condition.
The following hypotheses are added to the page and disclosed in each item:
A complete development needs:
All of these are reusable for other stochastic-approximation missions. Proofs of any milestone are welcome, as are alternative arguments for the noise bound that avoid the expansion.
A firm that sets prices without knowing how demand responds to them has to learn the demand curve from its own sales. Each price it charges is both a revenue decision and an experiment. The natural policy, certainty equivalent pricing, re-estimates the demand parameters after every period and charges the price that would be optimal if the estimates were exact. den Boer and Zwart show that this policy can fail: with positive probability its prices settle at a suboptimal value, because they converge too fast for the estimates to keep improving (den Boer–Zwart 2014, Proposition 1, the subject of the companion mission). The same phenomenon was found by Lai and Robbins (1982) for a linear control problem.
Their remedy, Controlled Variance Pricing (CVP), keeps certainty equivalent pricing but forces the sample variance of the chosen prices to decay no faster than . The main result is that this small amount of enforced exploration gives regret , hence for every , for a broad class of demand models that are specified only through their first two moments. Keskin and Zeevi (2014) later placed CVP in a larger family of semi-myopic policies with regret for linear demand.
A seller chooses in each period a price , with , and then observes demand . Demand at price has mean and variance , where the link and variance function are known and on , , and the parameter with is unknown. The noise is a martingale difference with conditional variance and a uniformly bounded conditional moment of some order .
The expected revenue is . Near it has a unique maximizer in the open interval with there, and . The regret of a policy is
The estimate is the maximum quasi-likelihood estimate (MQLE), the root of the quasi-score equation (3), . With and the sample mean and variance of , the taboo interval is with . CVP starts from two distinct prices , fixes and , and for : if does not exist or has the wrong signs, it charges whichever of is farther from ; otherwise it charges if that keeps , and the best price outside if not.
stated as: there is , depending on the model, , and the initial prices but not on , with for all . The constant is left free, so the statement survives any sharpening of the constants.
The theorem shows that a policy that is certainty equivalent almost all of the time, with a single interpretable tuning parameter , attains regret in generalized linear demand models, without distributional assumptions beyond two moments. It explains the role of precisely: is the cost of exploration and the cost of estimation error. Proposition 2 and Lemma 1 are reusable for any policy that enforces a variance floor on its actions, and (11) is a self-contained rate for least squares under adaptively chosen designs.
The result is proved in the paper, with Proposition 3 delegated to den Boer and Zwart (2012) for general links. To our knowledge none of it has been machine-checked. A formalization would verify the delegated consistency argument, fix the conditions under which it applies (see Formalization scope), and provide a Lean development of adaptive least squares and quasi-likelihood rates that the related Keskin–Zeevi missions also need.
The deterministic parts are short. The difficulty is Proposition 3. The prices are chosen adaptively from past data, so the regressors are not independent of the noise, and standard rates for (quasi-)likelihood estimates do not apply. The natural argument, bounding by with a self-normalized martingale quadratic form, needs a bound that holds in expectation and not only almost surely, as in Lai and Wei (1982). For a non-linear link the MQLE is defined only implicitly, and its existence near has to be shown first, with a moment bound on the last time it fails. That is the random time . Turning almost-sure consistency into a rate in expectation is where most of the work lies.
All declarations live in the namespace CVPricing.Regret. Periods are 1-based. Prices, demands and parameters are real; with the Euclidean norm (euclidNorm), not Mathlib's sup norm. The design matrix, sample mean and are the published Keskin–Zeevi definitions fisherOf, avgPriceOf, infoMetricOf. Every is "there is such that for all ", with quantified after the model data. Rates are stated for and the regret for . and are total functions constrained on . A root of (3) counts only where for every observed . CVP is a predicate on a realized path that allows every maximizer in (7) and (8).
Disclosed deviations from the page:
Corrected slips: Proposition 2 is stated for , because the printed range fails at (, not ). Theorem 1 keeps the printed range. Eq. (20) is stated for and for beyond an explicit threshold.
The goal does not assume the variance bound, consistency or (20). The policy contains the variance check and the taboo interval, and the regret is the expectation over the actual price process. A statement that assumed any of these, or that dropped the taboo step, would be trivial or false. Contributions are welcome on adaptive least squares (Sherman–Morrison and determinant-ratio bounds), martingale last-time moment bounds, and the implicit-function step (18).
The lost-sales inventory problem with lead times is a basic model of operations management. A retailer reviews one product's stock each period and places an order that arrives periods later. Demand that cannot be met from stock on hand is lost, and the retailer pays a holding cost per unit left on the shelf and a penalty per unit of lost demand. The optimal policy depends on the whole pipeline of outstanding orders, so the state space grows with , and the problem is computationally hard for long lead times. Simple base-stock (order-up-to) policies are therefore the standard heuristic, and Huh, Janakiraman, Muckstadt and Rusmevichientong (Management Science 2009) showed they are asymptotically optimal as the lost-sales penalty grows.
Agrawal and Jia (arXiv:1905.04337) study the learning version, in which the demand distribution is unknown and only sales, not demands, are observed. They give an algorithm whose regret against the best base-stock policy is , improving the earlier bound of Zhang, Chao and Shi, which grows exponentially in . The improvement rests on one structural fact: started from two different states, the base-stock system accumulates expected costs that differ by an amount linear in and independent of the horizon. That fact, Lemma 2.5 of the paper, is the goal of this mission.
Fix a lead time and a base-stock level . A state is a vector of real numbers. Its entry is the on-hand inventory after the current period's arrival, and are the outstanding orders, the most recent. Under a base-stock policy with level the states lie in
In each period a demand is drawn, independently across periods, from a distribution on . The sales are and the on-hand inventory is . The policy reorders exactly what was sold, so for the next state is
and for the state never changes. The pseudo-cost of period is , and the value over horizon from the start state is
Along a demand path, is the total sales and the total on-hand inventory.
States are compared by the order of Definition B.1: if with and some such that for and for . Thus holds the same total, shifted toward the shelf. The state dominates every state of .
For every , every horizon , all costs , every demand law and all ,
The constant is the paper's printed one. The proof's last display gives , a stronger bound, which is deliberately not the goal.
All of the following hold for , along any single demand path that drives both chains:
Lemma 2.5 bounds the dependence of the base-stock chain's finite-horizon cost on its starting state, uniformly in the horizon. In the paper it yields three consequences: the long-run average cost (the loss) of a base-stock policy does not depend on the initial state (Lemma 2.6), the bias of the chain is bounded by (Lemma 2.8), and finite-horizon average costs concentrate around the loss (Lemma 2.10). These feed the regret bound of Theorem 1.3. The lemma is also a statement about the base-stock lost-sales system alone, without any learning, so it is of independent interest for coupling arguments on lost-sales chains.
The paper's proof is complete on paper, but nothing in it has a machine-checked proof. Neither the lost-sales base-stock chain with lead times started from an arbitrary pipeline state nor any of the coupling lemmas of Appendix B is formalized elsewhere. This mission produces a checked proof of the goal and of the pathwise comparison lemmas. Theorem 1.3 is not posed: its supporting lemmas rely on limits whose existence the paper settles only by an informal discretization (Remark 4).
The obvious argument couples the two chains on a common demand path and waits until they coalesce. Coalescence is guaranteed only after consecutive periods of zero demand, an event of probability exponentially small in , so this argument gives a bound exponential in . That is the bound of earlier work.
The linear bound needs a finer pathwise accounting. The two coupled chains do not stay ordered: the one that starts with more inventory on the shelf sells more at first, then runs short and sells less. The order between the two states alternates along a sequence of times, and the sales gained in one phase must be shown to be lost again in the next, so that the cumulative difference stays bounded by a constant multiple of for every horizon. Turning this alternation into a bound requires tracking how the pipeline vectors evolve between alternation times, including the boundary cases in which the chains coalesce or the horizon ends inside a phase.
All declarations live in the namespace LostSalesLearning.ValueGap. A state is a function Fin (L + 1) → ℝ, a demand path is a function ℕ → ℝ≥0, and time is 0-based: traj s d 0 is the paper's , traj s d t is , and is a sum over Finset.range T. The demand law is a probability measure on ℝ≥0, and the demand path has the product law Measure.infinitePi (fun _ => F). The value is the expectation of the summed pseudo-costs, which equals Definition 2.4 by the tower property and is the form used in the paper's proof.
Committed conventions:
alternationTimes; an absent next crossing is none.Two trivializing formalizations are ruled out. A comparison of the two values on different or fixed demand paths would be a different statement: the goal compares two expectations under the same law, and each pathwise milestone uses one common path. A Bochner integral of a non-integrable function would be . The integrand here is measurable and bounded by on , so the values are genuine expectations.
A complete development needs the elementary dynamics of the chain, including invariance of and the shift of trajectories, which is reusable for other lost-sales models. It also needs the alternation times of Definition B.4, and measurability of the trajectory in the demand path. Proofs of individual milestones, alternative proofs of the goal, and sharper constants as separate statements are all welcome.
Many large convex programs have far more constraints than can be handled at once, but each constraint on its own is simple: a single linear equation or inequality. Row-action methods exploit this by touching one constraint per iteration. L. M. Bregman's 1967 paper (DOI 10.1016/0041-5553(67)90040-7) introduced the general framework behind most of them. A strictly convex function induces the "distance" , now called the Bregman distance, and the method moves from point to point by -projections onto one constraint at a time. For this reduces to Hildreth's method for quadratic programming; for entropy-type it gives the balancing (matrix scaling) methods used for transportation and traffic problems. The later literature on Bregman projections, mirror descent and entropic regularisation starts from this paper.
This mission formalizes the last main result of the paper, Theorem 4 (p. 212), which treats linear inequality constraints. Here a plain projection cycle does not minimize . Bregman's fix carries a vector of nonnegative multipliers along with the primal point and lets each step either move towards a violated constraint or relax a multiplier. The result is a primal–dual method.
Timeline. Hildreth (1957) gave the quadratic case. Bregman (1967) proved the general theorem stated here. Censor and Lent (1981) revisited the method for interval constraints under explicit assumptions on Bregman functions (DOI 10.1007/BF00934676).
Let be -dimensional Euclidean space and a convex set. Let be strictly convex on , continuously differentiable over with gradient , and continuous over the closure . Let be an matrix () with nonzero rows , and . The inequality program (2.11)–(2.13) is
with feasible set , assumed nonempty. The Bregman function is (1.4). The -projection of onto the hyperplane minimizes over . The standing hypotheses ("the conditions of Theorem 3") are that satisfies the abstract conditions I–VI of §1 for these hyperplanes, together with condition (2) of Note 1: implies . In addition, -projections of interior points of stay in the interior. Condition V (compact sublevel sets of ) is used for .
Write , where , and . A run of the method is a sequence of pairs with , , , and cyclic indices . Each step with is one of the following:
For every run of the method,
Theorem 4 says that a method using one constraint per step and only 's gradient converges to the minimizer of a strictly convex function over a polyhedron intersected with . Its multipliers form a dual sequence. Note 4 of the paper deduces from the theorem that the optimal value equals over dual-feasible pairs (, ). The theorem is the convergence statement behind Hildreth's algorithm, behind entropy-based balancing for linear inequality systems, and behind the later "interval convex programming" methods.
The theorem is proved on paper, but no machine-checked proof of it, or of any Bregman-projection row-action method, is known to exist. The formalization adds two things. It makes the paper's standing hypotheses explicit, since several are stated once or left implicit. It also forces a complete argument for the convergence of the whole sequence: the printed proof gets this from condition (2) by an argument that assumes a monotonicity property established in §1 for the pure projection method but not for the primal–dual one. A Lean proof of the goal therefore also supplies a complete proof of the paper's claim.
The standard argument for projection methods uses a Fejér-type property: decreases for every feasible . That fails here. In case (c) the point moves away from the hyperplane of a satisfied constraint, and can increase. So any argument has to control primal and dual quantities together. To pass from "every limiting point is feasible" to "the whole sequence converges to an optimal point", complementary slackness has to hold in the limit, and this depends on the cyclic order and on the cap . The naive route, applying the §1 convergence theorems to the hyperplanes , does not apply, because the iterates are not -projections onto fixed sets in case (c).
EuclideanSpace ℝ (Fin p); the rows are vectors , and is . The gradient is explicit data tied to by HasGradientWithinAt on . is not assumed open, and is continuous on .Many decision problems are solved repeatedly against data that arrive over time: routing traffic, allocating budgets, choosing portfolios or combinatorial structures. Online linear optimization models this. At each round a learner picks a decision from a fixed domain , then a reward vector is revealed and the learner earns . Performance is measured by regret, the gap to the best fixed decision in hindsight. When is combinatorial (paths, spanning trees, assignments), the only computationally reasonable access to is a procedure that optimizes a linear function over it, and in practice such procedures are often only approximate.
Follow the Perturbed Leader (FPL), introduced by Hannan (1957) and analysed for linear optimization by Kalai and Vempala (JCSS 2005), uses exactly one call to an exact linear optimizer per round and achieves regret over arbitrary, not necessarily convex, domains. Ben-Tal, Hazan, Koren and Mannor (arXiv:1402.6361, Operations Research 2015) needed a version of FPL that works with an additively approximate linear optimizer, as a building block for oracle-based robust optimization with linearly parametrized uncertainty sets. Their §3.3 analyses this variant and proves Theorem 6, the goal of this mission.
Fix a dimension , a domain (arbitrary: not necessarily convex, closed or bounded) and . An -approximate linear optimization procedure over is a map such that, for every ,
Reward vectors are fixed in advance (an oblivious adversary). Write , with , and .
Follow the Approximate Perturbed Leader with parameter plays at round
Three scale parameters enter the bound: bounds the diameter of , for ; bounds ; and bounds how much each reward varies over the domain, for .
With , for every ,
For every and ,
Theorem 6 shows that perturbed-leader online linear optimization is robust to additive error in its optimization subroutine: an -approximate oracle costs only extra regret, so the average regret is . This allows the algorithm to be run over domains where exact linear optimization is intractable but a good additive approximation is available, and the paper invokes it as the online-learning primitive of its oracle-based scheme for linearly parametrized uncertainty in §3.2 (that application is not part of this mission). Unlike online gradient methods, it requires no convexity of and no projection.
On the formal side, no regret bound for Follow the Perturbed Leader, exact or approximate, is currently formalized on the platform, and the Kalai–Vempala stability argument (comparing a uniform distribution on a cube with its translate) is a reusable piece of measure theory. The mission's statements are proved on paper; the work here is to formalize those proofs, with one correction to a hypothesis, explained under Formalization scope.
Lemmas 7 and 8 are deterministic and combinatorial. The substance is Lemma 9. It compares the expectations of one bounded function of under the uniform law on a cube and under its translate by . The natural first attempt, a pointwise comparison of and , fails: an approximate (even an exact) maximizer can jump arbitrarily under an arbitrarily small change of its input, and is not assumed continuous or even consistent between nearby inputs. Any valid argument must therefore control the two distributions as a whole rather than the decisions point by point, which in the formal development involves Lebesgue measure on , conditioning on a box and translation invariance.
A second subtlety is that the stability bound depends on how is read, which is the reason for the correction below.
Vectors are Fin n → ℝ with dotProduct. All quantities are written as , never with the default norm (the sup norm). Rewards are a function f : ℕ → Fin n → ℝ read at , and is prefixSum f t. The perturbation law is Lebesgue measure conditioned on the cube (ProbabilityTheory.cond volume), a probability measure for . Maxima over are expressed as "for every ", so neither attainment nor boundedness of is presupposed.
Conventions and deviations, each also stated in the affected item:
A trivializing formalization is ruled out: must return points of (otherwise would not bound ), it must be measurable, and the perturbation law is the normalized uniform distribution, not Lebesgue measure restricted to the cube (which is not a probability measure for ).
Needed infrastructure: the overlap estimate for a cube and its translate, , and the integrability of bounded measurable functions of . Both are reusable for any perturbation-based online-learning analysis; contributions of these as standalone lemmas are welcome.
A decision maker choosing a random outcome (a portfolio return, a policy's cost savings, a schedule's throughput) often has a reference outcome , the result of a benchmark policy, and wants the new outcome to be preferable to it for every risk-averse decision maker, not just on average. Expected-utility theory (von Neumann and Morgenstern) makes this precise: is preferred to by every decision maker with a concave nondecreasing utility function exactly when dominates in the second order, . Requiring as a constraint in an optimization problem avoids having to elicit any particular utility function, which is rarely possible in practice and impossible when several decision makers must agree.
Dentcheva and Ruszczyński (preprint 2002, published in SIAM J. Optim. 14(2), 2003) introduced optimization problems with stochastic dominance constraints and developed their optimality and duality theory. The central finding is that the Lagrange multiplier of a second-order dominance constraint is itself a concave nondecreasing utility function: the optimal solution maximizes the objective plus an expected utility, for a utility function implied by the problem. This interpretation underlies the later literature on dominance-constrained portfolio optimization, risk-averse stochastic programming, and the dual (quantile) theory of stochastic orders.
Let be a probability space and the space of integrable random variables with its norm topology. For the distribution function is and the second-order shortfall function is
Changing the order of integration gives (2.6), where . The relation means for all , and .
The problem data are a reference outcome , a convex closed set , a functional that is concave and continuous on , and an interval . The paper studies the relaxation in which dominance is enforced on :
The uniform dominance condition (Definition 4.1) asks for some with .
The multiplier class consists of the functions that are concave and nondecreasing, vanish on , and are affine on : for , with a constant . The Lagrangian is
Assume the uniform dominance condition. If is an optimal solution of (3.1)–(3.3), there is with
Conversely, if for some a maximizer of satisfies (3.2) and (4.3), then is optimal for (3.1)–(3.3).
The milestones follow the paper's proof. They are: finiteness of for ; the identity (2.6), already proved on the platform; Proposition 2.3 (convexity and closedness of , and its recession cone); the concavity of the constraint operator with respect to the cone of nonnegative functions; the existence of a nonnegative measure multiplier on satisfying (4.5)–(4.6); the facts that the function (), () of a nonnegative measure lies in and that every is for exactly one ; the key identity
and the weak-duality step: (3.2) implies for every .
With , the dual problem has a solution, its value equals the primal optimal value, and its solutions are exactly the satisfying (4.2)–(4.3).
Theorem 4.2 turns an infinite family of constraints, one for each , into a single scalar trade-off: at the optimum, the decision maker behaves as an expected-utility maximizer for an implicit utility , and the dominance constraint is active exactly in the sense . Theorem 5.1 makes the space of dual variables, which is the starting point of dual decomposition and cutting-plane methods for dominance-constrained problems and of their extensions to several constraints and to higher orders (Sections 6–7 of the paper, not part of this mission).
All results are proved in the paper. Apart from the identity (2.6), which is proved on the platform, none of them is formalized as far as the platform records show. A machine-checked development would provide, on top of the paper, a rigorous treatment of the measure–utility correspondence that the paper obtains from a textbook theorem "after an obvious adaptation", and a careful account of the multiplier class itself (see the scope section on the constant ). The definitions of and of the identity (2.6) are shared with the platform's missions on Dual Stochastic Dominance and Related Mean-Risk Models (Ogryczak and Ruszczyński, 2002).
The necessity half needs a Lagrange multiplier for a constraint taking values in the infinite-dimensional space ; finite-dimensional convex duality does not apply, and the multiplier first appears as a nonnegative measure on , an element of the dual of . A Slater-type point is required: without the uniform dominance condition the multiplier may not exist. This is why the dominance relation, which the paper first poses on all of , is relaxed to a bounded interval : for a reference outcome with a smallest value , , so no can dominate strictly near .
The second obstacle is the translation of that measure into a utility function. The identity (4.9) requires an interchange of integrals over and an integration by parts against the distribution function of an arbitrary integrable , followed by a limit in which the integrability of controls the linear growth of at . The converse direction needs every to be represented by a unique measure, through the left derivative of a concave function.
Outcomes are elements of Mathlib's space Ω →₁[P] ℝ over a probability measure P, coerced to functions inside integrals; no statement is pointwise in . is the published definition DualSSD.Shared.secondPerformance, a Bochner integral of over . The problem data form a structure whose fields include every standing assumption of the paper: convex and closed, concave and continuous on . The constraint (3.2) is stated in its printed expectation form, while Definition 4.1 and the proof objects use , as printed; their equality is (2.6).
Committed conventions:
A trivializing formalization is ruled out: a junk-valued expectation (a Bochner integral of a non-integrable function, which Lean sets to ) cannot occur for , and its integrability is a milestone. Dropping the concavity of or the convexity of would make the necessity half false, so these assumptions are fields of the problem data.
Infrastructure a complete development needs: convex duality for cone constraints in (or a direct separation argument in ), the Riesz representation of nonnegative functionals on , Fubini and integration by parts for Stieltjes measures, and the measure of a left-continuous monotone function. These pieces are reusable beyond this mission. Contributions to any milestone are welcome. The extensions to several dominance constraints and to higher-order dominance are not included.
In online convex optimization a decision maker picks points in a convex set , and after each choice pays for a convex cost function chosen in advance by an adversary. Performance is measured by regret: the total cost paid minus the cost of the best fixed point in hindsight. Zinkevich (ICML 2003) showed that projected gradient descent has regret when the whole function , or at least its gradient at , is revealed after each round.
In many applications only the number is observed: a seller sets a price and sees revenue, a router picks a path and sees its delay, an advertiser places a bid and sees the cost. This is the bandit setting. Flaxman, Kalai and McMahan (arXiv:cs/0408007, SODA 2005) gave the first simple algorithm for bandit convex optimization against an oblivious adversary with general bounded convex costs: a randomized gradient descent that estimates the gradient from a single function value, with expected regret . The same one-point gradient estimate is the starting point of later work on bandit convex optimization and on zeroth-order (derivative-free) stochastic optimization; see, e.g., Bubeck and Cesa-Bianchi's survey (arXiv:1204.5721, Ch. 6) and Hazan's textbook (arXiv:1909.05207, Ch. 6).
Timeline. Zinkevich (2003): regret with full gradient feedback. Kleinberg (NIPS 2004), independently: bandit regret for Lipschitz costs by a different reduction. Flaxman, Kalai, McMahan (2004/2005): for bounded convex costs and for Lipschitz costs, with one function value per round. Later work (Bubeck, Lee, Eldan 2017 and others) reached with more complex algorithms.
Let and be the closed unit ball and the unit sphere, . The feasible set is closed and convex with
The costs are fixed before play (an oblivious adversary); each is convex on with for , where . For , is the nearest point of to .
The bandit gradient descent algorithm (Figure 1 of the paper) keeps an iterate with . At period it draws a unit vector uniformly from , independently of the past, plays
observes only , and updates
The smoothed cost is with uniform on . The expected regret after rounds is
For every , with , and ,
The paper prints the constant . Its own last step bounds the regret by with , , , and with the stated and this equals . The goal states the bound the proof establishes.
The tuning identity (p. 9): at , , for .
Theorem 2 (p. 9). If each is -Lipschitz on , then with , , , and large enough that ,
The theorem shows that bandit feedback costs only a polynomial factor in regret for arbitrary bounded convex costs, with an algorithm that is gradient descent plus one random perturbation per round. Lemma 1 is the general tool behind it: an unbiased estimate of the gradient of a smoothed function from one function value. It is reused across zeroth-order optimization, bandit learning and stochastic approximation. Lemma 2 is a self-contained regret bound for projected gradient descent with noisy gradients, the shape in which Zinkevich's analysis is most often applied.
The results are proved in the paper and are standard. To the platform's knowledge none of them has a machine-checked proof. Related statements from Bubeck and Cesa-Bianchi's survey, for differentiable Lipschitz losses, are open on the platform, and two earlier formalizations of the textbook versions were disproved because of missing regularity or independence hypotheses. Formalizing this mission produces a checked one-point gradient identity for continuous (not differentiable) functions on the sphere, a measure-theoretic regret bound for stochastic projected gradient descent, and the corrected constant of Theorem 1.
The bandit algorithm itself is simple; the difficulty sits in Lemma 1 and in the measure theory around it. The paper derives Lemma 1 from Stokes' theorem, , and the ratio of the volume to the surface area of a ball. Mathlib has neither this divergence identity on balls in nor the explicit link between its spherical measure and the surface integral needed here. The identity must hold for functions that are merely continuous near the ball, since convex costs need not be differentiable.
The obvious first idea, differentiating under the integral sign in , fails because is not differentiable. The second obvious idea, applying Lemma 1 to as given, fails at the boundary of , where is unconstrained. Lemma 2's conditional expectation requires that the direction be independent of the iterate , and the integrability and measurability of the played points come from continuity of convex functions in the interior of .
Points are EuclideanSpace ℝ (Fin d) with , and rounds are numbered . The costs are functions on , and no statement assumes anything about them outside : no global convexity, continuity, differentiability or Lipschitz bound. The standing model is part of the goal's hypotheses: is convex with , the costs are convex on with values in there, and . Additions and conventions:
uniformSphere d). Uniform marginals alone are not enough.IsBGDRun) required for every outcome. Projection uses the published predicate IsNearestPoint, and regret the published pseudoRegret, whose minimum is an infimum over the subtype; it is attained in every use here.A formalization that assumed integrability of the costs along the run, assumed differentiable or globally Lipschitz costs, dropped the independence of the directions, or stated through Mathlib's gradient (which is off differentiability) would trivialize or change the result. All of these are ruled out.
Needed infrastructure: the divergence identity for the ball average (Lemma 1), conditional expectation given for vector-valued variables, continuity of convex functions on the interior of a convex set, and nearest-point projection onto closed convex sets. The first two are reusable well beyond this mission. Contributions toward Lemma 1 in particular are welcome.