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.
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?
Vertex connectivity measures how robust a network is against the failure of nodes. It can be measured in two ways that look different. One way counts the fewest nodes whose removal disconnects the network. The other counts the routes between two nodes that share no intermediate node. Whitney's theorem (1932) says that the two measures agree for every pair of nodes. It is the vertex form of Menger's theorem, and it underlies reliability analysis of communication and transportation networks, the design of fault-tolerant routing, and much of structural graph theory.
M. L. Balinski's 1961 paper On the graph structure of convex polyhedra in n-space proves that the graph of a bounded full-dimensional polyhedron in -space is -tuply connected (the subject of Mission I of this series). It then invokes Whitney's theorem to conclude that any two vertices of such a polyhedron are joined by disjoint paths. Balinski gives a short new proof of Whitney's theorem through the max-flow min-cut theorem of Ford and Fulkerson and of Dantzig and Fulkerson. That makes the theorem a consequence of linear programming duality. This mission formalizes that part of the paper: the network vocabulary, the max-flow min-cut theorem with capacities on both points and lines, the integrality of maximum flows, and Whitney's theorem itself.
Timeline.
A graph consists of a finite set of points and a set of lines, each line being a pair of distinct points. A path from to is a sequence of lines with , and . Paths are disjoint if they have no point in common except possibly their first and last points.
is -tuply connected if it has at least points and, for every set of fewer than points, the graph remaining after deleting is connected. has disjoint paths from to if there are pairwise distinct paths from to , none of which repeats a point, and no two of which share a point other than and .
A network is a connected graph with a capacity on every point and on every line, and with a distinguished source and sink . A flow assigns a number to every path from to , such that for every point and every line
Its value is . A disconnecting set is a pair of points and lines that meets every walk from to . Its value is .
The unit network of the proof has capacity on every point except and , and capacity on every line except the line (if present), which has capacity . In Lean these are IsNTuplyConnected, HasNDisjointPaths, IsFlow, flowValue, IsDisconnecting, cutValue, unitCapV and unitCapE, all in the namespace Balinski61.Whitney.
For a finite graph with at least two points and any :
Both directions are part of the goal.
Whitney's theorem turns a statement about all small deletion sets into the existence of explicit, verifiable path systems, and back again. In applications it certifies connectivity by exhibiting paths, and it certifies that connectivity is no larger by exhibiting a separating set. It is the base of the theory of -connected graphs: ear decompositions, the fan lemma, and the structure of minimally -connected graphs all use it. Inside this paper it supplies the COROLLARY that any two vertices of a bounded full-dimensional polyhedron in -space are joined by disjoint edge paths.
None of these results is formalized for vertex connectivity at this Mathlib revision. Mathlib has edge connectivity and connected components but no vertex Menger theorem. The Prove2Me library has max-flow min-cut statements for arc capacities only and integrality results for basic solutions of network LPs, but no flow model with capacities on points. A completed development gives a reusable vertex-capacitated max-flow min-cut theorem for undirected graphs and the first machine-checked Whitney theorem in this library. The results are classical and proved; the remaining work is the formalization.
The sufficiency direction is elementary. The necessity direction needs a global object (a flow, or a family of paths) to exist from purely local hypotheses about deletions. The obvious induction on , which deletes a point and applies the hypothesis to a smaller graph, does not keep the path systems disjoint. In Balinski's route the weight falls on max-flow min-cut and integrality for path flows with capacities on points, neither of which exists in the library. A second difficulty sits in a case the paper's proof skips: a disconnecting set of the unit network may use the line (capacity ) together with up to points, and the deletion hypothesis of -tuple connectedness speaks only about points.
Graphs are Mathlib SimpleGraphs on a Fintype with decidable equality and adjacency. Paths are walks with IsPath. A flow is a real function on the finite type G.Path ps pk of simple paths; "through a point" and "through a line" mean membership in the walk's support and edge list. Capacities are functions V → ℝ and Sym2 V → ℝ. Nonnegativity, connectivity of and are hypotheses of the network theorems.
The following readings of loose phrases are explicit in the statements:
The max-flow min-cut milestone states that the maximum and the minimum are attained. A statement that only bounds some flow by every cut is satisfied by the zero flow. A connectivity notion without the point count would make every complete graph -connected for all . Both trivializations are excluded.
Contributions welcome: a vertex-capacitated augmenting-path or LP-duality proof of max-flow min-cut for path flows, integrality by an augmenting-path argument, the unit-network lemmas, and direct combinatorial proofs of Whitney's theorem that bypass flows.
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.
The vertices and edges of a convex polytope form a graph, and much of polyhedral combinatorics and of the theory of the simplex method is about that graph: how far apart two vertices can be (the Hirsch question), which graphs arise (Steinitz's theorem in dimension 3), and how robust the graph is. In 1961 M. L. Balinski proved that the graph of a full-dimensional polytope in -space cannot be disconnected by deleting fewer than vertices (Pacific J. Math. 11 (1961) 431–434). The result, now called Balinski's theorem, is a standard entry in textbooks on polytopes (Grünbaum, Convex Polytopes, §11.3; Ziegler, Lectures on Polytopes, Thm 3.14) and is the starting point of the study of connectivity of polytope graphs. Its proof uses only linear programming: the improving-edge step of the simplex method and the connectivity of the graph of a face.
Timeline. Steinitz (1922) characterised the graphs of 3-polytopes as the 3-connected planar graphs, so the case is contained in his theorem. Balinski (1961) proved -connectivity in every dimension. Whitney (1932) had shown that -connectivity is equivalent to the existence of disjoint paths between any two points; Balinski gives a new proof of that equivalence through max-flow min-cut and draws the corollary that any two vertices of a full-dimensional polytope in are joined by disjoint edge paths.
Fix integers (the dimension of the space) and (the number of inequalities), vectors (the rows of a matrix ) and . Balinski's system (1) describes
written Hirsch.Hpoly a b in Lean. The paper assumes throughout two standing assumptions (StandingAssumptions a b):
A vertex of is an extreme point. An edge is a segment , , that is an extreme subset of (Hirsch.Adj S u v). The graph (polyGraph S) has the vertices as points and the edges as lines.
A graph is -tuply connected (IsNTuplyConnected G n) if it has at least points and remains connected after dropping out any or fewer points. Two points are joined by disjoint paths (HasDisjointPaths G u v n) if there are distinct paths from to which share no point other than and .
That is, and is connected for every set of at most vertices.
Hirsch.face_connected.The result. Balinski's theorem says that polytope graphs are highly connected, which constrains which graphs can be graphs of -polytopes and is the base case of later results on the connectivity of polytope graphs. Together with Whitney's theorem it gives vertex-disjoint edge paths between any two vertices. The improving-neighbour step is the local optimality criterion of the simplex method.
Formalizing it. The theorem is classical and proved; it has not been formalized. On this platform the case (the graph of a polytope is connected) is proved as Hirsch.graph_connected_general, and connectivity of the graph of each face as Hirsch.face_connected, both by Shuze Chen; LinearOptimization.polyhedron_bounded_convex_hull_extreme proves the convex-hull clause of milestone 1 for a matrix-form polyhedron under the hypotheses "nonempty and bounded", and ConnPreservingHamPath.IsKConnected.le_ncard_neighborSet proves "connectivity at most minimum degree" for its own notion of -connectivity. This mission adds vertex -connectivity in every dimension, the simplex improving-neighbour lemma for H-polytopes, and the corollary on disjoint paths. The corollary needs Whitney's theorem, which is the goal of the companion mission On the Graph Structure of Convex Polyhedra in n-Space II.
An induction on dimension through facets does not directly control where the deleted vertices lie. Balinski's argument leans on several facts the paper calls obvious or clear: that a vertex with no improving neighbour is optimal, that the graph of a face is connected, that points of lie on a common hyperplane while does not, and that has at least vertices. Each needs its own development from the two algebraic assumptions, in particular the passage from (i)–(ii) to a bounded full-dimensional polytope with finitely many vertices, and the identification of extreme segments with edges. Deleting fewer than vertices, which the definition requires and the proof's text does not treat, needs a separate argument. The proof also tacitly needs the affine function to take a nonzero value at some vertex.
EuclideanSpace ℝ (Fin n); rows a : Fin m → EuclideanSpace ℝ (Fin n), b : Fin m → ℝ. The published Hirsch_model names the dimension d and the number of rows n; here is the dimension, as in the paper.Set.extremePoints ℝ S; edges are Hirsch.Adj (extreme segments). is a SimpleGraph on the vertex subtype.Set.encard; " or fewer points" is X.encard < n. A path of the paper is a Mathlib Walk (consecutive points distinct).Hirsch.face_connected; the affine function of the proof is an arbitrary , and only the "maximum"/"" forms are stated (the others follow for ); "at least disjoint paths between any pair of vertices" is a family of pairwise distinct paths without repeated points, sharing only their endpoints, between two distinct vertices.Hirsch walk vocabulary and Mathlib Walks; all are reusable beyond this mission.Many controlled queueing, inventory and maintenance systems are modelled as controlled Markov processes (CMPs) on a countable state space whose one-stage cost grows without bound: the holding cost of a queue grows with its length. For such systems the natural performance measure is the long-run average cost, and the basic question is whether some simple policy, one that looks only at the current state and never randomizes, is optimal among all policies, including those that use the whole history.
When the cost is bounded, the classical answer goes through a bounded solution of the average cost optimality equation (ACOE). For unbounded costs, bounded solutions are rare: in many queueing models the relative value function grows with the state, and growth conditions such as (5.2) of the survey may fail (Arapostathis et al. 1993, p. 307). Sennott (1986; 1989) replaced boundedness by one-sided conditions on the discounted value functions, which are often easy to verify for queueing models because the relative values are bounded below. This mission formalizes Sennott's existence theorem in the form given in the survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus, Theorem 5.9.
Timeline. For bounded costs, Ross (1983, the survey's Theorem 5.2) obtained a bounded ACOE solution, and with it an optimal stationary policy, when the differential discounted values are uniformly bounded. Federgruen, Hordijk and Tijms (1979) treated unbounded costs under Lyapunov-type recurrence conditions, which restrict how fast the cost may grow (survey, Remark 5.7). Sennott (1986, 1989) replaced these by a uniform lower bound and a pointwise, one-step integrable upper bound on the differential discounted values. The survey (1993, Theorem 5.9) states the result with compact action sets and continuous data, and Sennott's 1999 book (§7.2) gives the finite-action version in textbook form.
The state space is . For each state the set of admissible actions is a nonempty compact subset of a metric space . Choosing in state costs , and the next state is with probability . For fixed , the maps and are continuous on .
An admissible policy chooses the action at time according to a probability distribution concentrated on , where is the history; it may use the whole history and may randomize. A stationary deterministic policy is a map with , applied at every step. Given an initial state and a policy , the states and actions form a stochastic process with law and expectation .
For , the discounted cost and the average cost of from are
both in . The optimal values are and , and the differential discounted value is . A policy is AC-optimal if for every .
Sennott's conditions (Assumptions 5.14–5.16) are:
The goal asserts only existence. It does not fix the optimal cost, and it does not claim that the optimal cost is constant or that an optimality equation holds.
The result. Theorem 5.9 is the standard existence theorem for average-optimal stationary policies with unbounded costs on countable state spaces. Its conditions are verified routinely for controlled queues, where relative values are monotone in the queue length and hence bounded below. It shows that randomization and memory do not reduce the long-run average cost, and the ACOI it produces is the starting point for value and policy iteration and for structural results such as threshold policies.
Formalizing it. The theorem is proved in the literature (Sennott 1989; Sennott 1999, Theorem 7.2.3; survey, p. 308). It has no machine-checked proof. The finite-action version, SennottDP.SEN.thm_7_2_3_sen_acoi, is posed on Prove2Me and still open; this mission poses the compact-action version, which needs continuity and compactness arguments that the finite case avoids. A formal proof also requires a general theory of history-dependent policies on path space (Ionescu-Tulcea), the discounted optimality equation with unbounded costs, and the passage from Abel to Cesàro means. All three are reusable well beyond this paper.
The obvious argument lets in the discounted optimality equation (5.6). Two steps fail without more structure. First, need not converge, and with unbounded costs it is not uniformly bounded, so the limit has to be taken pointwise along a subsequence, with only a lower bound uniform in the state. Second, the limit cannot be passed through the infinite sum by dominated convergence, because no integrable dominating function exists for every action. Only an inequality survives (Fatou), so the limit is an ACOI, not an equation. The inequality then has to be turned into optimality against all of , which includes history-dependent randomized policies whose costs are not described by any optimality equation. The lower bound for these comes from comparing Cesàro and Abel means, not from dynamic programming.
The Lean development uses the following representation and conventions.
ℕ. The action space is a metric space with its Borel σ-algebra. U i is nonempty and compact, c is measurable and nonnegative on admissible pairs, P is a Markov kernel, and , are continuous on .limsup in .A trivializing formalization is excluded. Sennott's conditions are satisfiable (a one-action, zero-cost model satisfies all three), and AC-optimality is measured against all admissible policies, so the goal cannot hold vacuously or by a junk value.
Welcome contributions: the Markov property of the path measure for history-dependent policies; the discounted optimality equation for nonnegative unbounded costs; a measurable-selection or compactness argument for minimizing actions on compact ; Fatou's lemma for series with converging weights; and the Abelian inequalities in a form applied to expected costs.
In multiclass classification a learner sees examples with in a domain and a label in a set , and must predict labels of new points. When is finite, the Natarajan dimension characterizes PAC learnability, extending the role of the VC dimension in binary classification (Natarajan 1989; Ben-David, Cesa-Bianchi, Haussler, Long 1995). Label sets in practice are often unbounded: structured prediction, ranking, and language modelling all predict from very large or infinite label spaces. For infinite the Natarajan dimension fails to characterize learnability, and the question of which combinatorial parameter does was left open by Daniely and Shalev-Shwartz.
Timeline:
A concept class is a set of functions. For a sequence the projection is the set of label words , . A finite non-empty set is a pseudo-cube if every has, in every coordinate , a neighbour that differs from exactly in coordinate . The sequence is DS-shattered if contains an -dimensional pseudo-cube, and the DS dimension is the maximum length of a DS-shattered sequence. The Natarajan dimension is the same with Boolean cubes , , in place of pseudo-cubes.
A sample is -realizable if some is consistent with it. An sample compression scheme for (Littlestone and Warmuth 1986) is a single reconstruction function such that every realizable sample of size contains of its examples with consistent with the whole sample. Logarithms are base throughout.
For with and , and all integers , there is an sample compression scheme, , with
The scheme combines two components, each with its own chain of results:
Theorem 36 is the algorithmic heart of the characterization: by the standard "compression implies generalization" argument it gives PAC learnability of every class of finite DS dimension, with sample complexity in the realizable case (), and with the agnostic case following by known reductions. It also exhibits sample compression schemes of size polylogarithmic in for multiclass classes with infinitely many labels, in contrast to the constant-size schemes known for finite VC classes.
The result is proved in the paper; none of it is formalized. The formalization would produce a machine-checked theory of one-inclusion graphs and their orientations, multiclass shifting, the exponential dimension, list learning, and sample compression schemes for arbitrary label sets. These objects recur throughout learning theory (one-inclusion graphs in optimal PAC learning, shifting in VC theory), so the infrastructure is reusable beyond this mission.
The natural first idea, running empirical risk minimization or bounding the Natarajan dimension, fails: classes with Natarajan dimension and infinitely many labels can be unlearnable, and ERM can fail even for learnable classes. The DS dimension gives only a weak guarantee: by Claim 16, among leave-one-out runs, one is correct. Turning this into a learner requires a list learner whose menus are still of unbounded total size, and then learning with a menu of size , where the obstacle is controlling one-inclusion graph orientations over by the Natarajan dimension. Multiclass shifting does not preserve the average degree (Example 20), so the binary argument breaks down, and a new potential () and a new dimension () are needed. Lemma 13 for infinite classes needs a compactness argument.
Lean conventions:
H : Set (X → Y) with arbitrary types X, Y; sequences and samples are functions on Fin n ( is 0-based).ℕ∞, so unbounded families give ⊤; hypotheses are written dsDim H = dDS with dDS : ℕ. A pseudo-cube is required to be finite.Real.logb 2. Menu sizes use Set.encard.∃ ρ, ∀ S, ∃ S'); a subsample may repeat and reorder examples. Theorem 36 states explicitly.Fin p; the shifting condition becomes .PMF), and i.i.d. probabilities are sums over . The measure-theoretic generality of the paper is not attempted.A trivial formalization is ruled out by these choices. Placing the reconstruction function after the sample would let it output the consistent hypothesis. A dimension in ℕ defined by sSup would be for infinite dimension. Pseudo-cubes without finiteness would change the dimension (Example 8).
Contributions welcome: proofs of any milestone, in particular the shifting results of §3 (self-contained combinatorics on finite classes), Fact 14 (pure discrete probability), and Lemma 13; general-purpose lemmas about one-inclusion graphs, orientations and sample compression schemes are reusable by other learning-theory missions.
A seller with a fixed stock of a single product and a finite selling season must post prices without knowing how demand responds to price. Revenue management treats this as a constrained stochastic control problem; with the demand curve known, the problem was solved by Gallego and van Ryzin (Management Science, 1994). When the curve is unknown, every price posted also serves as an experiment, so the seller faces an exploration–exploitation trade-off. Unlike a multi-armed bandit, this problem has a continuum of actions and a hard inventory constraint.
Besbes and Zeevi (Operations Research, 2009) measure a pricing policy by its worst-case relative revenue loss against a full-information benchmark, in an asymptotic regime where inventory and demand grow together. They give three upper bounds. This mission takes the third, Proposition 5: when the demand model has a single unknown scalar parameter, a policy that keeps re-estimating that parameter in stages of growing length has regret . The paper's lower bound for parametric families (Proposition 4) is of order , so the rate is optimal up to logarithmic factors.
Market. Prices lie in with . Posting the off price stops demand. The seller starts with inventory and sells over the horizon , .
Demand. A demand function maps a price to a demand rate. The class consists of the functions that are non-increasing with an inverse on , have a concave revenue rate , are bounded by , are -Lipschitz with a -Lipschitz inverse, and attain a revenue rate . The parametric family is , , with every member in the class (Assumption 1). Assumption 2 adds a test price , differentiability of and the Lipschitz bound . Assumption 3 requires and an -Lipschitz solution map of the equation .
Demand process. Let be a unit-rate Poisson process. Under a price path and parameter , the cumulative demand up to time is . Sales stop when the inventory runs out.
Benchmark and regret. The deterministic relaxation is the supremum of over price paths with . In the market of size the inventory is and the demand . If is the expected revenue of a policy , its regret is .
Algorithm 3. Start from and use stages of lengths summing to . Stage applies , estimates the demand rate from the stage's demand, solves for , and sets . Here maximizes and minimizes . The tuning (19)–(20) is stages with and .
The constants are uniform in and . This is the paper's (21): .
Milestones 6–8 hold in the case , the only case the paper's proof treats in detail.
Proposition 5 shows that with one unknown parameter, learning while earning reaches the rate, up to logarithms. The learn-then-price policies of Propositions 1 and 3 stop learning after an initial phase and reach only and . The paper leaves open whether the multi-parameter case attains the lower bound.
The analysis combines a continuous-time controlled Poisson model, an inventory constraint and a staged estimator, which also appear in later work on dynamic pricing with learning. A formal development would provide a time-changed Poisson demand model with random stage boundaries, a deterministic-relaxation benchmark, and concentration bounds stated for the scales this literature uses.
The result is proved in the paper, but parts of the proof are only sketched. The case is dismissed with "a similar result holds". The per-stage gap is obtained "by parallel reasoning". Display (A-30) has a typographical error in its threshold. To our knowledge, none of these results has been machine-checked.
The naive argument conditions each stage on its start time, as if that time were deterministic. It is not: the stage boundaries depend on all earlier observations, so every per-stage estimate needs the strong Markov property of the Poisson process at a random time. The inventory constraint makes the revenue a nonlinear function of the whole demand path. Bounding the loss therefore means controlling estimation error and overflow at the same time. The geometric stage lengths (20) are chosen so that the stage losses are all of the same order. That balance has to be checked exactly, including the rounding of to an integer.
Function.invFunOn. is a nonempty closed interval of .Contributions are welcome on every milestone. The Poisson process structure, its strong Markov property at stage boundaries, and Lemma 2 can be reused in other Poisson-demand pricing and queueing missions. Lemma 1 and Fact 1 are deterministic, and the rate estimate already has a local proof.
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.
Single-machine scheduling with precedence constraints, written in the notation of Graham et al., asks for an order of weighted jobs on one machine that respects a given partial order and minimizes the weighted sum of completion times. The problem is strongly NP-hard (Lawler 1978; Lenstra and Rinnooy Kan 1978), and closing its approximability gap is listed by Schuurman and Woeginger among ten outstanding open problems in scheduling theory. Several 2-approximation algorithms are known (Schulz 1996; Hall et al. 1997; Chudak and Hochbaum 1999; Chekuri and Motwani 1999; Margot et al. 2003).
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 precedence order. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) observed that this graph is the graph of incomparable pairs of dimension theory, and used that identification to obtain -approximations for orders of fractional dimension at most . This mission formalizes that framework: the identification of the two graphs and the rounding guarantee of the paper's Theorem 5.1.
An instance consists of a finite set of jobs, a partial order on (reflexive, antisymmetric, transitive; with means job finishes before job starts), processing times and weights .
Two jobs are incomparable, , when neither nor lies in . The set of incomparable pairs consists of ordered pairs and is closed under swapping. A linear extension of is a linear order on ; it reverses when in . A nonempty multiset of linear extensions is a -realizer if every incomparable pair is reversed by at least of them. The fractional dimension is the least ratio over all -realizers.
The vertex cover graph has the incomparable pairs as nodes; nodes and are adjacent if and , or and , or (symmetrically closed). Node has weight , and . is the minimum weight of a vertex cover of . The LP relaxation [CS-LP] asks for with on every edge, minimizing . For a solution write , and for a linear extension let be the pairs of reversed in .
The graph of incomparable pairs (Felsner and Trotter 2000) also has the incomparable pairs as vertices; two of them are adjacent when the pair of them is a minimal set of incomparable pairs that no linear extension reverses entirely.
For an instance , a -realizer of , and a half-integral optimal solution of [CS-LP], put . Then every is a vertex cover of , and
The result. Combined with the cited Theorem 2.1 (Ambühl–Mastrolilli 2009; Correa–Schulz 2005), which turns an -approximate vertex cover of into an -approximate schedule, Theorem 5.1 gives a -approximation for whenever the precedence order has an efficiently samplable realizer with . The paper applies it to interval orders (), convex bipartite orders and semiorders (), orders of bounded degree and orders of interval dimension two; for the earlier special classes it matched or improved the best known ratios, and for the last two it gave the first results. Proposition 3.2 makes the dimension theory of posets (realizers, critical pairs, fractional dimension) directly available to the vertex cover approach.
Formalizing it. The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. The mission produces a Lean development of incomparable pairs, linear extensions, -fold realizers and the hypergraph of incomparable pairs, which other dimension-theory missions can reuse, and a verified LP-rounding argument for half-integral vertex cover solutions under a distribution of independent sets.
Most of the rounding argument is arithmetic over finite sums. The central nontrivial step is the inclusion in Proposition 3.2: for two incomparable pairs that are not adjacent under the three-case rule, one must construct a single linear extension reversing both. This needs an extension of by two new comparabilities whose transitive closure is still antisymmetric, followed by Szpilrajn's theorem; checking that every potential cycle is excluded by the three cases is the actual content. The opposite inclusion, and footnote 4, follow from transitivity and antisymmetry of linear orders. A second point of care is the inequality used in step (7): it is not part of the definition of a realizer, and follows from each linear extension reversing exactly one of and .
N; the precedence order is a relation P : N → N → Prop with IsPartialOrder, carried by the structure Instance. Processing times and weights are nonnegative reals.IncPair P of N × N; a linear extension is a relation with IsLinearOrder containing P; a -realizer is a family Fin t → LinearExtension P with . Reversal of means in throughout; the page's "" in Eq. (4) and "" in Eq. (5) are the same family of inequalities because is symmetric.Contributions welcome: proofs of the milestones in any order, and a reusable Szpilrajn-style lemma producing a linear extension that reverses a prescribed set of compatible incomparable pairs.
Interior point methods solve linear programs in a number of arithmetic operations polynomial in the bit length of the input (Karmarkar 1984). Whether linear programming admits a strongly polynomial algorithm, one whose number of arithmetic operations is bounded by a polynomial in the number of variables and constraints alone, is open; it is the ninth of Smale's problems for the next century (Smale 1998/2000, see the references). A natural question is whether some interior point method is strongly polynomial. Primal-dual path-following methods follow the central path of a log-barrier problem and are the methods used in practice.
Allamigeon, Benchimol, Gaubert and Joswig (arXiv:1708.01544, SIAM J. Appl. Algebra Geom. 2018) gave such a family. For linear programs with variables and constraints, every path-following method that stays in the wide neighborhood of the central path needs at least iterations once is large enough. The same family disproves the "continuous Hirsch conjecture" of Deza, Terlaky and Zinchenko (DTZ09, see the references) on the total curvature of the central path. That curvature result is the subject of a separate mission. This mission formalizes the iteration bound.
For a real matrix , , and , the paper considers the linear program in slack form and its dual,
A primal-dual point is . The set of strictly feasible points consists of the with all coordinates positive that satisfy both equality systems. The duality measure is
and for the wide neighborhood of the central path is
The central path itself is the set of points where all products , are equal. The neighborhood bounds the products only from below. It contains the and neighborhoods used by short-step, long-step and predictor-corrector methods.
The instance is , for and :
With slacks it becomes with , , . Its wide neighborhood is written . A polygonal curve is a union of segments, and it is contained in the neighborhood when every point of every segment is.
The milestones use the tropical semifield with and . The tropical segment is the set of points with . The Funk metric is , with and the directed Hausdorff distance . Finally, is applied coordinatewise, with .
Let and , and suppose that
If a polygonal curve is contained in with and , then
The threshold (36) is the paper's own explicit constant. Corollary 31 (Theorem B of the introduction) restates the result for algorithms. Any method whose iterates and the segments joining them stay in the wide neighborhood performs at least iterations to reduce the duality measure from to .
The theorem shows that the iteration count of a large class of primal-dual log-barrier interior point methods cannot be bounded by any function of that grows more slowly than , uniformly in the data. The class includes the methods of Kojima–Mizuno–Yoshise, Monteiro–Adler and Mizuno–Todd–Ye. No such method is strongly polynomial. The constraint matrix of is fixed by and alone, so the bound concerns the combinatorial dimension, not the bit length. The only property of the method used is that its trajectory stays in . The lower bound therefore applies to every method with that property, whatever rule chooses its steps.
The result is proved in the paper; no machine-checked proof of it or of its tropical ingredients is known. A formalization would check the explicit threshold (36), which the paper derives in a few lines from bounds on Puiseux polyhedra. It would also produce reusable statements about tropical segments, the Funk and Hilbert metrics on , and determinants of monomial matrices.
Following the central path is not hard in principle: the obvious argument tracks the duality measure, which decreases by a constant factor per iteration in a neighborhood of the path. That argument gives only upper bounds. The lower bound requires showing that the neighborhood itself, for large , is too thin to be crossed in a few straight steps, uniformly over every possible trajectory. The paper does this by passing to the limit on logarithmic scale. The image of under collapses onto a piecewise-linear tropical central path, and a segment of becomes, up to , a tropical segment. The tropical central path of then has to be shown to need tropical segments. The limit argument has to be made quantitative at a finite, explicit . That is where the Puiseux-series machinery (Theorems 12, 15 and 19 of the paper) and the explicit constant enter.
Everything is stated over and ; the goal typechecks without the field of Puiseux series. A primal-dual point is an element of . The dual equation is with Mathlib's transpose, divides by (equal to for ), and the wide neighborhood is one-sided. The instance matrix is generated from the paper's 1-based row and column numbers; Lean indices are 0-based. A polygonal curve is a map with segment ℝ (z i) (z (i+1)) ⊆ N. The power in (36) is a natural-number power and the factorials are natural-number factorials. is WithBot ℝ, and distances that can be infinite take values in EReal, with the convention encoded explicitly.
Two statements are repaired or restated. Lemma 11 is printed for all , but its first inequality fails for (for at ), so it is stated for . Lemma 8 makes explicit its implicit hypotheses and . Proposition 20 is stated in the form its proof establishes, as the greatest point of a tropical polyhedron. Its identification with the valuation of the Puiseux central path is not part of the item. Monomial matrices are given by sign and exponent matrices, and the valuation of the determinant is computed from the permutation expansion.
A trivializing formalization is ruled out: is not empty, since the build includes a sorry-free proof that it contains an explicit point for , , . A curve with cannot satisfy both duality-measure conditions, since .
The paper's Puiseux-series results are not posed: Theorems 12, 15, 19 and 29, Propositions 14, 16, 21 and 28, Corollary 17, and the count of §6.2. They need a faithful model of the field of absolutely convergent generalized Puiseux series and of the tropical central path. Contributions of that infrastructure, and of these statements as further milestones, are welcome. So are proofs of the five milestones, which need no Puiseux series. Proposition 1, Lemma 5 and Proposition 20 are elementary, and Lemma 8 and Lemma 11 are estimates with explicit constants.
Robust optimization replaces uncertain data by a set of possible values and requires a decision to work for every value in that set. A central question is how to choose the set from data so that robust feasibility also gives a specified chance of satisfying the original constraint. Bertsimas, Gupta, and Kallus study this question for several sampling models in Data-Driven Robust Optimization. Their finite-support construction addresses a practical case: the uncertain vector can take one of finitely many known outcomes, while their probabilities must be inferred from observations. The resulting sets use classical goodness-of-fit tests to account for uncertainty in those probabilities. Bertsimas, Gupta, and Kallus, §§2–4, pp. 2–13.
In this case the support vectors are known in advance, so the problem is not to discover which outcomes are possible. The question is how much confidence to place in their estimated frequencies and how to turn that confidence region into a set of uncertain vectors suitable for a robust constraint. The paper gives two answers, one based on Pearson's chi-square statistic and one based on the likelihood-ratio, or G, statistic. Both answers are meant to work at every requested risk level for the same observed sample. Bertsimas, Gupta, and Kallus, Theorem 4, p. 13.
Let be the listed possible outcomes. A probability vector belongs to the simplex when all are nonnegative and . It determines the finite-support law . From a sample one obtains the empirical frequencies . A nonnegative number records the test threshold; in the paper it is , where is sample size and is the test's significance level. Bertsimas, Gupta, and Kallus, (10), p. 12.
The Pearson confidence region contains candidates satisfying . The G confidence region instead requires , with relative entropy . In either region, a candidate is excluded when : the source's divergence is then infinite. If both entries are zero, that coordinate contributes zero. These conventions matter because ordinary real division and logarithm in Lean have total values at zero. Bertsimas, Gupta, and Kallus, (10), p. 12.
For a direction , value at risk is the lower quantile of the scalar loss . Conditional value at risk is the minimum over real of . The paper's auxiliary set reweights the outcomes with another probability vector constrained by . The two data-driven uncertainty sets and allow such a reweighting for some in the corresponding confidence region. Their support function is the largest over . Bertsimas, Gupta, and Kallus, (11)–(13), pp. 12–13; Theorem EC.1, p. ec2.
The first target is the paper's finite-support CVaR identity and the comparison between the two risk measures:
The goal is Theorem 4's deterministic claim, simultaneously for all . For each in the relevant confidence region, it asks for both bounds
for every , with each uncertainty set nonempty, convex, and compact. A supporting milestone identifies each support function as the supremum of CVaR over its confidence region. The paper also displays conic optimization programs for these support functions in (14) and (15); those programs are outside this mission's drafted statements. Bertsimas, Gupta, and Kallus, Theorem 4, p. 13; proof, p. ec2.
The bounds give a way to certify the directional risk of every candidate distribution accepted by a goodness-of-fit test. For a nonempty convex compact uncertainty set, the paper's Theorem 1 turns this directional condition into a probabilistic guarantee for every constraint concave in the uncertain vector. Theorem 4 adds the sampling claim through coverage of the confidence region: when the true finite-support distribution belongs to that region, the whole family indexed by receives the guarantee. The statistical tests use chi-square approximations, so their advertised coverage is asymptotic rather than an exact finite-sample result. Bertsimas, Gupta, and Kallus, Theorems 1–4, pp. 10–13.
The paper proves the mathematical result. This mission asks for machine-checked proofs of its finite-dimensional definitions, the CVaR identity, the worst-case support identities, and the deterministic risk bounds. The drafted Lean statements are open goals. A completed development would also give reusable facts about finite-support risk measures and support functions under divergence-constrained probabilities. It would leave the test coverage calculation and the explicit programs (14)–(15) for separate work.
The risk comparison alone does not identify a robust uncertainty set: the support function must agree with the worst-case CVaR over an entire region of probability vectors. This brings a finite-dimensional optimization identity into the formal proof, including attainment and the relationship between reweightings and distributions. Boundary coordinates create another difficulty. The Pearson expression divides by , and the G expression contains ; silently accepting Lean's values at zero would enlarge the regions and change the theorem. The support function and CVaR are real infima or suprema, so their nonempty, bounded domains must also be established. Bertsimas, Gupta, and Kallus, (10)–(13), pp. 12–13; proof, p. ec2.
Lean represents outcomes and probability vectors as functions on Fin d and Fin n; indices start at zero. The simplex is Mathlib's stdSimplex. The law is a finite sum of point masses. If two listed vectors coincide, their point masses aggregate; the paper's notation is recovered with the intended distinct listing. Value at risk and the support function reuse published Prove2Me definitions; the finite-vector relative entropy also reuses a published definition, guarded at zero in this mission's G region. CVaR uses a real sInf, equal to the paper's minimum for a simplex law and . No statement applies it outside that domain.
The goal assumes and . These express, respectively, that the center is an empirical probability vector and that the chi-square threshold is nonnegative. It quantifies over every , with the same confidence regions for all levels. The paper's sample size, chi-square quantile, and significance level are compressed into ; coverage of the true distribution by the test is a separate statistical premise and is not formalized here. The source's is represented by for a supported probability vector . The draft does not treat an arbitrary unsupported law as a member of the confidence region.
The nonempty and compact conclusions rule out a zero returned by a support function on an empty or unbounded set. The zero-denominator guards rule out candidates the paper assigns infinite divergence. Contributions needed to close the mission include finite-simplex geometry, the finite-support CVaR identity, continuity of the divergence regions at boundary coordinates, and the risk-bound theorem. Those facts can be reused in later data-driven robust optimization developments.
Two-stage adaptive optimization models decisions taken in two steps: a first-stage decision is fixed before an uncertain right-hand side is revealed, and a second-stage decision is chosen afterwards, with the worst case over an uncertainty set to be minimized. Problems of this form arise in capacity planning, network design and inventory control, where the first stage is an investment and the second stage a recourse. Computing the fully adaptable optimum is hard in general, so tractable restrictions are used in practice, most prominently affine policies (Ben-Tal, Goryashko, Guslitzer, Nemirovski, Math. Program. 2004).
Bertsimas and Goyal (Math. Program. Ser. A, DOI 10.1007/s10107-011-0444-4) characterize how well affine policies perform. Their Section 5 shows a factor when the first-stage matrix satisfies . Section 6, the subject of this mission, drops the sign condition on : it constructs, from , a polytope with at most vertices that dominates , and shows that an optimal first stage for is a -approximate first stage for the original problem.
Timeline. Ben-Tal et al. (2004) introduced affinely adjustable robust counterparts. Bertsimas, Iancu and Parrilo (Math. Oper. Res. 2010) proved optimality of affine policies for one-dimensional multistage problems. Bertsimas and Goyal (Math. Oper. Res. 2010) analysed static robust solutions for two-stage problems. The present paper (received 2009, published 2011) gives the picture for affine policies and the general-case first-stage approximation formalized here.
Fix matrices , and cost vectors , . The uncertainty set is convex, compact and full-dimensional. A feasible solution of is a pair with and, for every , and , componentwise. Its worst-case cost is , and the fully adaptable optimum is
An optimal solution attains this value.
For let and let be a maximizer, (display (38)). Algorithm (Fig. 1 of the paper) starts with the index set ; while some has , it picks a maximizer of that scaled sum over , adds to a running total on the coordinates of , and removes from every coordinate whose total has reached . It stops after iterations and returns . The dominating set is
For every run of Algorithm , every choice of the maximizers , and every optimal solution of ,
The page states the factor as ; is the constant its proof establishes.
The result gives a first-stage decision with a guarantee of order for two-stage problems with an arbitrary first-stage matrix, a setting where the affine-policy analysis of Section 5 does not apply. The decision is obtained from a problem whose uncertainty set has at most extreme points, so it reduces an adaptive problem over a general convex set to one over a polytope with few vertices. Together with the paper's lower bounds (Theorems 2 and 3, for affine policies), it places the general-case approximability of the first stage at the same order as the affine-policy gap.
The result is proved in the paper. It has no machine-checked proof that we know of. The formalization produces, beyond the theorem itself, an encoding of model (1) with values that are honest infima, a relational encoding of Algorithm usable for its termination and output properties, and a reusable domination lemma for two-stage problems. Mission IV of this series (the case ) formalizes Lemmas 9 and 10 on Algorithm , which the proofs here use.
The obvious argument replaces by a simple set that contains or dominates it, such as the box , and solves over that set. This loses a factor , not : for with , , , , the optimum over is while the optimum over the box is . A dominating set with few vertices whose cost is only times the original optimum has to be built from itself, and controlling the cost of its vertex depends on the number of iterations of Algorithm , which is bounded only through the potential argument of Lemma 10 in the paper.
A second difficulty is that is an infimum, not an attained minimum, over second-stage rules that are arbitrary functions; the cost comparison must work from near-optimal solutions of .
Vectors are functions on Fin m, matrices are Matrix (Fin m) (Fin n) ℝ, and inequalities between vectors are componentwise. The paper's coordinate is Fin index . is the infimum of the set of bounds such that some feasible satisfies for all ; this avoids a real supremum of a possibly unbounded worst case. An optimal solution is a feasible one that achieves every achievable bound. and the maximizers enter the theorems as data with their defining properties. Algorithm is a relation on a choice sequence : the theorems hold for every run and every choice of maximizers, never for "some simplex dominating ".
Standing assumptions of (1) carried by the goal and Lemma 13: , , convex, compact and with nonempty interior, and (1) feasible. There is no sign condition on . Lemma 12 keeps only nonnegativity and full-dimensionality of ; the domination claim is stated for arbitrary scenario sets and with dominating and assumes that the optimal solution over has a finite worst-case cost.
The printed Lemma 13 also asserts on the grounds that is a simplex. Its generators need not be affinely independent, so this equality is not part of the mission; Theorem 6 does not use it.
A bound on alone is not the goal: the goal requires, for each scenario of the original set , a feasible second stage completing the fixed first stage at the stated cost. Lemma 13 also asserts feasibility over with a finite bound, so its inequality cannot hold through the value of an infimum over an empty set.
A complete development needs elementary facts about convex hulls of finitely many points (representation by convex weights), the properties of Algorithm (its output bound and termination, Lemmas 9 and 10 of the paper), and -approximation arguments for infima. The encoding of model (1) and of Algorithm is shared with the other missions of this series. Contributions of these supporting lemmas are welcome.
Two-stage adaptive optimization models decisions taken in two steps: a first-stage decision is fixed before an uncertain right-hand side is revealed, and a second-stage recourse is chosen afterwards, with the worst case over an uncertainty set to be minimized. The fully-adaptable problem, in which may be an arbitrary function of , is intractable in general. The standard tractable restriction, introduced by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004), requires to be an affine policy ; it turns the problem into a single convex program and is used throughout robust inventory, network design and energy planning.
How much is lost by this restriction? Bertsimas and Goyal (Math. Program. 2012) answer the question for problems with a nonnegative constraint matrix. On one side, affine policies are optimal when is a simplex, and are within a factor of the optimum on every instance of the class, where is the number of constraints. On the other side, the bound is nearly tight: Section 4 of the paper constructs an instance on which the best affine policy costs times the fully-adaptable optimum, for any . This mission formalizes that lower bound.
Timeline: Ben-Tal et al. (2004) propose affinely adjustable robust counterparts; Bertsimas, Iancu and Parrilo (2010) prove optimality of affine policies for one-dimensional multistage problems; Bertsimas and Goyal (2012) give the upper bound and the matching lower-bound example formalized here.
The two-stage problem has data , , , and :
The value is the same minimum over policies of the form ; such a policy must be nonnegative on all of .
The large-gap instance of display (19) has , a parameter with (condition (18)), and
where are the unit vectors and is the indicator vector of a set of coordinates. A permutation of the coordinates acts on vectors by and on matrices by .
The paper writes ; the constant is the one the proof establishes, so the explicit statement is the stronger one.
The result shows that the approximation guarantee for affine policies on problems with (Theorem 4 of the same paper) cannot be improved beyond a factor , so the uncertainty set that looks like a portion of the unit sphere in the nonnegative orthant is essentially the worst case for affine recourse. It also explains why later work moved to piecewise-affine and finitely adaptable policies to close the gap. The example satisfies , and , so the lower bound applies to every larger problem class.
The theorem is proved in the paper; to our knowledge no machine-checked version exists. A formalization adds checked statements of the symmetrization argument (an optimal affine policy may be taken invariant under the symmetry group of the instance), which applies to any symmetric robust linear program, and a checked derivation of the explicit constant.
The upper bound is a direct construction. The difficulty lies in the lower bound on , which must hold for every affine policy, a family with free parameters. Bounding the cost of a policy at a few chosen points of does not suffice without first reducing the parameters, and the reduction requires that an optimal affine solution exists (attainment of the minimum over an unbounded parameter set) and that averaging over the symmetric group preserves both feasibility and optimality. The remaining argument balances three different generators of against each other, and the exponents of must be tracked exactly through ceilings and real powers.
Vectors are Fin m → ℝ with the componentwise order and 0-based indices; matrices are Matrix (Fin m) (Fin m) ℝ. The values and are infima of the sets of worst-case cost bounds achieved by feasible solutions (epigraph form), so they do not rely on a supremum of a possibly unbounded function. Affine policies must be nonnegative on . Optimal solutions are defined as feasible solutions whose worst-case cost is bounded by every achievable bound, so Lemma 8 asserts attainment. Powers are real powers; and exactly as on the page. is the convex hull of its listed generators; the generator count printed in (19) plays no role.
The parameter is not restricted beyond and , as in the paper. Lemma 4's proof on the page uses ; the statement is kept for all , where it remains true with a different witness. The Claims are stated for any symmetric feasible affine policy with cost at most ; their hypotheses are jointly unsatisfiable by Theorem 3, which is inherent in steps of a proof by contradiction.
A trivializing formalization is excluded: the goal mentions only the instance data and the two optimal values, not the symmetric parameters , and the nonemptiness of the feasible sets is established by Lemma 4 and by the existence of a feasible affine policy, so neither value is a junk infimum of an empty set.
A complete development needs: convex hulls of finite point sets in and their extreme points; the action of by coordinate permutation; averaging over the finite group ; and existence of minimizers for linear programs over a polytope. The symmetrization lemmas (5–8) are reusable for other symmetric robust problems. Proofs of any milestone, including partial infrastructure for linear-programming attainment, are welcome.
Multistage robust optimization chooses decisions over time while an adversary picks the uncertain data from a known set; every later decision may react to what has been observed. The exact problem is a nested min-max over functions of the past, and is intractable in general. The standard workaround, proposed by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 2004), restricts every decision to an affine function of the observed disturbances. The restricted problem is a single convex (often linear) program, which is why disturbance-affine policies are used throughout robust control, inventory management and model predictive control. The price is suboptimality, and before this paper there was no nontrivial multistage problem in which that price was known to be zero.
Bertsimas, Iancu and Parrilo (arXiv:0904.3986, 2009; Math. Oper. Res. 35(2), 2010) proved that for one-dimensional linear dynamics with box constraints on controls and disturbances, linear control costs and convex state costs, disturbance-affine policies are exactly optimal. Their companion paper (Bertsimas & Goyal, Math. Program. 2012) shows how poorly affine policies can perform in other settings, so the one-dimensional result marks one side of the boundary between models where affine policies are exact and models where they are not.
Fix a horizon and an initial state . For each stage there are a per-unit control cost , control bounds , disturbance bounds , and a state cost that is convex and coercive. The state evolves as
The controller chooses after seeing ; the adversary then chooses . The min-max value is the value of the nested problem , computed by the Bellman recursion with :
An affine control policy and an affine running cost at stage are
so sees the disturbances before stage and those up to stage . Under these policies the state after stage is .
There exist affine policies and affine costs such that, for every ,
At this says that affine policies are robustly feasible and attain the min-max value.
The theorem is one of the few exact optimality results for affine policies in multistage robust optimization. Combined with linear programming duality it has a computational corollary: when the are piecewise affine, an optimal policy for the full min-max problem is obtained from a single linear program (the affinely adjustable robust counterpart, p. 5), instead of a dynamic program over a continuous state. The construction also shows what is special about one dimension: the relevant uncertainty enters only through a planar zonogon, whose right side has at most vertices, matching the coefficients of an affine policy.
The result is proved in the literature, not formalized; no machine-checked proof of it, or of the zonogon lemmas it uses, is known. The formalization adds a checked proof of the main theorem and of the planar convexity facts (Lemma 4.1, Corollary 4.1) that are reusable for other zonotope arguments. It also closes the gaps the preprint leaves to the reader: Assumption 2 is removed by an infinitesimal perturbation argument, footnote 4 assumes a unique minimizer of , and Lemma 4.3 is proved in one sub-case only.
Dynamic programming gives the optimal control as a function of the current state, , which is piecewise affine in with up to three pieces. Since is affine in past disturbances, the obvious idea is to substitute; but the composition is piecewise affine, not affine, in the disturbances, and no single affine function reproduces it. An affine policy is necessarily suboptimal at some disturbance sequences. The theorem asserts only that it is never suboptimal at the worst case, and that the excess cost it causes can be absorbed into an affine cost that still dominates . Establishing this requires controlling where a convex objective is maximized over a zonogon, and showing that the affine controller and the affine cost can be chosen to reproduce exactly the right-side vertices that matter, at every stage, while staying feasible. A naive matching of all vertices of the disturbance box is overdetermined.
Stages are indexed by Fin T (0-based). The model is the reduced form (DP) of §2, with dynamics coefficients equal to 1; the paper notes that this is without loss of generality. The standing hypotheses are those of Problem 1.1 (, convex and coercive) plus two disclosed additions, and : the page writes both as intervals but does not say they are nonempty. is defined by the Bellman recursion with sSup/sInf over images of nonempty compact intervals of continuous functions, so the values are attained maxima and minima. The max in (14) is stated with IsGreatest, which asserts attainment.
The goal carries none of the proof's normalizations (Assumptions 1–3 of p. 10, the unique minimizer of footnote 4). The milestones of §4 are stated in the paper's simplified notation: the unit hypercube, generators ordered as in (32) (cross-multiplied), the clamp form of the optimal control law (the printed (8) has misprinted thresholds), and, where the paper divides by , the hypothesis . Lemma 4.4 takes Lemma 4.3's conclusions as hypotheses; Lemmas 4.8–4.9 take system (51)–(53) (with two misprints of (53) corrected) as hypotheses instead of "computed by Algorithm 2". Every fraction in a system is cross-multiplied.
Trivializing formalizations are ruled out. (14) uses a maximum over a nonempty box of a continuous function, with the true . The policies read only past disturbances (sums over , resp. ). is the Bellman value over all state-feedback controls, not the value of the affine problem.
The development needs convexity of value functions under partial minimization and maximization, extreme points of planar polygons, and maxima of convex functions over polytopes. Contributions of independent planar-geometry lemmas are welcome, as are proofs of Lemma 4.3 (not stated here) and of the remaining construction lemmas 4.5–4.7.
A robust linear constraint for all protects a decision against every realization of the data in an uncertainty set . Robust optimization took this form in the work of Ben-Tal and Nemirovski (Math. Oper. Res. 1998; Oper. Res. Lett. 1999), where is chosen by the modeller. Bertsimas and Brown (Oper. Res. 2009) tie the choice of to the decision maker's attitude towards risk: on a finite sample , a coherent risk measure constraint is equivalent to a robust constraint over a convex set built from , and for the distortion risk measures (the law-invariant, comonotone coherent measures, which include CVaR) that set is a polytope of a special kind, a permutohull.
An uncertainty set in practice is often an arbitrary polyhedron, given by the modeller or by previous analysis. Section 4.5 of the paper asks which distortion risk measure best approximates such a polyhedron from inside: the largest permutohull of a given shape contained in it. A positive answer quantifies how conservative a given polyhedral uncertainty set is relative to a distortion risk measure, and gives the risk measure that is closest to it. This mission is the third of a series of three on the paper; the first establishes the permutohull representation of distortion risk constraints, the second the generators of the centrally symmetric distortion measures.
Fix and data , the columns of a matrix . Let have at each entry, so the sample mean is .
measures against the shifted permutohull (12).
The family of candidate inner approximations is obtained by mixing a fixed with the uniform generator: , .
Let be the optimal value of the linear program
in and , and . Then
and, when , if and only if
The theorem reduces a geometric question — the largest member of a one-parameter family of centrally symmetric polytopes, each with potential vertices, that fits inside an arbitrary polyhedron — to a linear program with variables and constraints. Its solution identifies a distortion risk measure , which the paper reads as a mean–deviation measure in the style of a Sharpe ratio, and the bound (16) decides whether the optimal set is itself a distortion set or must be shrunk further.
The results are proved in the paper, with short proofs that pass over several points: the scaling identity is asserted, the duality step leaves the assignment-problem structure implicit, and the norm claim requires a nondegeneracy condition that the page does not state. No machine-checked proof of any of them is known. A formalization fixes the exact hypotheses (nonempty interior for the norm, in (13), in (16)), and the containment equivalence for arbitrary real weight vectors is a reusable fact about permutohulls and assignment duality.
The goal combines three ingredients of different nature. The containment equivalence needs that minimizing a linear function over the permutohull is a linear program over the Birkhoff polytope of doubly stochastic matrices, followed by linear programming duality for that program; neither the Birkhoff–von Neumann theorem nor assignment duality is a one-line consequence of what is in Mathlib. The scaling identity is a statement about convex hulls under an affine map and holds for all real , including the reflected case ; the maximality claim then needs the central symmetry of about , which is a property of (Proposition 4.1 of the paper) and not of a general . The tempting shortcut — comparing gauges directly — fails at , where the permutohull is the single point and the gauge is degenerate.
Vectors in and are Fin N → ℝ and Fin n → ℝ, with -based indices; is a i, is a dot product. uses Mathlib's stdSimplex and Antitone. The permutohull is convexHull of the range over Equiv.Perm (Fin N), defined for every real because (15) evaluates it at mixtures with possibly negative entries. The Minkowski functional is Mathlib's gauge, which takes the value (not ) on points no positive multiple of the set reaches; this is why Proposition 4.2 assumes has nonempty interior and why the goal states "largest" as set containment. is . The optimal value is a hypothesis (it is the greatest element of the feasible set of (15)), not a supremum defined by sSup.
Standing assumptions and disclosed additions: ; the polyhedron (14) is not assumed bounded (a generalization); in (13) the right-hand norm is that of , not as printed, and ; in (16), ; "corresponds to a distortion risk measure" is read, as the proof reads it, as . A formalization that assumes or the maximality of trivializes the theorem: both are conclusions, and the linear program enters only through its constraints and its optimal value.
A complete development needs: convex hulls under affine maps; the Birkhoff–von Neumann theorem (doubly stochastic matrices are convex combinations of permutation matrices); duality for the assignment linear program; gauge calculus for centrally symmetric convex bodies. The containment equivalence and the scaling identity are reusable beyond this mission. Proofs of any milestone, and of the Birkhoff and assignment-duality infrastructure, are welcome.
Airlines, hotels and cruise lines rarely change prices continuously. They sell a fixed product (seats on one flight, rooms on one night) over a finite selling season, and they sell it at a small set of fares, opening and closing fare classes as the season unfolds. Gallego and van Ryzin, in Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons (Management Science 40(8), 1994, doi:10.1287/mnsc.40.8.999), model this as the sale of items over a horizon of length , with Poisson demand whose rate depends on the current price. Section 4 of the paper restricts the price to a finite menu and asks how much is lost by using a simple rule that charges only two adjacent prices and switches once. The answer, Theorem 5, gives one explanation of fixed-fare-class yield management: with two fares and one well-timed switch, a seller earns asymptotically the best revenue any policy over the menu can earn. The source of this mission is the published 1994 article.
The paper is the starting point of a long line of work on fluid (deterministic) approximations in revenue management, including Feng and Gallego (1995) on optimal switching times between two prices and later re-solving and bid-price analyses, all of which compare stochastic policies to the value of a deterministic problem in the same way.
A menu consists of prices and Poisson demand rates ; the firm may also charge the null price , at which demand is . The revenue rates satisfy , and the points lie on a concave function on vanishing at .
The deterministic problem replaces random demand by its rate. If is the time spent at price , the problem is the linear program
Given and , let be the index with , and put
The stopping-time (ST) heuristic starts at price and switches to at the random time , where is the time of the -th demand. Sales stop when the items are gone or at time . is its expected revenue.
For a fixed index with and any sequences , with ,
No rate of convergence is fixed in the goal, and the ratio may vary along the sequence.
Theorem 5 says that a policy with one price change, chosen from the deterministic solution, loses a vanishing fraction of the deterministic revenue. Since bounds the optimal expected revenue over all non-anticipating policies with prices in the menu (§4.0.1 of the paper), the ST heuristic is asymptotically optimal, and the optimal policy, which solves a Hamilton–Jacobi–Bellman system with no closed form, can be replaced by a rule that is computed by hand. The result also shows that a finite menu, together with dynamic allocation of capacity between two neighbouring prices, can realize the effective price of a continuous demand curve.
The theorem is proved in the paper. As far as the platform's index shows, neither this result nor the controlled Poisson sales process it needs has been formalized; Mathlib has the exponential and Poisson distributions but no counting process with a policy-dependent intensity. The mission produces a machine-checked version of the paper's proof chain: the LP solution, the coupling inequality between two heuristics, the deterministic horizon estimate (28), and the Poisson overflow estimate built on Gallego's bound (inequality (18) of the paper, already proved on the platform as PricingRM.DetHeuristic.gallego_bound).
The deterministic parts (Proposition 4, (28), the closed form of ) are finite-dimensional linear algebra. The difficulty sits in the stochastic comparison . The ST heuristic's switching time depends on the sales process, and after the switch the remaining stock and the remaining time are both random. The obvious attempt, writing as a sum of two independent Poisson terms, is wrong: the two phases are dependent through . Any comparison has to handle a second phase whose starting stock and starting time are both random, which brings in the behaviour of the sales process after a random time determined by the process itself. The limit step then needs the overflow bound uniformly along sequences whose ratio is not fixed.
All declarations live in the namespace GVRPricing.StoppingTime. The committed conventions are:
Fin K): Lean index is the paper's price number , and lamN, pN, rN extend the sequences by beyond , matching the paper's .A trivializing formalization would define through the wasteful formula, or by a closed-form expression, which makes the goal the wasteful bound; here is the expected revenue of the switching rule on the sales process. Likewise the limit is taken along sequences with , not at a single .
Useful infrastructure, reusable beyond this mission: the exponential-clock construction of a Poisson process with piecewise-constant intensity, the strong Markov property at a stopping time of the clocks, and the expected Poisson overflow . Contributions to any milestone, and alternative proofs of , are welcome.
A retailer, an airline or an online platform decides which products to show a customer. Showing more is not always better: a customer who would have bought an expensive product may switch to a cheap one once it is offered. The assortment problem asks for the set of products that maximises expected revenue, given a model of how customers choose. It is a central problem of revenue management (Talluri and van Ryzin, 2004), and it is NP-hard even for mixtures of two multinomial logit models (Rusmevichientong, Shmoys, Tong and Topaloglu, 2014).
The standard heuristic in practice is revenue-ordered assortments: sort the products by price and only consider the sets consisting of the most expensive products down to some threshold. It is optimal under the multinomial logit model (Talluri and van Ryzin, 2004), but not in general. Berbeglia and Joret (arXiv:1606.01371) ask how much revenue the heuristic can lose under every reasonable choice model, and answer with guarantees that depend only on the prices.
Timeline:
There is a finite nonempty set of products. For a choice set , is the probability that a customer offered buys product , and is the probability that the customer buys nothing. The system is a regular discrete choice model if
Axiom 4, regularity, says that adding products never makes a given product, or leaving without buying, more likely. Every random utility model is regular.
Each product has a positive price . The revenue of is , and . Let be the distinct prices, so counts price levels and not products, and set . The revenue-ordered assortments are , , and the heuristic earns
The goal fixes no constant beyond the paper's own quantities. Both parts are required: the sum form is the sharper bound, and the paper shows it is attained (Theorem 3.4, a later mission of this series).
The theorem shows that a pricing-only quantity controls the loss of the most common heuristic in revenue management, uniformly over all regular choice models, including every random utility model, mixtures of logits and Markov chain models. Combined with the hardness result of Aouad et al., it shows that revenue-ordered assortments achieve essentially the best ratio, as a function of or of , that an efficient algorithm can achieve. The same analysis transfers to the envy-free pricing and Stackelberg problems studied in the later sections of the paper.
The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a Lean formalization of regular choice models, the revenue-ordered heuristic and its two guarantees, on which the paper's tightness examples, the purchase-probability bound (Theorem 3.3) and the applications to pricing can build.
The argument is short, but two points are easy to get wrong. First, revenues of and of an optimal involve choice probabilities evaluated at different sets, so the comparison must pass through , using regularity once for products and once for the no-purchase option. A model that only assumes regularity for products does not satisfy the theorem. Second, the bound runs over distinct price levels, not products, and the first summand uses the convention ; indexing by products or dropping gives a different quantity. The comparison of the sum with is a Riemann-sum estimate for and needs a real-analysis lemma not phrased this way in Mathlib.
C with decidable equality; choice sets are Finset C. The choice probabilities are P : C → Finset C → ℝ, defined on all pairs. The no-purchase option is not a product: is the derived quantity noPurchase P S = 1 - ∑ x ∈ S, P x S.IsRegular P carries axioms (i)–(iv), with (i) and (iv) each split into a product case and a no-purchase case. The no-purchase case of (i) is redundant with (iii) and is kept to match the page.r : C → ℝ with the hypothesis ∀ x, 0 < r x. revenue P r S is and opt P r is the maximum over all Finset C (Finset.sup'), including the empty set.level r i is for and level r 0 = 0; numVals r is , the number of distinct values. roSet r i is ; roValue P r is the maximum over only.Real.log, applied to .Needed infrastructure: finite sums over price levels and summation by parts, the comparison of with , and the sorted enumeration of a finite set of reals (Finset.orderEmbOfFin). The regular model and the revenue-ordered sets are shared with the other missions of this series. Contributions of any milestone, alternative proofs of the logarithmic bound, and proofs that specific choice models are regular are welcome.
A retailer holding a fixed stock of a perishable or seasonal good (fashion items, airline seats, hotel rooms, concert tickets) must sell it before a deadline, after which unsold units are worthless. Demand is random and depends on the posted price, and the firm may change its price at any time. Dynamic pricing asks how the price should depend on the remaining stock and the remaining time.
Gallego and van Ryzin (Management Science 40(8), 1994) posed this problem as a continuous-time intensity control problem and established its basic structure. Their Theorem 1 says that the optimal expected revenue is strictly increasing and strictly concave in both the stock and the time remaining, and that the optimal price falls as stock grows and rises with the time left to sell. The paper is a standard reference of revenue management; the structural result is the continuous-time counterpart of the monotonicity of marginal values in discrete-time models (Talluri and van Ryzin, The Theory and Practice of Revenue Management, 2004, Proposition 5.2), and it is what makes the optimal policy computable by restricting attention to monotone policies. The paper credits a slightly weaker version to Kincaid and Darling (1963). The source formalized here is the published 1994 article.
The firm chooses a demand rate from a set of allowable rates, an interval containing ; the market then sets the price , where is the inverse demand function, strictly decreasing and nonnegative on the positive rates. The rate corresponds to the null price at which nothing sells. The revenue rate is
The demand function is regular when is continuous, bounded and concave on and has a least maximizer . The exponential demand , with , and , is the running example.
With units in stock and time remaining , write for the optimal expected revenue. The paper derives the Hamilton–Jacobi system
with and . The difference is the marginal value of an item; a rate attaining the supremum is an optimal intensity , and is the optimal price .
For the solution of (8), with strictly concave, differentiable on the interior of , and interior:
Theorem 1 is the qualitative backbone of single-product dynamic pricing. Concavity of in means that each additional unit is worth less than the previous one, which is the basis of bid-price and marginal-value reasoning in revenue management; the monotone price path justifies markdown practice as the deadline approaches and reduces the policy search to monotone policies. Proposition 3 answers, for exponential demand, a question raised by Mills (1959): the stochastic optimal price is never below the deterministic one. The closed form (9)–(10) is one of the few exactly solvable intensity control problems in pricing.
The results are proved in the paper; none of them has a machine-checked proof. Formalizing them requires the comparison and monotonicity theory of a countable system of coupled ordinary differential equations whose right-hand side is a convex conjugate, a theory that Mathlib does not package. A complete development would also certify the corrected hypotheses of Theorem 1 described below.
The value functions are defined only implicitly by (8), a triangular infinite system of ODEs in which each is driven by through the nonsmooth map . Monotonicity of the optimal intensity in is a statement about the time derivative of a marginal value, and the paper establishes it by an induction on combined with an argument by contradiction on the first interval where monotonicity could fail. The obvious approach of differentiating (8) twice in needs second derivatives of and of that the hypotheses do not provide, and the paper's own proof of Proposition 1 assumes that is nondecreasing in , which is only established in Theorem 1; a rigorous development must break this circularity.
A regular demand function is a Lean structure (GVRPricing.Structure.Model) holding , and with the paper's standing assumptions of §2.1: an interval, strictly decreasing and nonnegative on , continuous, concave and bounded on , and the least maximizer. The definition IsHJBSolution encodes (8) for , with the second argument the time remaining, the two-sided derivative at each , continuity on , the boundary conditions, and the requirement that the set inside the supremum be bounded above, so that the real supremum is never a default value. An optimal intensity at is any maximizing over .
All theorems are about solutions of (8), on which the paper's proofs operate. The identification of the solution of (8) with the supremum of expected revenue over non-anticipating pricing policies is Brémaud's verification theorem, which the paper cites and does not prove; it is not part of this mission.
Added hypotheses and corrected statements.
A formalization that defines by a formula, or postulates a monotone function as the optimal intensity, would trivialize the goal: the goal quantifies over every solution of (8), and the optimal intensity it asserts must maximize the right-hand side of (8) at every .
A complete development needs comparison principles for scalar ODEs with Lipschitz right-hand sides, properties of the concave conjugate (monotonicity, Lipschitz continuity, envelope theorem), and monotone comparative statics of maximizers. These are reusable well beyond this mission; contributions of any of them, or of the milestones in any order, are welcome.
The data of a linear program are often not known exactly: they are measured or estimated, or they are forecasts. The robust counterpart approach, going back to Soyster (1973), asks for a solution that is feasible for every data matrix in a prescribed uncertainty set and is best among such solutions. Ben-Tal and Nemirovski's 1999 paper [1] showed that the method stays computationally tractable for a broad class of uncertainty sets, the ellipsoidal uncertainties: the robust counterpart of an uncertain LP is then a conic quadratic program (CQP), solvable by interior point methods at roughly the cost of an LP of similar size. This result is the basis of robust linear optimization as it is used today [2], [3]. It is also the reason ellipsoidal sets are the default choice in robust portfolio selection (§4 of the paper) and in many later robust models.
Timeline. Soyster (1973) treated column-wise box uncertainty, for which the counterpart is again an LP [4]. Ben-Tal and Nemirovski (1998) developed the general theory of robust convex optimization [5]. The present paper (1999) proved the ellipsoidal-to-CQP reduction for LPs (Theorem 3.1). Its proof relies on the conic duality theory of Nesterov and Nemirovski (1994) [6].
An uncertain linear program in the homogeneous form (6) is
where are fixed and the matrix lies in an uncertainty set . A point is robust feasible if and for every . The robust counterpart minimizes over the robust feasible set
An ellipsoid in (display (14)) is a set
where is affine in , is an matrix, and is the Euclidean norm. A singular gives an ellipsoidal cylinder, which may be unbounded. An ellipsoidal uncertainty is a set
(condition A) that is bounded (condition B) and contains a matrix with and for every (condition C, a Slater condition).
For every ,
Here is an explicit system: linear equations and one linear inequality in , together with the second-order cone constraints . Its coefficients are the matrices and . The robust feasible set is therefore the projection of the feasible set of the conic quadratic program (CQP), which minimizes subject to and .
The CQP forms (16) and (17) of the simplest cases (a single ellipsoid; constraint-wise ellipsoids), Remark 3.1 (bounded polytopes are ellipsoidal uncertainties), and the robust portfolio counterpart (22).
The result. Theorem 3.1 turns a semi-infinite constraint system (one constraint for every ) into finitely many conic quadratic constraints whose size is polynomial in the data. Robust LPs with ellipsoidal uncertainty, which by Remark 3.1 include polytopic uncertainty, can therefore be solved by standard conic solvers. Later robust optimization results, such as budgeted uncertainty, affinely adjustable policies and distributionally robust LPs, refine this pattern.
Formalizing it. The theorem is classical and its proof is complete, but no machine-checked proof exists. A formal proof needs a conic quadratic strong duality theorem with dual attainment (claim (II)), which Mathlib does not have in this form. That duality theorem can be reused well beyond this mission. The companion results (16), (17) and (22) are self-contained computations of a minimum of a linear function over a Euclidean ball.
The "if" direction is weak duality: a solution of certifies that the -th constraint holds for all of . The content is the "only if" direction. It requires dual attainment, not merely equality of optimal values, because a solution of must exist. Dual attainment fails without a constraint qualification. Condition C must hold strictly for every ellipsoid, including , and the ellipsoids may be cylinders, so the variables can range over unbounded sets even though is bounded. Projecting the problem onto a single parameter space is not available in general, because the maps need not be injective.
Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ. The indices are Fin (k + 1), and the equality multipliers , , are indexed by Fin k. Every norm is Euclidean, written out as euclidNorm v = √(∑ v_j²), because Mathlib's norm on Fin M → ℝ is the sup norm, under which ellipsoids would become boxes. Condition B is a uniform bound on all matrix entries, and condition C is required for every . The page's words say "", but its display and the proof use every . Injectivity of is not assumed, and neither is §2.1's standing assumption that is convex and closed. An ellipsoidal uncertainty is convex automatically, and closedness is not used, so both omissions generalize the statement. Three printed slips are corrected and disclosed: the sum in the equality constraint of (CQP) runs over ; has where the page prints ; and Remark 3.1 has the factor where the page prints .
The goal is not the contentless statement "some conic quadratic program has as a projection", which holds for every closed convex set. It names the system built from the data , . The goal also does not mention optimal values, (CQP) or strict feasibility; those are milestones.
Contributions are welcome on the conic duality theorem (II) as a standalone result, on the finite-dimensional facts that minimize a linear function over a Euclidean ball (used in (16), (17) and (22)), and on the goal itself.
Robust linear optimization replaces an uncertain constraint by the requirement that hold for every in an uncertainty set (Ben-Tal and Nemirovski 1999). The method leaves open where should come from. Risk theory answers a related question from the other side: a decision maker's attitude to an uncertain reward is described by a risk measure , and the constraint is imposed as .
Bertsimas and Brown (2009) connect the two. When is coherent and is supported on finitely many observed data points , the risk constraint is exactly a robust constraint whose uncertainty set is built from the data and the family of probability vectors generating . For the class of distortion risk measures, the uncertainty set has an explicit polyhedral form, the -permutohull of the data, and the robust constraint has a reformulation of polynomial size. This mission formalizes that chain of results, Sections 2–4.3 of the paper.
The sample space is finite, , and a random variable is a vector , read as a reward; means for every . The probability simplex is , and .
A risk measure is a function with and . It is coherent if it is moreover convex and positively homogeneous. A set generates if for all . The conditional value-at-risk under a probability vector is for .
Two random variables are comonotone if for all ; is comonotonic if it is additive on comonotone pairs, and law invariant if it takes equal values on random variables with the same distribution. A distortion risk measure is a coherent, comonotonic, law-invariant risk measure. From Section 4.2 on, carries the uniform distribution .
The restricted simplex is . For put
where are the increasing order statistics of . The data are , the uncertain vector takes the value at , and the -permutohull of is
Under the uniform distribution, for every distortion risk measure there is with , and for this , all data and every ,
The vector depends on only; the data are quantified after it.
A companion item states Corollary 4.3: , and the class equality it yields: the uncertainty sets of all distortion risk measures are exactly the polytopes , , .
The goal theorem identifies the uncertainty set implied by any distortion risk measure: it is a permutohull of the data, a polytope with up to vertices that is nevertheless representable with extra variables and linear constraints. Combined with Theorem 4.2, the uncertainty sets of distortion measures are exactly the mixtures of the sets of -point averages of the data (Corollary 4.3), with as the generators. The later sections of the paper build on this: centrally symmetric permutohulls (Section 4.4) and the construction of a distortion risk measure from a given polyhedral uncertainty set (Section 4.5) are the subjects of the two companion missions.
The results are proved in the paper; no machine-checked version is known. The formalization adds checked statements of the finite-space representation theory of coherent and distortion risk measures, which the paper obtains partly by citing general results, and records the corrections the printed statements need.
The two equalities of the goal have unequal weight. The second is a statement about one polytope with up to vertices and a linear system of size ; it is finite-dimensional linear programming. The first requires the complete characterization of distortion risk measures on a finite uniform space, and that is where the obvious approach fails. The known representation of law-invariant comonotonic coherent measures as mixtures of CVaR (Kusuoka 2001) is proved for atomless spaces and does not transfer to a discrete . The uniform distribution is essential, not a convenience: Remark 4.2 of the paper gives a two-point space with probabilities and a monotone, normalized, submodular set function depending only on probability whose induced distortion is not concave, so the conclusion of Theorem 4.2 fails there.
Fin N with ; random variables are Fin N → ℝ; indices are 0-based throughout, so qhat j is the paper's and is Antitone q. Order statistics are X ∘ Tuple.sort X.stdSimplex ℝ (Fin N). Generation (1) is an IsLUB over an arbitrary set of probability vectors, not a maximum over a finite family (that version is false).A linear decision made with uncertain coefficients can be protected by requiring the constraint to hold for every coefficient vector in an uncertainty set. Choosing that set determines how conservative the decision is. Bertsimas and Brown connect this choice to a risk measure: a functional that assigns a cost to the random reward left by a decision. Their construction turns certain risk constraints into robust linear constraints over a convex hull of weighted samples. This mission isolates the structural question asked in §4.4 of their paper: which such risk measures always produce uncertainty sets that are centrally symmetric about the sample mean? The answer matters because this symmetric family is the class used in the paper's subsequent approximation of general polyhedral uncertainty sets. Bertsimas and Brown (2009), §§4.3–4.5.
There are observations, indexed by , with equal reference probabilities. A probability weight vector has nonnegative entries summing to one. The restricted simplex contains those vectors whose entries are nonincreasing: . For a reward vector , write for its increasing order statistics. The associated distortion risk measure is . A larger reward therefore reduces risk. Under the uniform distribution, the paper's Theorem 4.2 identifies these functionals, for , with its distortion risk measures. Bertsimas and Brown (2009), Theorem 4.2.
Take arbitrary sample vectors . For a permutation of their indices, form the weighted vector . The -permutohull is the convex hull of all these vectors. Its center of interest is the sample mean . A set is centrally symmetric through when implies for every . The quantifier “for any data” ranges over every dimension and every choice of sample vectors. It is stronger than symmetry for one selected data set. Bertsimas and Brown (2009), Definitions 4.7–4.8.
The first target is Proposition 4.1's characterization of weights giving universal symmetry. If is the vector with every entry , then
This condition defines the symmetric restricted simplex inside . Bertsimas and Brown (2009), Proposition 4.1 and Definition 4.9.
The main target is Theorem 4.4. Put . For , define a generator by
A functional represented by a whose permutohull is symmetric for every data set is exactly a convex mixture of the generator functionals:
The milestones also state the two set inclusions behind the equality of with the convex hull of these generators, including the coordinate reversal identity. Bertsimas and Brown (2009), Theorem 4.4 and its proof.
The result gives a finite list of risk functionals from which every member of the universally symmetric distortion subclass can be formed. The number of generators is , rather than an unspecified family. It also connects a geometric property of a robust uncertainty set to a checkable condition on its weights. The paper uses this symmetric subclass to formulate the inner approximation problem in §4.5, where a symmetric permutohull is fitted inside another polytope. Bertsimas and Brown (2009), §§4.4–4.5.
The mathematical result is proved in the 2009 paper. This formalization task is to obtain Lean proofs of the classification and its source-stated intermediate claims. The definition layer is a reusable interface for finite distortion risk measures, permutohulls, and symmetry under coordinate permutations. Formal proofs here would provide a checked foundation for later robust optimization statements using the same finite sample model. The proposed goal and milestones are open Lean statements; compiling them verifies their syntax and types, not their proofs.
Symmetry of one pictured polygon does not determine its weight vector. The hypothesis demands symmetry for every possible collection of sample vectors, so the converse in Proposition 4.1 must recover a relation among weights from a universal geometric property. Another difficulty is that the explicit generators change shape at the midpoint, and the odd and even cases have different middle ranges. The paper writes the calculation for odd and says the even case is analogous; the theorem itself makes no parity restriction. A proof therefore has to cover the even boundary, including the generator whose band is empty. Bertsimas and Brown (2009), Proposition 4.1 and proof of Theorem 4.4.
The Lean sample space is Fin N, with . Its indices start at zero; the prose and source formulas above start at one. The source's is N / 2 + 1 in natural numbers. Probability vectors use Mathlib's standard simplex together with antitone coordinate order. Permutohulls use convexHull of the finite permutation family, and order statistics use Tuple.sort. The reference distribution is uniform, as in the paper's Assumption 4.1. Real vector spaces of dimension zero are allowed because the claim quantifies over every dimension; the nonempty sample condition excludes division by zero.
The goal takes an arbitrary functional and requires an actual representation by a restricted-simplex weight. This is the paper's Theorem 4.2 parametrization of distortion risk measures, stated directly because that theorem is being drafted in a separate mission of the same series. Universal symmetry is derived from the data quantifier; it is not assumed as a condition on . The generator mixture is likewise the conclusion, with its coefficients nonnegative and summing to one. Central symmetry includes membership of the center in the set.
Useful contributions include proofs of the source's permutation characterization, validity and symmetry of generator mixtures, and their converse spanning property. The definitions of finite probability weights and weighted permutation hulls can support further finite sample robust optimization results. The paper's inconsistent accent on the generator risk measure in Theorem 4.4 is read as the functional of the displayed generator vector; its intermediate sum on p. 1492 does not alter the stated normalized mixture.
Hassler Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets of elements carrying an abstract notion of dependence that captures what linearly dependent columns of a matrix and cycles of a graph have in common. A distinctive feature of the paper is that it gives several independent axiom systems for the same structure: one in terms of rank, one in terms of independent sets, one in terms of bases, and one in terms of circuits (minimal dependent sets). It then proves they are interchangeable. These equivalences, now called cryptomorphisms, are what allow matroid theory to move freely between the algebraic picture (rank of a set of vectors) and the combinatorial one (cycles of a graph, minimal dependent column sets). Every textbook on the subject relies on them, for example J. Oxley, Matroid Theory, Chapter 1.
This mission treats one of them: the equivalence of Whitney's rank postulates (§2) and circuit postulates (§8). The circuit side is the one used in combinatorial optimization, where circuits appear as cycles in network flows, as minimal infeasible subsystems, and in the exchange arguments behind the greedy algorithm.
Let be a finite set of elements. For subsets we write for and for .
Rank system. A function assigning an integer to each satisfies the rank postulates if
With the number of elements of , the nullity is . An element is dependent on if . A circuit of is a minimal dependent set: a subset with such that for every proper subset of . In Lean these are IsRankSystem r, nullity r N, IsDependentOn r e N and circuitsOfRank r P.
Circuit system. A family of subsets, called circuits, satisfies the circuit postulates (§8, p. 516) if
(C₁) No proper subset of a circuit is a circuit.
(C₂) If P₁ and P₂ are circuits, e₁ is in both P₁ and P₂, and e₂ is in P₁ but not in P₂, then there is a circuit P₃ in P₁ + P₂ containing e₂ but not e₁.
In Lean this is IsCircuitSystem C for a predicate C : Finset α → Prop.
Rank from circuits. Whitney defines (p. 516):
Let e₁, ⋯, e_p be any ordered set of elements of M. Set Γᵢ = 0 if there is a circuit in e₁ + ⋯ + eᵢ containing eᵢ, and set Γᵢ = 1 otherwise (compare Theorem 5). Let the "rank" of (e₁, ⋯, e_p) be r(e₁, ⋯, e_p) = Σ_{i=1}^{p} Γᵢ.
In Lean, rankSeq C l is this sum for a list l, and rankOfCircuits C N is its value on the enumeration N.toList of a subset .
For every finite set :
where is the family of circuits of and is the rank defined from . This is Whitney's closing sentence of §8 (p. 517): "The definitions of rank and of circuits under the two systems (R), (C) agree, and hence the systems are equivalent."
The equivalence makes the circuit postulates a complete description of a matroid: everything stated about rank, nullity, independence and bases can be phrased through circuits and back. Downstream in the same paper, the fundamental sets of circuits of §9 (Theorem 9) and the binary-matroid characterization of the Appendix are stated in terms of circuits, and they depend on circuits and rank being interchangeable. Theorem 5, read on its own, expresses the nullity of a set as a count of circuit-closing steps. This is the abstract form of the fact that the cycle space of a graph has dimension equal to the number of non-tree edges.
On the formal side, Mathlib's Matroid is built on the base axioms and proves circuit elimination (Matroid.IsCircuit.strong_elimination) as a theorem about that structure. Whitney's own route is different: rank defined from circuits by an ordered sum of , with order-independence (Lemmas 7 and 8) as the central step. That route has no machine-checked version that we know of, on Prove2Me or elsewhere. This mission formalizes the 1935 argument as stated: the rank and circuit systems as Whitney wrote them, and the two translations between them.
The obvious definition of the rank of a set from its circuits enumerates the set and counts the elements that do not close a circuit with their predecessors. This definition depends on the enumeration, and nothing in , obviously prevents two orderings from giving different counts. Lemma 7, the swap of two adjacent elements, is where does real work, through a case analysis on which of the two swapped elements closes a circuit. In the other direction, for circuits of a rank function requires turning the local postulate into a statement about unions of two circuits. Defining the circuit rank as a maximum over orderings, or as the size of a largest circuit-free subset, sidesteps exactly the step the paper proves and is not this mission.
α with [Fintype α] [DecidableEq α]. The ground set is all of α, and subsets are Finset α. Whitney's matroid is a finite set .ℤ), so that is a true difference.N.toList. Its independence from the enumeration is Lemma 8, and the definition does not build it in.Matroid in the statements. Doing so would turn the equivalence into a library lemma. The statements are about Whitney's postulates on bare functions and predicates.The development needs only finite sets, lists and permutations from Mathlib. The definitions IsRankSystem and IsCircuitSystem can be reused for the other cryptomorphisms of the paper. Contributions are welcome on any milestone, and so are local helper lemmas, such as monotonicity of rank under – or invariance of rankSeq under prefix-preserving changes.
Mathlib/Combinatorics/Matroid/Circuit.lean (circuits of Mathlib's Matroid). https://github.com/leanprover-community/mathlib4A firm holds a fixed stock of a perishable or seasonal product: airline seats, hotel rooms, fashion goods, tickets. It must sell the stock over a finite season, and whatever is left at the end is worth nothing. The firm can change its price at any time, and demand responds to the price at random. Should it adjust its price continually as sales occur and time runs out, or is one well-chosen price nearly as good?
Gallego and van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons (Management Science 40(8), 1994, doi:10.1287/mnsc.40.8.999), set up this question as a continuous-time stochastic control problem and answered it. The source for this mission is the published 1994 article. Its answer is quantitative: the expected revenue of a single fixed price is within a factor of the best possible dynamic policy. The paper is one of the founding results of dynamic pricing in revenue management. The deterministic (fluid) upper bound it introduced became the standard benchmark of the field, and later work on re-solving heuristics, network revenue management and learning-while-pricing builds on it.
Demand. The firm chooses a demand intensity from an interval of allowable rates, and the market charges the inverse-demand price . On nonzero rates, is strictly decreasing and nonnegative; rate corresponds to the null price , at which nothing sells. The revenue rate is . It has , and it is continuous, concave and bounded on . denotes its least maximizer, and , . Such data form a regular demand function (§2.1).
The stochastic problem. At time the firm holds items and has a horizon . A non-anticipating pricing policy chooses the intensity at each elapsed time as a function of the sales history so far. Sales follow a Poisson process with this controlled intensity, and at most items can be sold. A sale at time earns the current price . The expected revenue is , where counts the sales, and the optimal expected revenue is .
The deterministic problem. Replacing random sales by their rates gives
It is solved by the constant rate (Proposition 2).
Fixed-price heuristics. is the expected revenue of charging for the whole horizon. is the expected revenue of the best constant price.
For , and , is finite and positive, and
The result. Theorem 2 says that uncertainty can only cost revenue. The deterministic value is a computable upper bound for every policy, so any heuristic can be judged against it. Theorem 3 turns this into a guarantee: with 400 items and scarce stock, a single price earns at least 97.5% of the optimum. The loss vanishes as the expected sales volume grows. This is the justification for the stable, rarely changed prices seen in practice, and the template for the asymptotic-optimality analyses that followed: fluid bounds, re-solving, bid prices.
Formalizing it. The results are proved on paper, and none is formalized. The platform has a discrete-time Bernoulli analogue of Theorem 2 (Talluri–van Ryzin, RevenueManagement.deterministic_upper_bound) and Bitran–Caldentey's periodic-review version as open items. Neither is this continuous-time model. A formalization would add a controlled Poisson sales process with a policy-dependent intensity, the compensator identities (13)–(14) for it, and a Lagrangian-duality argument over measurable rate paths. These are reusable for every continuous-time revenue-management model on the platform. Gallego's moment bound (18) is already proved there.
The deterministic side (Proposition 2, the duality gap) is convex analysis on one concave function. The fixed-price bounds reduce to a Poisson computation and (18). The obstacle is Theorem 2's stochastic step. The revenue is collected at random jump times chosen by an adaptive policy, and comparing it with a deterministic integral requires the compensator identity for an arbitrary non-anticipating intensity. The paper cites Brémaud's martingale theory for this, which Mathlib does not have. A first idea is to apply Jensen's inequality to directly. It fails because the stock constraint holds only pathwise, through , and not in expectation for a rate path. Restricting to Markovian policies does not remove the need for the identity.
RevenueManagement.*).PricingRM.DetHeuristic.*).A controller often cannot see the state of the system it steers. It sees only measurements that are noisy functions of that state. In operations research this happens in machine maintenance and inspection, in queues observed only partially, and in inventory systems with inexact stock records. In control engineering it is the usual case. The question is what the controller should base its decisions on. The full record of past measurements is the obvious choice, but that record grows with time, so a law that uses it is a function on a space whose dimension grows with the horizon.
K. J. Åström's 1965 paper Optimal Control of Markov Processes with Incomplete State Information answered this question for finite Markov chains. The answer is that the conditional distribution of the hidden state given the measurements is a sufficient statistic. The problem with incomplete information is equivalent to a problem with complete information whose state is that distribution. This is the model now called a partially observable Markov decision process (POMDP), and the conditional distribution is now called the belief state.
Timeline. For linear systems with quadratic cost and Gaussian noise, the separation theorem of Joseph and Tou (1961) and Gunckel and Franklin (1963) says that the optimal control is a fixed function of the conditional mean of the state. Åström (1965) proved the reduction for finite-state Markov chains with arbitrary costs, with the conditional distribution as the new state. Smallwood and Sondik (1973) showed that for finite horizons the value function is piecewise linear and concave in the belief, which made exact computation possible. Bertsekas and Shreve (1978) and Bäuerle and Rieder (2011) gave the reduction for general Borel models.
The hidden state , , takes values in a finite set . The controls range over a compact nonempty set . The state moves by the transition probabilities , which are continuous in . The state is observed through outputs in a finite set , with , conditionally independent given the states. The law of is . An instantaneous cost , continuous in , is paid at each time.
A control law chooses from the outputs observed so far, . With moving to , a law determines the joint law of and the expected cost
Problem P.1 is to find an admissible law minimizing (2.6).
The conditional state distribution is . It is updated by Bayes' rule: with and , the output gives , and is the probability of that output. The cost-to-go is the minimal expected cost of the steps when has distribution , with . Problem P.2 controls the process directly: a law chooses from to minimize .
P.1 has a solution if and only if P.2 has one. For every solution of the functional equation
with attaining the minimum, the law
is optimal for P.1 and for P.2, among all admissible laws of each, and both minimal values equal .
The result. Theorem 3 replaces a minimization over functions of ever longer measurement records with a recursion over a fixed space, the probability simplex over the states. Every exact and approximate POMDP algorithm starts from it: value iteration on beliefs, the piecewise-linear representation of Smallwood and Sondik, point-based methods. It also splits the controller in two. A filter computes in real time, and the function can be computed off-line. This is the decomposition the paper draws on p. 189, and it extends the linear-quadratic separation theorem to arbitrary finite chains.
Formalizing it. The theorem is proved. The platform has the reduction in Bäuerle and Rieder's discounted Borel model with an observable state component and rewards in extended reals. It does not have Åström's model: finite chains, time-dependent transition matrices, an unobservable state, costs, and laws of the raw output history. This mission formalizes Åström's statements as he gives them. The cost (2.6) is defined from the joint law of states and outputs, and the comparison classes are all laws of the outputs (P.1) and all laws of the distribution history (P.2). The finite setting makes every expectation a finite sum, so a complete development needs no measure theory.
The obvious argument is backward induction on the conditional distributions. The difficulty is that depends on the controls already used, so it is not given in advance: the state of the reduced problem is produced by the law being optimized. It has to be shown that the expected cost of an arbitrary law of the outputs, computed from the joint law, splits as the reduced recursion says. In particular, laws that use more of the record than must gain nothing. Restricting the comparison class to laws of the form assumes this conclusion.
A second difficulty is attainment. "Min" in (3.28) and "has a solution" presuppose that minima over are attained, which needs continuity of on the simplex. The weights can vanish, and then the update is undefined.
States and outputs are finite types, St and Obs, with the chain given by the structure Model. Controls are Fin r → ℝ, and is compact and nonempty. The law of is the datum in place of the paper's law of , since no control exists. The transition from to uses and the matrix . Times are indexed by Fin N as .
The norm is the norm l1, not Mathlib's sup norm. Conditional distributions are ratios of path sums, condState, and are claimed only on output histories of positive probability. When the update is the zero vector and is always multiplied by .
The cost-to-go costToGo is an infimum over admissible tail laws. Its index set is nonempty and the costs are bounded below, so the real infimum is a true infimum. It is never defined through (3.28), since that would make Theorem 1 circular. The P.2 functional sums branch by branch over the outputs, with weights . "Given by Theorem 1" is read as " attains the minimum in (3.28)" (IsSolution328).
The goal is not the bare equivalence of solvability. In this compact, continuous, finite setting both problems always have solutions, so that sentence alone is trivially true. The goal also requires the law to be optimal in both problems, against every admissible law, with equal minimal values.
Reusable beyond this mission are the finite POMDP model, the joint path law, the Bayes filter and the belief-MDP kernel. Welcome contributions include proofs of the milestones, the continuity of on the simplex, and existence of solutions of (3.28).
Least-squares regression fitted by stochastic gradient descent — the least-mean-square (LMS) algorithm — is the basic large-scale learning procedure: each observation is touched once, at a cost linear in the dimension. Classical analyses of stochastic approximation give the rate for non-strongly-convex objectives, and when the objective is -strongly convex. For least squares, is the smallest eigenvalue of the input covariance, which in high-dimensional problems is close to zero, so the strongly convex rate is often worse than the non-strongly-convex one.
F. Bach and E. Moulines (arXiv:1306.2119, NeurIPS 2013) showed that for the square loss this dichotomy disappears: averaged LMS with a constant step size reaches the rate with no strong-convexity assumption, and with a constant that does not involve the smallest eigenvalue. Averaging of stochastic approximation iterates goes back to Polyak and Juditsky (SIAM J. Control Optim. 1992), whose guarantees are asymptotic and use decreasing step sizes. The proof technique for the expansion of the noise process is adapted from Aguech, Moulines and Priouret (SIAM J. Control Optim. 2000). This mission formalizes the non-asymptotic bound in expectation (Theorem 1 of the paper) and the chain of lemmas of its Appendix A.
Let with , inner product and norm . For , is the operator . For self-adjoint operators, means that is positive semi-definite.
The data are independent and identically distributed pairs , , with finite second moments. The covariance operator is , assumed invertible (its eigenvalues may be arbitrarily small). The least-squares objective
attains its global minimum at , and is the residual. The model need not be well specified: need not vanish. Two constants satisfy
These are assumptions (A1)–(A6) of §2.1. The LMS recursion with constant step size , started at , is
and its average is .
For every step size and every ,
The constants are the paper's. A companion item states the case , where the bound reads .
The result. Theorem 1 gives a finite-sample, dimension-explicit bound with two terms: a variance term , which matches the minimax rate for least-squares regression, and a bias term . Neither involves the smallest eigenvalue of , so the guarantee survives ill-conditioning, which is the regime of high-dimensional learning. The bound is the basis for the paper's later results: the high-probability bound (Theorem 2) and the constant-step algorithm for logistic regression (Theorem 3), whose analysis invokes Theorem 1 for the quadratic approximations.
Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge no part of it has been machine-checked. A formalization yields a reusable layer for linear stochastic approximation in finite dimension: martingale-difference noise in , second-moment bounds for linear recursions driven by random operators, Loewner-order arguments, and averaging. The lemmas are stated for an abstract filtration and an abstract operator , so they apply beyond this model. The mission also records the corrections the appendix needs (an "" that should be "" in (13), an index in (16), and the exponent of in A.5).
Two steps resist the naive approach. First, the obvious one-step analysis — expand and take expectations — yields the bias part and Lemma 1, but on the noise it gives only , which does not decrease with . The rate requires averaging to cancel the noise, and this cancellation is visible only for the recursion with replaced by its mean . The random recursion is therefore expanded in powers of around the mean recursion, and each term needs its own covariance bound, by induction on , using the independence of from . Second, the induction relies on Loewner-order bookkeeping: sums of must be bounded uniformly in without dividing by small eigenvalues.
The space is EuclideanSpace ℝ (Fin d). Operators are continuous linear maps, and is an explicit two-sided inverse. Observations are indexed from . Averages are , with in every statement that uses them. The covariance operator is defined by its bilinear form, . Every Loewner inequality whose sides are expectations is an inequality of quadratic forms (for example for all ), which is the same order for self-adjoint operators.
Lean's Bochner integral is on non-integrable functions, so every moment assumption carries the integrability of its integrand, and every bounded expectation in a conclusion is paired with an integrability conjunct. Without these, a heavy-tailed would satisfy (A6) vacuously and a conclusion could hold through the value ; neither formalization is acceptable. Independence is of the pairs , not of and separately. (A4) is attainment of the minimum, not a gradient condition.
The following hypotheses are added to the page and disclosed in each item:
A complete development needs:
All of these are reusable for other stochastic-approximation missions. Proofs of any milestone are welcome, as are alternative arguments for the noise bound that avoid the expansion.
Policy gradient methods optimize a parameterized policy of a Markov decision process by gradient ascent on its expected discounted return. They are among the most widely used methods in reinforcement learning, from REINFORCE (Williams 1992) and the policy gradient theorem to natural policy gradient and trust-region methods. The objective is not concave in the policy, even when the policy is a raw table of action probabilities, so standard optimization theory guarantees at best convergence to a stationary point, and it was long unclear whether or how fast these methods find an optimal policy.
Agarwal, Kakade, Lee and Mahajan (JMLR 2021) give a systematic answer for the tabular and function-approximation settings. This mission formalizes their warm-up result, Theorem 4.1: projected gradient ascent over the simplex of stochastic policies reaches an -optimal policy after a number of iterations polynomial in the sizes of the MDP, the effective horizon , , and a distribution mismatch coefficient. The gradient domination idea it rests on goes back to the analysis of conservative policy iteration by Kakade and Langford (2002) and to Scherrer and Geist (2014).
A finite discounted MDP consists of finite sets of states and of actions, a transition kernel , rewards and a discount factor . A policy assigns to each state a probability distribution over actions. Its value from a start state is
and for a start distribution , . The action value is and the advantage is . The discounted state visitation distribution is . An optimal policy maximizes at every state simultaneously; .
In the direct parameterization the parameter is the table itself, , a point of the product simplex . The algorithm optimizes for a chosen start distribution by projected gradient ascent
where is the Euclidean projection and . Performance is measured under a possibly different distribution , and the distribution mismatch coefficient (componentwise ratio) measures how well covers the states an optimal policy visits from .
With step size , from any initial policy, for every and ,
The theorem shows that, for the simplest constrained parameterization, a first-order method finds a globally optimal policy at a polynomial rate in spite of non-concavity. The guarantee holds for every performance distribution at once, and it isolates the role of exploration in a single quantity, the mismatch coefficient; Section 4.3 of the paper shows that without a well-covering gradient methods can need exponentially many steps. Lemma 4.1 and the smoothness bound are reused across the rest of the paper, and the performance difference lemma underlies essentially all of its analyses.
All results here are proved in the paper, with Theorem E.1 and Theorem E.2 cited from Beck (2017) and Ghadimi–Lan (2016). None of them has a machine-checked proof on the platform. A formal development provides a verified link between the policy gradient expression of the direct parameterization and a standard nonconvex projected-gradient rate, and a reusable formal library of discounted visitation distributions, the performance difference identity, and projected gradient methods on Euclidean spaces.
The obvious argument, "projected gradient ascent converges to a stationary point, and stationary points are optimal", fails on both counts as stated. Stationary points of need not be optimal when does not cover the relevant states; the quantitative replacement is gradient domination, which only controls suboptimality through the mismatch coefficient. The convergence rate itself requires smoothness of the value as a function of the policy table, which is a bound on second derivatives of a matrix inverse with the dependence and the factor made explicit. Finally, the near-stationarity delivered by the gradient-mapping rate is at the next iterate, not the current one, which is why the conclusion is over . On the Lean side, the value is an infinite series in the policy entries, so its differentiability and the exact gradient formula have to be established for a function defined on the whole parameter space.
Policies are parameter vectors in EuclideanSpace ℝ (S × A), so norms are and Mathlib's gradient is ; the objective is defined on the whole space and is only ever evaluated, with its gradient, at policies. The MDP layer (transition kernels, policies, , , occupation distributions, optimal policies) is the published FoundationsML.ReinforcementLearning library; is the unnormalized discounted sum. The projection is any map satisfying the nearest-point property. The optimal policy is a hypothesis IsOptimalPolicy (optimal from every state), not a supremum over all functions.
Conventions committed to:
A formalization that defines the update through formula (7), that assumes gradient domination or smoothness as hypotheses of the goal, or that takes the gradient off the simplex where the value series may diverge, would trivialize the goal; the goal mentions none of these, and (7) is a milestone theorem.
A complete development needs: summability and differentiability of the value series near the simplex; the performance difference lemma; the Euclidean projection inequality on a closed convex set; the descent lemma for functions smooth on a convex set; and the gradient-mapping argument. The projection and gradient-mapping results are independent of reinforcement learning and reusable. Contributions to any milestone are welcome, as are proofs of Theorem E.2 (Ghadimi–Lan) as a stepping stone to Proposition B.1.