Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the accepted cutoff-87 theorem already covers every , the new work is the range from 85 to 87.
The cutoff came down from 90 to 87 in a day, through moona3k's proofs at 89, 88 and 87. The 89 proof reran the cutoff-90 argument with sharper, second-order estimates. A numerical model of that argument with retuned constants puts its limit between about 86.6 and 87.5: two of its steps pull the same parameter in opposite directions, and below that point no setting satisfies both. So reaching 85 is expected to need a new idea, not just tighter numbers. The goal theorem below gives the exact statement.
This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 85 or lower also settles this mission.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryAssortment optimization asks a retailer which products to offer when customers substitute among them. The nested logit model groups products into nests and is one of the most used choice models in revenue management, because it relaxes the independence of irrelevant alternatives of the plain multinomial logit model while keeping choice probabilities in closed form. Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) study how the tractability of the assortment problem under this model depends on two features: whether the dissimilarity parameters of the nests are at most one, and whether a customer who selects a nest always buys there (fully-captured nests).
When the dissimilarity parameters are at most one and the nests are fully captured, offering the highest-revenue products in every nest is optimal (Theorem 4 of the paper). This mission concerns what survives when a dissimilarity parameter exceeds one, the regime the paper calls possibly synergistic products. Then the problem is NP-hard (Theorem 5), and the paper shows that the same nested-by-revenue assortments still achieve an explicit, data-dependent fraction of the optimal expected revenue.
There are nests and products in every nest. Product of nest has a revenue and a preference weight , ordered so that . Nest has a dissimilarity parameter , and is the weight of leaving without choosing a nest. Throughout this mission the nests are fully captured: the within-nest no-purchase weights are zero. For an assortment in nest ,
and the expected revenue of is
Problem (2) maximizes ; its optimal value is . The nested-by-revenue assortment collects the highest-revenue products of nest , with and .
Problem (2) is equivalent to the linear program (3): minimize subject to and for every nest and every . Problem (4) keeps the second family of constraints only for candidate assortments; here the candidates are , which gives a linear program with variables and constraints. The performance factor of the nested-by-revenue assortments is
Assume for every nest, for some nest, positive revenues and . If is an optimal solution of (4) over the nested-by-revenue assortments, then
Combined with Theorem 1 of the paper this yields for the assortment read off the small linear program; that consequence is a companion item.
Two companion statements follow the goal: the bounds and when revenues, respectively preference weights, within each nest differ by at most the factors , ; and the guarantee .
Because problem (2) is NP-hard once a dissimilarity parameter exceeds one (Theorem 5 of the paper), an exact polynomial algorithm is not expected, and a guarantee for a polynomial-size candidate family is the natural substitute. Theorem 7 gives one with an explicit factor computed from the data: when revenues within each nest are balanced, when preference weights within each nest are balanced, and the nests may differ arbitrarily from one another. The same linear-programming argument (Theorem 1) is reused for partially-captured nests in §6 of the paper.
The result is proved in the paper (Appendix A.1); no machine-checked version is known. A formalization verifies an appendix argument that is stated with little detail, and fixes the conventions that the page leaves implicit, such as the value of the objective of (8) at and the role of the standing assumption that some exceeds one.
Theorem 7 is a feasibility statement for the exponentially many constraints of (3), one per subset of every nest, while optimality of only controls the nested-by-revenue constraints per nest. The obvious approach, comparing each subset directly with a nested-by-revenue assortment, fails: when the nested-by-revenue assortments are not optimal within a nest, and the example of §4.1 shows that they can lose an unbounded factor. The constant must absorb the gap between a fractional assortment and its two neighbouring nested-by-revenue assortments, which the dual-style solution of the small program does not see.
Lean 4 with Mathlib. Nests form a finite type ι; products are Fin n, indexed from , so is nbr n j = {k | k < j} and product of the page is ⟨k - 1, _⟩. Powers are real powers (Real.rpow), and division is total (), which gives and value for the objective of (8) at .
Standing assumptions in every statement: , , , , , revenues ordered within each nest (§1); for every nest and for some nest (§4, p. 16). Added and disclosed: wherever (6) appears, so that no denominator of (6) vanishes; , the nonempty range of (6); only in the guarantee , inherited from Theorem 1. The factor enters as a real number with the hypothesis that it is the greatest element of the set of terms of (6). An optimal solution of (4) is a feasible pair whose is minimal among feasible pairs.
A trivializing formalization is ruled out: is the maximum of (6), not an arbitrary upper bound, and the goal states feasibility for the full program (3) over every subset of every nest, not for (7) or for the candidate collection.
Needed infrastructure: maximization of a continuous function on , the greedy solution of a continuous knapsack, monotonicity of weighted averages and elementary real-power calculus. These are reusable beyond this mission. Proofs of any milestone, of the companions, and of the §4.1 example are welcome.
A portfolio manager who maximizes expected utility needs the distribution of asset returns, but in practice only estimates of its first two moments are available, and these estimates are themselves noisy. Distributionally robust optimization handles this by optimizing against the worst distribution in a set of plausible ones. Delage and Ye (Operations Research 58(3), 2010) proposed a set of distributions defined by confidence bounds on the mean and on the second-moment matrix, showed that the resulting problems are solvable in polynomial time for a large class of costs, and applied the framework to portfolio selection.
The set contains an upper bound on the covariance but no lower bound. Remark 1 of the paper says a lower bound "leads to important computational difficulties" and argues it should be unnecessary: for a concave utility, a less predictable market can only reduce expected utility, so the worst distribution should already have the largest covariance allowed. Proposition 3 in §5.2 turns this argument into a theorem for piecewise-linear concave utilities and unconstrained support. This mission formalizes Proposition 3 and the steps of its proof.
Let assets have a random return vector , and let be a portfolio, so the return is . A distribution of is a Borel probability measure on with finite second moments. For symmetric matrices, (the Loewner order) means is positive semidefinite.
Given a support set , a centre , a positive definite matrix and , , the distributional set of Assumption 3 is
The second constraint, (1b), is the covariance constraint.
The utility is piecewise linear concave, with pieces, and the cost of a return is :
With estimates , of the mean and covariance, the inner problem of the robust portfolio problem with unconstrained support and an exactly known mean () is
The proof relates (18) to a semidefinite program in variables , , :
For every (the mean-uncertainty radius of the robust portfolio problem (16); (18) is the case ),
The worst-case expectation is attained, and at a distribution for which the covariance constraint holds with equality. The statement holds for every portfolio , every , every , every , every , every and every .
The proposition justifies a modelling decision of the whole paper: for portfolio problems with piecewise-linear concave utility, adding a lower bound (display (2)) to the distributional set cannot change the robust decision, so the computational difficulty that lower bound would cause is avoided at no loss. It also shows that, under these assumptions and with , the paper's semidefinite formulation solves the known-moment portfolio problem of Popescu (2007) in polynomial time (Remark 4). The worst case is explicit: a finite mixture of distributions with prescribed first and second moments, read off an optimal solution of (19).
The result is proved in the paper; no machine-checked version is known. Formalizing it requires a moment-problem argument (from a distribution to a feasible point of an SDP) and its converse (from an SDP solution to a distribution), both of which are reusable for other moment-based distributionally robust results. The proposition concerns the robust portfolio problem with ; the paper's proof writes out only "for simplicity of our derivations". The goal states the proposition for every ; the milestones follow the written proof and are stated for .
The obvious argument, "a concave utility prefers less spread, so the adversary maximizes spread", does not prove anything by itself: increasing the second-moment matrix of a given distribution in the Loewner order does not determine its law, and the expected cost depends on the whole law, not on the moments. The proof goes through the semidefinite program (19). Two steps carry the weight. First, every distribution in must be mapped to a feasible point of (19) with no smaller value, although the cost is only piecewise affine in . Second, an optimal point of (19) must be turned back into a distribution in ; this needs the existence of random vectors with prescribed first and second moments, and care with blocks where , which the paper sets aside "without loss of generality" although such a block can carry a nonzero that the mixture would lose.
Fin n → ℝ; all Euclidean quantities are dot products, never the sup norm. Matrices are Matrix (Fin n) (Fin n) ℝ; is (B - A).PosSemidef; is Mathlib's matrix inverse, used only with .Measure (Fin n → ℝ) that is a probability measure and whose coordinates are in (MemLp _ 2). This makes every mean, second moment and expected cost a genuine integral; without it a non-integrable expectation would evaluate to .[NeZero K]).The source is the authors' draft of 20 February 2008 of the Operations Research paper; every page, display and label in this mission refers to that draft.
Graham (1966) showed that list scheduling finds a schedule within a factor of optimal for precedence-constrained jobs on identical parallel machines, the first performance guarantee for an approximation algorithm. When the machines run at different speeds (uniformly related machines), the same analysis breaks down, and for two decades the problem resisted a guarantee independent of the speeds better than .
Timeline:
The mission formalizes the makespan half of that paper, up to its Theorem 3.7.
An instance has jobs and machines. Job requires units of processing, and machine runs at speed , so job takes time units on machine . A strict partial order on the jobs gives precedence constraints: means that job may not start until job has completed.
A schedule runs each job without interruption on one machine , from a start time to its completion time . A machine processes at most one job at a time, and forces . Its length is . is the length of an optimal schedule.
Let be the distinct speeds and the number of machines of speed . An assignment names the speed class at which job is to run. Its loads are , and its chain bound is the largest value of over chains of . Speed-based list scheduling is Graham's rule restricted by the assignment: whenever a machine of speed is idle, it starts the first available job on the list with .
The linear program LP has variables , and . It minimizes subject to the following constraints:
From a solution, with , the assignment algorithm gives each job the speed class of largest capacity .
There is an absolute constant such that for every instance with machines and distinct speeds, the better of the two schedules below has length at most
The result gives the first guarantee for , independent of the speeds, and a guarantee depending only on the number of distinct speeds. Through the batching technique of Shmoys, Wein and Williamson it extends to release dates (Corollary 3.8). Since LP also relaxes the preemptive problem, it gives an bound on the ratio between the nonpreemptive and preemptive optima (Corollaries 3.9, 3.10). The "In fact" form, relative to an arbitrary feasible LP solution, drives the paper's algorithm in §4.
The result is proved in the literature but, as far as is known, not formalized. A formal proof requires machine-checking the following:
Later work gave a combinatorial -approximation (Chekuri and Bender, 2001) and an -approximation (Li, 2017). These are not part of this mission.
Graham's argument has two lower bounds:
With different speeds, the first bound fails: a chain may have been run on slow machines, and its length then says nothing about . Forcing every job onto a fast machine repairs chains but can leave most machines idle, so the second bound fails. The paper only guarantees that all machines of one speed are busy at each moment of an idle period. Making this pay off requires an assignment that controls chain lengths and per-class loads simultaneously. That assignment is the delicate part: Theorem 2.1 is the bookkeeping, while Lemmas 3.2 and 3.4 rely on the LP. Two of the formal steps are routine on paper but fiddly in Lean: time-interval accounting over a continuous-time schedule, and the counting of rounded speed classes.
Fin n and machines Fin m with . and . is a strict partial order, and a chain is a finite set of pairwise comparable jobs. is the maximum completion time, or with no jobs.Proofs of any milestone are welcome. Reusable beyond this mission are the following: the model of nonpreemptive schedules on uniformly related machines with precedence, the speed-based list-scheduling predicate with Theorem 2.1, and the LP.
Fashion and consumer-electronics retailers sell a product at full price early in a season and mark down what is left. Consumers learn the pattern, and some of them wait for the markdown. Such strategic consumers lower the revenue of the full-price period, and the retailer's stocking decision affects how deep the markdown is expected to be. Quick response — a second, more expensive replenishment placed after demand is observed — is usually valued as a way to match supply with exogenous demand (Fisher and Raman 1996; Cachon and Terwiesch, Matching Supply with Demand, 2005). Cachon and Swinney ask how strategic waiting changes that value.
The source is the authors' working paper of April 2007, revised November 25, 2007, not the 2009 Management Science version, whose numbering and wording may differ. Its answer: with strategic consumers the retailer stocks less (Theorem 1), and under an explicit cost condition, quick response is worth more to a retailer facing strategic consumers than to one facing only myopic consumers (Theorem 3).
A retailer sells over two periods. It sells at the exogenous full price in period 1 and at a markdown price chosen at the start of period 2. Leftover units are worth . First-period demand has density and distribution function , and satisfies the monotone scaled likelihood ratio (MSLR) property: for every , is monotonic on the support of .
The market has three segments:
The standing assumptions are and . Let be the fraction of strategic values above .
By a threshold argument (Lemma 1), strategic consumers with value below some buy at and the rest wait. A fraction of demand then buys in period 1, and the inventory left for period 2 is . The period-2 revenue counts the waiting strategic consumers with value at least and, if , the bargain hunters, up to the inventory . The retailer's expected profit at unit cost is
With quick response, units ordered before the season cost and units ordered after observing cost , with . The second order covers all first-period demand and may add stock for the sale. The resulting profit is .
In the sale period, waiting strategic consumers are rationed: they effectively face the inventory , where measures their place in the queue. A strategic consumer with value who waits gains, in expectation,
where is the demand level below which the retailer clears stock at . A rational expectations equilibrium is a pair in which maximizes and is a best response of consumers who correctly expect . The superscript denotes the benchmark with only myopic consumers (): and are the optimal myopic profits without and with quick response.
Assume MSLR and no rationing, , , , and condition (6):
Let be any equilibrium without quick response, any equilibrium with it, and , the myopic optima. Then
The milestones follow the paper's path:
Corollary 1 is the percentage form, .
Theorem 3 identifies a second channel through which quick response creates value. Beyond matching supply to demand, it lets the retailer keep its initial stock low enough that a deep markdown becomes unlikely, so strategic consumers buy at full price. Under (6), all of them do. Quick response thus reduces strategic waiting without withholding availability, unlike the inventory-signalling remedies in the literature, and the theorem quantifies when this effect dominates.
The results are proved in the working paper, partly in a technical appendix. No machine-checked version of them, or of the underlying markdown game, is known. A formalization pins down several statements that the paper states loosely:
It also produces reusable components: the newsvendor with salvage and the reactive-capacity fractile under a general density, and a rational-expectations equilibrium predicate for a retailer–consumer game.
The profit is not concave: with strategic consumers it is concave–convex (Figure 4 of the paper). The newsvendor argument therefore does not give a unique optimal order, and Lemma 3's quasi-concavity rests on MSLR in a short appendix step.
Existence (Theorem 1) needs a fixed point of the map best response, but the consumer best response is a correspondence, not a function, so the printed intermediate-value argument does not apply directly. Theorem 3 needs a statement about every equilibrium with quick response, while Theorem 2's proof only exhibits one. Ruling out an equilibrium with requires comparing the derivative (4) of with the myopic derivative along the whole demand distribution.
Lean represents prices, quantities and valuations as reals, demand by a density on , and expectations as Lebesgue integrals against . The model carries the standing assumptions of §3 as fields, plus the following additions and corrections, each disclosed in the item notes:
Optimal revenues are suprema over all prices (and with quick response). "Optimal order" means a maximizer over all , never a stationary point, and the myopic benchmarks are the same functions at . Defining the optimal revenue by Lemma 2's closed form would make Lemma 2 and the first-order conditions definitional; it is not done.
The fill rate is , set to when no strategic consumer waits. With Lean's instead, would be a best response to every order and Theorem 2's last claim would be trivial.
A complete development needs:
The last two are reusable beyond this mission. Proofs of any milestone, alternative existence arguments, and sorry-free proofs of the newsvendor items are welcome. The comparison ", " of Theorem 2 and §8's numerical study are outside the scope.
In a stochastic multi-armed bandit a player repeatedly chooses one of arms and receives a random reward drawn from that arm's unknown distribution; the aim is to pull suboptimal arms as rarely as possible. Lai and Robbins (1985) and, for general models, Burnetas and Katehakis (1996) showed that any reasonable strategy must pull a suboptimal arm at least times in rounds, where is a minimal Kullback–Leibler divergence defined below. A strategy whose expected number of pulls matches this constant is asymptotically optimal.
For rewards in , classical index policies such as UCB (Auer, Cesa-Bianchi and Fischer, 2002) achieve pulls but with a constant governed by the gap of the means, not by . Cappé, Garivier, Maillard, Munos and Stoltz, Kullback–Leibler upper confidence bounds for optimal sequential allocation, Ann. Statist. 41(3), 2013 (arXiv:1210.1136v4), introduce the KL-UCB family of index policies and prove finite-time bounds whose leading term is the Lai–Robbins/Burnetas–Katehakis constant. This mission formalizes their result for empirical KL-UCB (Algorithm 3, Theorem 2), which is asymptotically optimal in the nonparametric model of finitely supported distributions on . A companion mission covers kl-UCB in one-parameter exponential families (Theorem 1).
Timeline: Lai and Robbins (1985), lower bound for parametric families; Burnetas and Katehakis (1996), lower bound and asymptotically optimal policies for general models; Honda and Takemura (2010, 2011), the DMED algorithm, asymptotically optimal for finitely supported and bounded rewards; Cappé et al. (2013), the first index policy with a non-asymptotic bound whose leading term is optimal in this model.
A bandit has arms with reward distributions in a known model : the set of probability distributions over with finite support. Write , and ; arm is suboptimal if . At each round the player picks an arm based on past observations and observes a reward drawn from . is the number of pulls of arm up to round .
Equivalently, each arm has a reward stack of i.i.d. draws from , all stacks independent, and the -th pull of arm returns . The empirical distribution of the first rewards is , and .
The minimal divergence is
the smallest Kullback–Leibler divergence from to a distribution of the model whose mean exceeds .
Empirical KL-UCB (Algorithm 3) pulls each arm once, then for pulls an arm maximizing
where is the set of probability distributions carried by and . The added point is essential: without it the index is the empirical-likelihood bound, which equals the empirical mean when every observation is .
Assume for all arms and . There is a constant depending only on and such that, for every suboptimal arm and all ,
The constants are the paper's. is the one quantity the main text does not give; it is existentially quantified, before the bandit, so it may depend on nothing but .
Theorem 2 gives a finite-time bound whose leading term, , equals the Burnetas–Katehakis lower bound for the model . Hence empirical KL-UCB is asymptotically optimal among all strategies for finitely supported rewards in , and the regret inherits the optimal constant. Since is at least the Bernoulli divergence of the means, and usually larger, the bound improves on kl-UCB and UCB for the same rewards. Proposition 1 is a non-asymptotic coverage bound for the empirical-likelihood upper confidence bound with the point added, valid for every law on , not only finitely supported ones.
The proofs of Theorem 2 and Proposition 1 are in the paper's supplemental article (Appendix B), not in the main text; no machine-checked proof of either exists. The mission produces formal statements of the theorem and of the proof skeleton (5)–(10) that the paper shares with Theorem 1, and of the two facts about that the bound needs. A formal proof would supply an explicit , which the paper defines only inside the supplement.
The skeleton (5)–(10) is elementary bookkeeping; the difficulty lies in the two sums it leaves, both of which must be shown to be with explicit constants. The second, , needs a deviation estimate for the empirical of a suboptimal arm that is precise enough to keep the leading constant : a bound that only controls the deviation of the empirical mean loses it, since depends on the whole distribution. The first, , concerns the optimal arm after a random number of pulls , which the algorithm itself determines, so fixed-sample bounds such as Proposition 1 do not apply directly. Both need regularity of as a function of a distribution in an infinite-dimensional model, where none of the closed forms of the exponential-family case is available.
Arms are Fin K, and arm of the paper is index . The bandit is the platform's stack-of-rewards model RegretBandits.Stochastic.IsStochasticBandit: (indexed from ) are independent, identically distributed within each arm, with mean . Pull counts and are the platform's pullCount and bestMean. Added to the page, and disclosed in each statement: every reward lies in pathwise (a representation of " is carried by "), every arm choice is measurable, and in the goal the strategy is non-anticipating ( is measurable with respect to the arms and rewards of rounds ). A run of Algorithm 3 is a pathwise predicate: rounds pull distinct arms, and every later round pulls a maximizer of , with ties broken by any rule. KL is Mathlib's InformationTheory.klDiv in , with the empirical distribution as first argument. is kept in and converted to a real number only in the final bounds, where it is finite and positive. Probabilities of events whose measurability is not asserted are outer probabilities. The page's in (10) is stated as the finite sum over that (8) produces. The probability space of Theorem 2 lies in Type.
Trivializing formalizations are ruled out. The index is a supremum over a set that is nonempty (it contains ) and bounded above, so it is never Lean's junk value. and range over , not over all measures. The run predicate has both the initialization and the argmax clause. is quantified before the bandit and the horizon.
Reusable beyond this mission: for , the empirical-likelihood bound of (15), and Proposition 1, a concentration inequality for empirical that applies to any bounded i.i.d. sample. Proofs of any milestone are welcome, as are proofs of the skeleton (5)–(10) that also apply to the companion kl-UCB mission.
In online routing of virtual circuits, connection requests between pairs of nodes of a capacitated network arrive one at a time. Each request must be accepted and routed on a single path with bandwidth , or rejected, immediately and irrevocably, and no edge may carry more than its capacity. The goal is to maximize the number of accepted requests (the throughput). The model goes back to Awerbuch, Azar and Plotkin (FOCS 1993), whose deterministic algorithm has a logarithmic competitive ratio when edge capacities are at least logarithmic in the size of the network, and it underlies the analysis of admission control in circuit-switched and bandwidth-reserved networks.
Buchbinder and Naor (Math. Oper. Res. 2009) recover an algorithm with the same competitive factor from a general recipe: an online primal–dual scheme first produces a feasible fractional routing online, and an online version of Raghavan's pessimistic estimator (J. Comput. Syst. Sci. 1988) then rounds it, also online. This mission formalizes that construction and its guarantee (Section 5.2 of the paper, with the Section 3 scheme it uses).
Timeline:
Let be a finite set of edges with capacities , and . Requests arrive online; request comes with a finite list of admissible paths, each a set of edges, all of size at most .
A fractional routing assigns flows ; it is feasible when for every request and the load of every edge is at most . Its value is ; is the largest value of a feasible routing of the arrived requests, an upper bound on the integral optimum.
The fractional scheme. The covering LP paired with the routing LP (the paper's primal, Fig. 3) has variables (cost ) and (cost ) with constraints . When arrives, its paths are visited in order; for each path whose constraint fails, is raised from to the least value restoring it, while for and follow the flow ( the load of , the flow of ). The parameters are and .
The rounding. With the rounding scale , the integral edge usage and the number of served requests, the potential is ,
After the fractional round of , the algorithm serves on a path (adding to for ) if this gives potential at most the potential before the round; otherwise it rejects .
For every request sequence, the algorithm never exceeds a capacity, and for every feasible fractional routing ,
The fractional scheme's flows are feasible and for every feasible .
initially, always, and whenever the flows of a request are raised by a non-negative amount of total at most , serving the request on some path or rejecting it does not increase .
The result shows that a deterministic online algorithm for throughput-competitive routing, previously designed by hand, falls out of two generic components: an online fractional packing scheme and an online pessimistic estimator. A side product is that the fractional phase alone produces, online, a near-optimal routing that respects all capacities exactly, independently of their size. When the rounding loses only a constant factor and the algorithm is -competitive, as in Awerbuch–Azar–Plotkin.
The results are proved in the paper; none is machine-checked. A formalization supplies a checked instance of the online primal–dual method together with derandomized online rounding, and fixes the constants the paper leaves inside . Related platform content: the monograph's OnlinePrimalDual.Routing.per_copy_guarantee and routing_competitive concern the Buchbinder–Naor -competitive algorithm with copies of the graph, a different scheme.
The fractional guarantee is argued in the paper continuously (rates of change of the primal and dual values), while the scheme as formalized is discrete: each flow is the least value restoring a constraint, and every primal variable is a maximum whose branch may switch during the increase. The continuous argument does not transfer verbatim, and feasibility depends on the least value restoring the constraint with equality.
The rounding is a derandomization. The existence of a good path or a good rejection is established in the paper as an expectation over a random trial; a deterministic statement about finitely many alternatives is what the mission asks for, with all exponential terms of under control at once. A frequent first attempt compares with the potential after the fractional round; the rule compares with , before the flow increase, and the guarantee is stated for that comparison.
Fintype E; capacities are real and positive. A request is a List (Finset E) of paths; the request sequence is a list. Simple paths of a graph are a special case; nothing in the argument uses graph structure. is a parameter with every path of size at most .List (List ℝ) of the shape of the request sequence. is quantified as "every feasible fractional routing".sInf). Ties among good paths are broken by list order; only paths that received flow in the current round are candidates for serving, so a request whose flow was not increased is rejected.Contributions welcome: proofs of the milestones, a reusable lemma "convex combination value some outcome value" for derandomization, and the discrete-to-continuous bridge for the Section 3 scheme.
Retailers of seasonal goods (fashion, electronics, airline seats) sell a fixed stock over a finite season to customers who arrive over time, and those customers know that prices may fall. A customer who expects a markdown waits, and a seller who ignores this loses revenue. The classical revenue-management literature (Gallego and van Ryzin 1994; Talluri and van Ryzin 2004) models myopic customers who buy on arrival or leave; the literature on forward-looking (strategic) buyers, for instance Aviv and Pazgal (2008), studies particular price paths.
Board and Skrzypacz ask the mechanism-design question: among all selling schemes, which maximizes the seller's expected discounted revenue when buyers arrive over time, have private values and time their purchases strategically? Their answer, published in the Journal of Political Economy in 2016, is that the optimal mechanism has a simple structure: in every period the seller sells to the highest remaining buyer if and only if his value exceeds a cutoff that depends only on the period and the number of units left. When demand is weakly decreasing over time, the cutoffs are characterized by one-period indifference conditions, which in the continuous-time limit can be implemented by posted prices. The source used here is the authors' accepted manuscript of February 6, 2015; all page numbers refer to that manuscript.
A seller has units of a good and sells them over periods ; unsold units are worth zero after period . Payoffs are discounted by . At the start of period a random number of buyers arrives, independently across periods, with a law that may depend on . Each buyer wants one unit; his value is drawn independently from a distribution with continuous density , distribution function and support . The marginal revenue of a buyer with value is
assumed strictly increasing and continuously differentiable, with .
By the standard mechanism-design reduction (§2.1, eq. (2.5)), the seller's problem is to choose when to serve each buyer so as to maximize the expected discounted sum of the served buyers' marginal revenues. The state in period , after the period- entrants have arrived, is the number of units left and the values of the buyers present. The value and the pre-entry value satisfy the Bellman equation (4.3):
where is the set of buyers left after the highest are served and the next period's entrants. Selling one unit to today rather than none gives the difference function
and the cutoff is the smallest with . Comparing selling to today with waiting and selling at least one unit tomorrow (to the best of and the entrants) gives (p. 17). Demand is weakly decreasing in the usual stochastic order if for all and .
If is weakly decreasing in the usual stochastic order then, for every ,
and is the unique root of in for : the seller is indifferent between selling to the cutoff type today and waiting one period to sell that unit tomorrow (the one-period-look-ahead property).
For every and , the optimal rule sells to the highest buyer iff , whatever the values of the lower buyers; ; and is the unique root of .
In attack order:
After the goal, (4.7) gives the period- cutoff equation .
Theorem 1 says that the optimal allocation does not depend on how many buyers are present or what their values are, only on time and inventory. This is what makes the optimal mechanism implementable without eliciting values from buyers as they arrive. Theorem 2 turns the global dynamic program into local indifference conditions. In the continuous-time limit (§5 of the paper) these become differential equations, and the optimum is implemented by posted prices with an auction at the end of the season. Under weakly decreasing demand, therefore, the classical revenue-management practice of posting prices loses nothing against the best possible mechanism.
The paper's results are proved, in prose, with envelope-theorem and coupling arguments. They have not been machine-checked. A formal development would produce a verified backward-induction model of multi-unit dynamic allocation with random arrivals, with the structural results (monotonicity, deterministic cutoffs, monotone comparative statics in inventory and time) that recur across dynamic pricing and optimal stopping. Two printed gaps are recorded below: the positivity of , and the restriction of footnote 12 to .
The obvious argument fails at "deterministic". A priori the cutoff for the highest buyer depends on the values of the lower buyers, because selling a unit today changes which of them will be served later and when. Lemma 3(a) holds only under the induction hypothesis that all future cutoffs are already deterministic and decreasing in inventory, so Lemma 3, Theorem 1 and (A.1) form a single backward induction over periods and units, and none of them can be proved in isolation. The value function is an expectation, over a random number of i.i.d. entrants, of a maximum over sorted values, so continuity and strict monotonicity in (Lemma 3(b), and the same for ) are not available from general facts. The tempting argument for Theorem 2, that cutoffs fall over time simply because fewer buyers arrive later, is incomplete: Lemma 4 has to compare two periods with different arrival laws and different future cutoffs at once.
Periods are natural numbers with , and units are natural numbers. Values, marginal revenues and profits are real numbers. The buyers present form a finite multiset of reals, and an absent buyer is absent, never a value . The value law is the measure with density ; the density is positive and continuous on and zero outside, and is defined from and . Expectations over a cohort are lower Lebesgue integrals against of nonnegative bounded quantities, so no non-measurable or non-integrable integrand can silently become . The value function is defined by the Bellman equation (4.3), with . The sequence problem (4.1) over purchase times is not formalized; the paper says either may be used (footnote 16).
Standing assumptions and handled gaps:
The cutoff is defined from , never as the threshold of an optimal policy, and "optimal" always means maximal in (4.3) over every number of units sold. A formalization that postulates a threshold policy, replaces the random cohort by its mean, or sets absent buyers to value would trivialize or change the statements and is ruled out. The mechanism-design reduction (IC/IR to (2.5)) and the continuous-time results of §5 are out of scope.
The usual stochastic order is the published platform definition StochasticOrders.Usual.UsualOrder. A complete development needs finite-horizon dynamic programming over multisets, expectations of functions of sorted i.i.d. samples, envelope arguments, and monotone coupling for the usual stochastic order on ; these parts are reusable beyond this mission. Proofs of any milestone are welcome, as is a proof that (4.3) agrees with the sequence problem (4.1).
Newton's method is the basic second-order method of continuous optimization: at the current point it replaces the objective by its second-order Taylor model and jumps to the stationary point of that model. Its defining property is speed near a nondegenerate minimum, where the error is squared at every step, so that the number of correct digits roughly doubles per iteration. This local behaviour is what makes Newton's method the inner engine of interior point methods, the polynomial-time algorithms for linear, conic and general convex programming (Nesterov and Nemirovski, 1994). In S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015; arXiv:1405.4980v2), §5.3.2 recalls the traditional local analysis of Newton's method, Theorem 5.3, before turning to the affine-invariant self-concordance analysis used for interior point methods. This mission formalizes that theorem and the four steps of its proof.
Let carry the Euclidean norm , and write for the operator norm of a linear map , so that . Let be a function, with gradient and Hessian , a linear map (the derivative of the gradient map). For a real number , means for all .
The Hessian is -Lipschitz if for all .
Newton's method starts at and iterates, for ,
A point is a local minimum of if for all in a neighbourhood of ; it has strictly positive Hessian if for some .
Assume the Hessian of is -Lipschitz, , and is a local minimum with , . If , then Newton's method from is well defined (every Hessian along the iterates is invertible, so the sequence exists and is unique) and
The theorem gives a quantitative basin of quadratic convergence: an explicit radius , depending only on the curvature at the minimum and the Lipschitz constant of the Hessian, inside which Newton's method needs only iterations to reach accuracy . It is the classical statement whose shortcomings (dependence on a choice of norm, constants that change under linear changes of variables) motivate the self-concordance theory of the following subsections, and it is the local convergence result invoked whenever a damped or globalized Newton scheme is shown to enter its quadratic phase.
On the formal side, Mathlib has the calculus this needs (Fréchet derivatives, interval integrals of vector-valued maps, operator norms) but no convergence theorem for multivariate Newton's method for minimization. A formal proof produces reusable pieces: the integral form of the mean value theorem for gradients, the stability of a positive-definite lower bound under Lipschitz perturbations, and an inverse-operator norm bound from a quadratic-form lower bound. The result itself is classical and fully proved in the literature; what is open here is its machine-checked proof in this form.
The individual inequalities are short, but the argument is an induction in which well-definedness and the rate are proved together: the Hessian at is invertible only because is still in the ball of radius , and stays in that ball only because of the rate. A proof that first assumes the sequence exists and then bounds it is circular. The proof also passes between two kinds of control on the Hessian, a lower bound on its quadratic form and an operator-norm bound on its inverse, and the second is only meaningful once invertibility is established. Finally, the integral manipulations need integrability of the maps , which comes from the continuity of the Hessian.
is EuclideanSpace ℝ (Fin n). The gradient and Hessian are explicit maps and with ContDiff ℝ 2 f, HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every point; the norm on is Mathlib's operator norm, as on the page. is the quadratic-form inequality. A Newton run is a sequence indexed from satisfying the linear system ; no inverse of a possibly singular operator appears in any hypothesis, and "well defined" is a conclusion: a unique run exists from and every Hessian along it is bijective. The rate and are asserted for every run. The error representation is stated with both sides multiplied by , which is equivalent to the printed form once the Hessian is invertible. Milestones 3 and 4 use only the Lipschitz property and are stated for any Lipschitz map .
Added hypothesis: (the radius divides by ; with , Lean's convention would collapse the hypothesis to ). Convexity of is not assumed, as on the page; is a local minimum and is derived, not assumed. Encoding the Newton step with Lean's inverse (which returns on singular maps), or replacing by mere invertibility, would change the theorem and is ruled out.
A complete development needs the fundamental theorem of calculus for vector-valued maps along segments, Hessian-based quadratic-form estimates, and operator-norm bounds for inverses; all are reusable for the analysis of damped Newton, cubic regularization and interior point methods. Proofs of the milestones independently of the goal are welcome.
First-order methods, which query only function values and gradients, are the workhorse of large-scale optimization in machine learning, signal processing and operations research, because each step costs little more than one gradient evaluation. For a function that is both strongly convex and smooth, plain gradient descent converges geometrically, but the number of steps needed to reach accuracy scales with the condition number of the problem. In 1983 Nesterov showed that a gradient method with a carefully chosen momentum term needs a number of steps proportional to instead, and that this is optimal for black-box first-order methods. On ill-conditioned problems, where is in the thousands or millions, the difference between and is the difference between practical and impractical.
This mission is the tenth of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015; arXiv:1405.4980v2). It covers §3.7.1, the smooth and strongly convex case of Nesterov's accelerated gradient descent, and its main result, Theorem 3.18.
Work in with the Euclidean inner product and norm . Let be differentiable with gradient .
Nesterov's accelerated gradient descent starts at an arbitrary point and iterates, for ,
The point is a gradient step from , and moves beyond in the direction by the fixed momentum factor .
The analysis in the book uses auxiliary quadratic functions (an estimate sequence), defined from the points by
together with their centres (with and the recursion (3.21) of the book) and their minimum values .
For every run of the method and every ,
The geometric form in milestone 3 is slightly stronger than the goal, which follows from .
Theorem 3.18 gives -accuracy after gradient evaluations. Projected gradient descent with step on the same class contracts only at the rate (Theorem 3.10 of the book). The lower bound of Theorem 3.15 shows that no black-box first-order method can do better than , so the accelerated rate is optimal up to constants. The estimate-sequence argument is the template for many later accelerated methods: proximal, stochastic and variance-reduced variants such as Katyusha, and accelerated coordinate descent.
The result is classical and fully proved on paper. No machine-checked proof of the accelerated rate for strongly convex smooth functions is known to exist in Lean's Mathlib. This mission produces one, with the estimate sequence , its centres and its minimum values as reusable objects, and with every algebraic identity of the book's proof stated separately.
The algorithm is two lines, but its analysis is not a one-step contraction: neither nor decreases by the factor at every step. A Lyapunov argument for gradient descent, applied directly to , gives only the rate . The book obtains the rate through the auxiliary functions . The inequality (3.18) is easy, but (3.19), that the minimum of never drops below , depends on the exact choice of the momentum factor. It holds only through the identity , which ties the centre of to the iterates. Formally, the obstacles are the bookkeeping of the recursive quadratics on and the algebra in , and .
EuclideanSpace ℝ (Fin n). The gradient is an explicit map g with HasGradientAt f (g x) x at every point, which is part of the smoothness predicate IsBetaSmooth f g β. Strong convexity is the published definition OnlineConvexOpt.ConvexBasics.StronglyConvexOn Set.univ f g α, which is the book's (3.13).IsNesterovSCRun g α β x y on two sequences indexed from , with arbitrary. Every theorem holds for every run, that is, every starting point.kappa α β = β / α. All theorems assume and . The second is implied by the other hypotheses for ; no hypothesis is added.ConvexOptAlg.NesterovStrong. β-smoothness duplicates the predicate of other missions of the series and will be merged afterwards. Contributions welcome: proofs of the milestones, and general lemmas on quadratics that the algebraic milestones need.Regularized logistic regression and the support vector machine (SVM) are two of the most widely used linear classifiers. Both are usually introduced as empirical risk minimization plus a norm penalty whose size is tuned by cross-validation, with the penalty justified heuristically as a guard against overfitting. Distributionally robust optimization (DRO) offers a different reading: instead of minimizing the average loss on the training sample, minimize the worst average loss over all distributions close to the empirical one. Blanchet, Kang and Murthy (arXiv:1610.05627v4; J. Appl. Probab. 56(3), 2019) show that, for a suitable notion of closeness based on optimal transport, the robust problem and the penalized problem coincide exactly. The penalty is then the price of robustness against perturbations of the predictors, and the regularization parameter becomes the radius of an uncertainty set, which the same paper later chooses by a statistical criterion (the robust Wasserstein profile).
Related earlier work: Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015) studied Wasserstein-robust logistic regression with a metric that charges a finite price for flipping a label, and obtained regularized logistic regression only in the limit . The result formalized here is the exact statement at , together with the analogous statement for the hinge loss.
Training data are pairs with predictors and labels , . Their empirical distribution is , a probability measure on .
For a cost , the optimal transport cost between probability measures and on is
The cost used here is the label-preserving cost: for ,
Every distribution with has the same label distribution as ; only the predictors are perturbed. The exponent is the conjugate of , .
The losses are the log-exponential loss and the hinge loss , for a coefficient vector . The worst-case expected loss at radius is , the supremum over probability measures on .
For every and every ,
and consequently the two identities obtained by taking on both sides, which is how the paper prints the theorem.
The theorem identifies two standard estimators as exact solutions of a robust decision problem. Consequences: the penalty has a quantitative meaning (the adversary's transport budget), the regularization parameter can be chosen by the paper's robust Wasserstein profile instead of cross-validation, and the norm of the penalty is tied to the geometry of the perturbations (perturbations measured in give an penalty). The same identity is the input of the paper's coverage bound (Proposition 6) for .
The result is proved on paper; no machine-checked version is known. The formalization adds a precise statement of the objects involved (couplings with both marginals fixed, an infinite cost across labels, expectations of nonnegative losses with values in ), a checked version of the duality step specialised to this cost, and the treatment of boundary cases (, , ) that the paper does not discuss.
The identities are short once Proposition 1 is available, so the weight of the mission lies in two places. First, Proposition 1 itself is a strong duality theorem for optimal transport over all probability measures on , with a cost that takes the value and an unbounded loss, and with attainment of the dual minimum; it is quoted from Blanchet and Murthy (Math. Oper. Res. 2019) and not proved in this paper. The weak-duality inequality is routine; the reverse inequality requires constructing near-optimal distributions from the dual, which needs measurable selection of near-maximizers and does not follow from finite-dimensional convex duality. Second, the inner suprema require an exact Hölder-attainment argument for the pair of conjugate norms and , including and , and for the hinge loss a minimax exchange over . Bypassing duality by a direct construction of the worst distribution is possible for the upper value but not obviously for the lower bound at the boundary .
Fin d → ℝ, a data point is (Fin d → ℝ) × ℝ with the product Borel σ-algebra, and samples are indexed by Fin n with 0 < n. Labels are real numbers with the hypothesis , which Theorem 2 inherits from Example 2; the cost is defined on all of .PiLp q, with q p : ℝ≥0∞ and p.HolderConjugate q; and are included, and no further restriction on is imposed.WassersteinDRO.Regularization.empiricalDistribution.PiLp, and calculus for the logistic function. Contributions to any of these are welcome, as are proofs of the inner suprema, which are independent of Proposition 1.Upper bounds for an optimization method say how fast it converges; oracle complexity lower bounds say how fast any method of a given kind can possibly converge. Chapter 3 of S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015, arXiv:1405.4980) proves upper bounds for subgradient descent on Lipschitz functions and for gradient methods on smooth functions. Section 3.5 (Lower bounds, pp. 279–283) shows that these rates cannot be improved by more than a numerical constant, as long as the number of queries is smaller than the dimension. For smooth convex functions the matching lower bound is what identifies Nesterov's accelerated gradient descent, with its rate, as an optimal method.
Timeline. The lower bounds first appeared in A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization (Wiley, 1983). The presentation followed by the book, with an explicit tridiagonal quadratic as the hard instance and the "span of past gradients" restriction on the method, is that of Y. Nesterov, Introductory Lectures on Convex Optimization (Kluwer, 2004), §2.1.2. Nesterov's accelerated method (1983) attains the matching upper bound.
Work in with the Euclidean inner product , coordinates , canonical basis and balls . A first-order oracle for answers a query with a subgradient (the gradient when is differentiable). A black-box procedure maps the history to the next query . Section 3.5 restricts attention to procedures with
which covers gradient descent, its accelerated variants and conjugate gradient. A function is -smooth if its gradient is -Lipschitz; -Lipschitz on if every subgradient at every point of has norm at most ; -strongly convex if is convex.
The hard smooth instance uses, for , the symmetric tridiagonal matrix with entries on the first diagonal positions and on the neighbouring off-diagonal positions of the leading block, zero elsewhere, and the quadratics
For and there are a -smooth convex and a minimizer such that every procedure satisfying (3.15) has
The constant is the book's.
For and there are a convex , -Lipschitz on , and a first-order oracle for it such that every procedure satisfying (3.15) has ; and for there are an -strongly convex , -Lipschitz on , and an oracle with gap at least over that ball.
The upper bounds of Chapter 3 (projected subgradient descent at rate , accelerated gradient descent at rate ) become optimal statements only through these lower bounds: no method in the class (3.15) can be faster by more than a constant factor while is below the dimension. The restriction to is necessary, since Chapter 2's cutting-plane methods converge exponentially once the number of queries exceeds the dimension.
The results are classical and proved. Formalizing them yields machine-checked versions of the quadratic-form computation for the tridiagonal matrix, of the Krylov-type support argument under (3.15), and of the explicit minimizer of , each reusable in other lower-bound arguments (Theorem 3.15 in , lower bounds for strongly convex smooth functions, conjugate gradient analyses). The platform held no formal statement of these oracle lower bounds when this mission was drafted.
Each analytic step is elementary; the difficulty is in the bookkeeping. The span argument is an induction that must track, at each step, that the gradient of a tridiagonal quadratic at a vector supported on the first coordinates is supported on the first , and that the span hypothesis transfers this to the next query. The minimizer computation requires solving on the leading block and showing that the coordinates beyond do not affect . A natural first attempt, choosing the hard function after seeing the procedure, proves a much weaker statement and is excluded by the quantifier order: the function is fixed first and must defeat every procedure.
is EuclideanSpace ℝ (Fin n). Coordinates in Lean are 0-based; the definitions provide the book's 1-based coordinate coord x i and basis vector basisVec n i, and the matrix tridiag n k translates book index to Fin n index . The query sequence starts at index . The oracle is a fixed map , so (3.15) reads with . In Theorem 3.14 the oracle is the gradient, given as a map with HasGradientAt everywhere; -smoothness is the Lipschitz bound on that map. In Theorem 3.13 the oracle is part of what is constructed, because the book's proof uses a specific "resisting" subgradient selection and the claim fails for an arbitrary one.
Committed conventions, each stated in the item's Formalization Note: the minimum over is the bound for every such , and is required; is ; the minimizer is existentially chosen together with (the hard function has many minimizers when , and the bound is false for some of them); the minimum over a ball is the bound against every point of the ball; is the real infimum, asserted to be attained.
A formalization that let the function depend on the procedure, dropped , or took the span over gradients at points other than the queries would state a different and weaker theorem; the statements here keep (and the oracle) before the universally quantified procedure.
Infrastructure needed: quadratic forms of explicit matrices on EuclideanSpace, gradients of quadratics, and span/support lemmas for EuclideanSpace.single-type vectors. Contributions of proofs for any milestone, and of the strongly convex lower bound (Theorem 3.15, not included here), are welcome.
Many planning problems are made in two stages: a first decision (capacity, inventory, a network design) is fixed before an uncertain demand is revealed, and a second decision (recourse, routing, overtime) is taken afterwards. Two-stage stochastic optimization models the demand as random and minimizes expected cost; its second stage is a whole policy , and the problem is intractable in general, especially with integer variables (Dyer and Stougie, 2006). Robust optimization instead picks one static pair that is feasible for every possible demand and minimizes its worst-case cost; it is a single deterministic mixed-integer program and needs no knowledge of the distribution (Ben-Tal and Nemirovski, 2002; Bertsimas and Sim, 2004).
The question this mission addresses is how much is lost by solving the robust problem in place of the stochastic one. Bertsimas and Goyal (Math. Oper. Res. 2010) show that when only the right-hand side is uncertain, the uncertainty set is symmetric and the distribution is centred at its point of symmetry, the loss is at most a factor of two, and that this factor is tight.
Fix , and nonnegative costs , . A set of scenarios carries a probability measure , and each scenario has a right-hand side . The uncertainty set is . First-stage variables are nonnegative, with integer values on a designated set of coordinates; second-stage variables are nonnegative reals ().
The stochastic problem , (1.1), chooses and a policy :
The robust problem , (1.2), chooses one for all scenarios:
A set is symmetric (Definition 1.2) if there is with for all ; is its point of symmetry. Hypercubes, ellipsoids and norm balls are symmetric. A probability measure on a symmetric set is symmetric (Definition 1.4) if it gives a set and its reflection the same mass.
If is symmetric with point of symmetry , , and satisfies
then
The result. The robust problem is one mixed-integer program, independent of ; the stochastic problem optimizes over policies and requires the distribution. Theorem 2.1 says that under symmetry the static robust solution used in every scenario is a 2-approximation of the optimal expected cost, for every centred distribution at once. The companion results of the paper show the hypotheses matter: the bound is tight for symmetric sets, the gap is unbounded (at least ) on the non-symmetric simplex (Theorem 2.6), and unbounded when costs are uncertain as well (Theorem 3.1). The theorem also underlies later work on the power of static and affine policies in adaptive optimization (Bertsimas and Goyal, 2012).
Formalizing it. The theorem and its proof are published; nothing in this mission is open mathematics. To our knowledge none of these statements has a machine-checked proof. The mission produces a reusable Lean model of two-stage stochastic and robust mixed-integer covering problems with arbitrary scenario spaces, extended-real optimal values and genuine expectations, together with the elementary geometry of point-symmetric sets. The same objects are used by the other missions of this series (the simplex and cost-uncertainty gaps, and the adaptability gap).
Each step of the published argument is short; the difficulty is in stating it at the right generality. The paper begins "consider an optimal solution" of ; optimal policies need not exist for an arbitrary scenario space, so the statement is about infima and every step must work for an arbitrary feasible pair. Passing from " for all " to "" needs integrability of the policy and of and linearity of the Bochner integral through a matrix. The bound uses symmetry together with nonnegativity of the uncertainty set; symmetry alone does not give it. Integrality of the second stage breaks the argument, since need not be integral.
Fin k → ℝ with the componentwise order, products A *ᵥ x and inner products c ⬝ᵥ x. The mixed-integer domain is "nonnegative with integer values on a set of coordinates", which is the paper's up to relabelling.Set.range b. Constraints hold for every scenario, not almost surely.EReal, equal to when infeasible; no attainment is assumed. A real-valued infimum would return on an infeasible robust problem and make the goal trivial; that formalization is ruled out.Contributions welcome: proofs of the milestones and the goal, and general lemmas on point-symmetric sets and on interchanging Bochner integrals with matrix–vector products, both reusable outside this mission.
Many constrained optimization problems in machine learning and statistics have a feasible set over which a linear function is cheap to minimize but a Euclidean projection is expensive: the -ball, the simplex, the nuclear-norm ball, the convex hull of a combinatorial family. Projected gradient descent needs a projection at every step. Conditional gradient descent, introduced by Frank and Wolfe in 1956 for quadratic programming, replaces the projection by a call to a linear minimization oracle over , and its iterates are convex combinations of oracle outputs, which makes them sparse when is a polytope.
This mission is the seventh of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015, arXiv:1405.4980v2). It covers Section 3.3, whose main result, Theorem 3.8, is the rate of the method in the form given by Jaggi (2013), going back to Dunn and Harshbarger (1978).
Let be a finite-dimensional real vector space with an arbitrary norm . For a linear form on , written , the dual norm is . Let be nonempty, compact and convex, with diameter .
Let be differentiable with gradient , a linear form on . For , is β-smooth with respect to on if
A point with is fixed throughout, and .
Given step sizes , a run of conditional gradient descent is a pair of sequences with and, for every ,
The minimizer need not be unique; any choice is allowed.
If is convex and -smooth with respect to and for , then every run satisfies, for every ,
Theorem 3.8 is the basic guarantee for projection-free first-order optimization. Its rate does not depend on the dimension, and it depends on the geometry only through the product , both measured in the same norm, which may be chosen to fit : for the -ball, smoothness in with dual norm gives much better constants than the Euclidean analysis. The book applies it this way to a LASSO-type problem (Section 3.3, pp. 274–276), and the same bound underlies the sparse-approximation corollary on the simplex (p. 273) and the many later variants of the method (away steps, stochastic and online conditional gradient).
The result is classical and proved in the book. What this mission adds is a machine-checked statement and proof in an arbitrary finite-dimensional normed space, with the dual norm as the operator norm on linear forms, and a reusable encoding of norm-smoothness and of conditional gradient runs. On Prove2Me a related result is already proved: Lan's Theorem 7.1 (First-order and Stochastic Optimization Methods), which bounds by with a different indexing; after the diameter bound it yields at Bubeck's iterate , which is weaker than Theorem 3.8 by one step.
The difficulty is in the bookkeeping of norms and indices, not in a deep idea. Inequality (3.4) is proved in the book only for the Euclidean norm, where and the Cauchy–Schwarz inequality is used; in a general norm it needs the pairing between a linear form and a vector and the bound . The rate is attained only by starting the induction at , where the step erases the dependence on the starting point; at the bound can fail, since is arbitrary. A first attempt that runs the induction from with an arbitrary does not give the stated constant.
is a type with [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]; nothing is specialised to the Euclidean norm. The gradient is an explicit derivative map f' : E → (E →L[ℝ] ℝ) with HasFDerivAt f (f' x) x for every x; is f' x v, and is the operator norm, which equals . is Metric.diam X, which equals the supremum of over because is compact. Sequences are indexed by ℕ with the first iterate at index 1.
Committed conventions: compact, convex and containing (hence nonempty); convexity of and the Lipschitz bound on the gradient are assumed on only, which is weaker than the book's global assumptions; ; the existence of the minimizer is the book's standing assumption (p. 242); the conclusion is stated for , as in the book. Runs are predicates: is any minimizer of the linear form over and is required, so the goal quantifies over every run with . A formalization in which need not lie in , or in which smoothness is assumed only along the iterates, states a different theorem and is excluded.
A complete development needs the descent inequality (3.4) for Fréchet derivatives in a normed space (reusable for every smooth method in the series and beyond), the fact that the iterates stay in , and a scalar induction. Proofs of the milestones are welcome independently; milestone 4 is a statement about real sequences only.
Gradient descent is a basic method for minimizing a differentiable function when evaluating its gradient is practical but solving the optimization problem directly is not. The rate at which its iterates approach an optimizer depends on the assumptions about the function. For a convex function with a Lipschitz gradient, the value error decreases at a sublinear rate. Adding strong convexity changes the behavior: the distance from the optimizer contracts at each step, giving an exponential bound on the value error. This section of Bubeck's monograph identifies a fixed step size that uses both the smoothness and curvature constants and gives the corresponding rate.
The result matters when a high-accuracy answer is needed. A sublinear bound makes each extra digit progressively more expensive; an exponential bound says that a fixed number of additional gradient evaluations reduces the error by a fixed factor. The theorem is a textbook result, already proved mathematically. This mission asks for its precise machine-checked statement and the source's supporting inequalities, rather than for a new optimization method.
Work in Euclidean space with , equipped with its usual inner product and norm. A differentiable function has gradient . It is -smooth when its gradient is -Lipschitz: for every . It is -strongly convex when, for every ,
The first condition limits how rapidly the gradient changes. The second gives a quadratic lower bound on the function around any point. Here and . In positive dimension, the two conditions together entail , so the condition number is at least one. The case remains part of the target.
A point is a global minimizer when for every . The book assumes such a point exists as a standing convention. A gradient descent run is a sequence satisfying at each positive index. Its first iterate is arbitrary. The step size in this mission is fixed at , rather than chosen by line search or adapted along the run.
The central target is Theorem 3.12 of Bubeck, p. 279. For every integer , the gradient descent run satisfies
At this is a smoothness bound on the initial value gap. For subsequent iterations it gives a linear convergence rate with the explicit exponential factor stated in the book. No initial-radius bound or bounded domain is imposed: the actual squared distance appears in the conclusion.
The milestones trace the mathematical claims stated in the source. Equation (3.6) is the co-coercivity inequality for gradients of convex smooth functions. The proof of Lemma 3.11 introduces , and identifies it as convex and -smooth. Lemma 3.11 combines curvature and smoothness into a sharper inequality for two gradients. The proof of Theorem 3.12 then gives a value-gap bound, a one-step distance contraction, and its iterated exponential form. These statements are separately useful: the co-coercivity and contraction bounds can be reused in analyses of related first-order methods.
The theorem states a complete guarantee for the algorithm: an explicit rule, the hypotheses on the objective, and a bound valid for every iteration count. It makes the role of visible. When is close to one, the contraction is strong; when the smoothness constant is much larger than the curvature constant, more iterations are needed for the same error reduction. The stated dependence supports comparisons with projected and accelerated gradient methods elsewhere in the same monograph.
Formalizing the result requires a common interface for actual gradients, smoothness, strong convexity, and algorithm runs. The strong-convexity predicate is an existing published definition, while the local smoothness and run definitions use Bubeck's conventions. Once these interfaces and the inequalities are proved, later missions can use the resulting declarations to compare rates without translating between informal meanings of “smooth” or changing the iterate index. The source provides a mathematical proof; these draft Lean theorems carry sorry and do not yet constitute machine-checked proofs.
The main issue is getting the sharp contraction factor from two assumptions that control different parts of the gradient step. A direct Lipschitz estimate on the update map does not by itself express the mixed inner-product term with the constants needed for the stated factor. Lemma 3.11 is the source's precise bridge between the gradient difference, the point displacement, and their inner product. The case also needs to remain valid: a proof route that divides by cannot cover that boundary by the same calculation.
The last display in the proof of Theorem 3.12 joins a one-step inequality involving to an exponential inequality involving . The latter is the cumulative statement after steps. Keeping these as separate milestones makes each quantified claim explicit while preserving the theorem's bound.
Lean represents as EuclideanSpace ℝ (Fin n), with . The gradient is an explicit map required to be the actual gradient of at every point. Smoothness is the gradient Lipschitz condition, not a quadratic upper bound used as a definition. Strong convexity uses the published OnlineConvexOpt.ConvexBasics.StronglyConvexOn predicate on the whole space; its formula is the book's (3.13). Iterates are indexed from one, and index zero imposes no condition. The norm, inner product, constants, and real exponential follow the printed formulas.
The added explicit conditions are , , and where Equation (3.6) divides by . Positive dimension excludes a degenerate space where curvature imposes no restriction on smoothness. The positivity of makes meaningful; the source treats it as a positive strong-convexity parameter. The minimizer hypothesis is the book's standing convention. There is no assumption that : that property follows from global minimality and differentiability. A gradient map unrelated to would trivialize the model, so the smoothness definition includes the gradient identity.
The local development needs Euclidean inner-product identities, convexity, differentiability, Lipschitz gradient bounds, and real exponential estimates. The auxiliary function and the two co-coercivity inequalities are reusable outside this chapter. Contributions should prove the exact milestone statements and the final theorem, including and , without weakening constants or substituting another gradient descent step.
A shortest path problem asks how to reach a destination at minimum cost. In a stochastic shortest path problem, a decision at a state selects a probability distribution over successor states, so both the route and its total cost are random. Costs may have either sign. This makes the problem relevant to finite-state control models where rewards and expenses occur before eventual termination. Bertsekas and Tsitsiklis analyze this setting without requiring all one-stage costs to be nonnegative or all to be nonpositive. Their condition instead rules out an improper stationary policy whose costs stay finite from every initial state. Bertsekas and Tsitsiklis (1991), pp. 580–583.
Earlier treatments established Bellman-equation and algorithmic conclusions under positive or nonnegative costs. The 1991 paper traces the finite-control development from Eaton and Zadeh and the compact-control extension from Kushner, then removes the sign restriction while retaining finite state space. It also explains why the Bellman mapping need not contract when an improper policy is available. Bertsekas and Tsitsiklis (1991), pp. 581, 585. A separate, proved Prove2Me theorem from Bertsekas's textbook treats the special case in which every policy is proper and controls are finite; the result here permits improper policies and compact control spaces.
There are states. State is the destination. At state , a control incurs a real cost and moves the process to state with probability . A selector chooses one control at every state. A policy may change selectors over time; a stationary policy repeats one selector. The matrix has entries , and is the vector of one-stage costs. Bertsekas and Tsitsiklis (1991), p. 582.
The cost vector is the coordinatewise limit inferior of expected partial costs, including the possibility of infinite values. The optimal cost is the infimum of over all policies, including nonstationary ones. Optimality of a policy means it attains that infimum from every initial state. The fixed-selector operator is ; the Bellman operator takes the coordinatewise infimum of these vectors over selectors. Bertsekas and Tsitsiklis (1991), pp. 582–583, equations (2)–(6).
A stationary policy is proper when its probability of reaching state tends to one from every starting state. Assumption 1 says state is absorbing and cost-free, at least one proper stationary policy exists, and every improper stationary policy has a partial-cost coordinate tending to . Assumption 2 makes each control space compact, each cost function lower semicontinuous, and each transition-probability coordinate continuous. Work takes place in . Bertsekas and Tsitsiklis (1991), pp. 583–584.
Under Assumptions 1 and 2, the optimal cost is finite and is the unique fixed point of in . Every initial has
A stationary selector is optimal exactly when ; an optimal proper stationary selector exists. These are all clauses of Proposition 2, rather than separate targets selected from it. Bertsekas and Tsitsiklis (1991), p. 586, Proposition 2.
The milestone list follows the source's Proposition 1, Lemmas 1–3, and the numbered equations used by their proof. Proposition 1 supplies a weighted maximum-norm contraction when every stationary policy is proper. Lemma 1 describes fixed costs of a proper policy and characterizes properness through a Bellman inequality. Lemma 2 gives continuity of . Lemma 3 controls limits of proper policies; its second part detects a limit that becomes improper through diverging costs. Appendix equations (22) and (24), and the policy-improvement equation (15), provide the paper's intermediate targets. Bertsekas and Tsitsiklis (1991), pp. 585–587, 591–592.
Proposition 2 identifies the cost of the best policy by a finite-dimensional Bellman equation even though the definition of optimal cost ranges over all, possibly nonstationary, policies. Its convergence clause justifies value iteration from any vector whose destination coordinate is zero. Its policy criterion and existence clause connect a fixed point to an implementable stationary decision rule. The paper applies these conclusions to successive approximation and policy iteration in §4. Bertsekas and Tsitsiklis (1991), pp. 586, 590–591.
The paper proves these statements. This mission seeks machine-checked proofs of their exact finite-state formulation and of the listed intermediate results. The resulting finite stochastic-matrix, hitting, and policy-cost infrastructure can also support other undiscounted control problems. The related proved Prove2Me result for the all-proper finite-control case does not settle this mission's compact-control or improper-policy cases.
When every stationary policy is proper, a common weighted maximum norm makes the Bellman mapping contract. An improper policy can destroy this route: Figure 2 has an absorbing destination and satisfies both assumptions, yet is not a contraction in any norm on . The main result therefore needs a way to retain fixed-point uniqueness and convergence without a uniform contraction rate. Compactness matters because a sequence of proper selectors may converge to an improper selector; Lemma 3 explains the associated cost behavior. Bertsekas and Tsitsiklis (1991), pp. 585–586, 591–595.
States are Fin n, with the paper's state represented by 0; the model requires . A control set is a type with a metric, with compactness asserted for its whole carrier. Transition rows explicitly have nonnegative entries summing to one. These are the probability-vector conditions implicit in the word “probability.” Assumption 1 supplies a selector and therefore nonempty control sets. The paper writes ; where a theorem uses only Assumption 1, finite real Bellman infima are made explicit through TRealValued. Under Assumption 2, compactness and lower semicontinuity give real attained minima. Bertsekas and Tsitsiklis (1991), pp. 582–584.
Policy costs and their infimum use extended reals so that an improper policy's cost is represented without a default finite value. Proposition 2 concludes, rather than assumes, that has real coordinates. Its policy infimum ranges over every sequence of selectors. Matrix products use the identity at time zero; is the identity. The destination-zero restriction is retained in every fixed-point and iteration claim. Defining optimal cost as a Bellman fixed point, or restricting the infimum to stationary policies, would remove the result the paper proves. Solvers can contribute the finite-chain, matrix-inverse, semicontinuity, and convergence arguments needed by these targets.
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 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 .