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?
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.
A firm that sets prices without knowing how demand responds to them has to learn the demand curve from its own sales. Each price it charges is both a revenue decision and an experiment. The natural policy, certainty equivalent pricing, re-estimates the demand parameters after every period and charges the price that would be optimal if the estimates were exact. den Boer and Zwart show that this policy can fail: with positive probability its prices settle at a suboptimal value, because they converge too fast for the estimates to keep improving (den Boer–Zwart 2014, Proposition 1, the subject of the companion mission). The same phenomenon was found by Lai and Robbins (1982) for a linear control problem.
Their remedy, Controlled Variance Pricing (CVP), keeps certainty equivalent pricing but forces the sample variance of the chosen prices to decay no faster than . The main result is that this small amount of enforced exploration gives regret , hence for every , for a broad class of demand models that are specified only through their first two moments. Keskin and Zeevi (2014) later placed CVP in a larger family of semi-myopic policies with regret for linear demand.
A seller chooses in each period a price , with , and then observes demand . Demand at price has mean and variance , where the link and variance function are known and on , , and the parameter with is unknown. The noise is a martingale difference with conditional variance and a uniformly bounded conditional moment of some order .
The expected revenue is . Near it has a unique maximizer in the open interval with there, and . The regret of a policy is
The estimate is the maximum quasi-likelihood estimate (MQLE), the root of the quasi-score equation (3), . With and the sample mean and variance of , the taboo interval is with . CVP starts from two distinct prices , fixes and , and for : if does not exist or has the wrong signs, it charges whichever of is farther from ; otherwise it charges if that keeps , and the best price outside if not.
stated as: there is , depending on the model, , and the initial prices but not on , with for all . The constant is left free, so the statement survives any sharpening of the constants.
The theorem shows that a policy that is certainty equivalent almost all of the time, with a single interpretable tuning parameter , attains regret in generalized linear demand models, without distributional assumptions beyond two moments. It explains the role of precisely: is the cost of exploration and the cost of estimation error. Proposition 2 and Lemma 1 are reusable for any policy that enforces a variance floor on its actions, and (11) is a self-contained rate for least squares under adaptively chosen designs.
The result is proved in the paper, with Proposition 3 delegated to den Boer and Zwart (2012) for general links. To our knowledge none of it has been machine-checked. A formalization would verify the delegated consistency argument, fix the conditions under which it applies (see Formalization scope), and provide a Lean development of adaptive least squares and quasi-likelihood rates that the related Keskin–Zeevi missions also need.
The deterministic parts are short. The difficulty is Proposition 3. The prices are chosen adaptively from past data, so the regressors are not independent of the noise, and standard rates for (quasi-)likelihood estimates do not apply. The natural argument, bounding by with a self-normalized martingale quadratic form, needs a bound that holds in expectation and not only almost surely, as in Lai and Wei (1982). For a non-linear link the MQLE is defined only implicitly, and its existence near has to be shown first, with a moment bound on the last time it fails. That is the random time . Turning almost-sure consistency into a rate in expectation is where most of the work lies.
All declarations live in the namespace CVPricing.Regret. Periods are 1-based. Prices, demands and parameters are real; with the Euclidean norm (euclidNorm), not Mathlib's sup norm. The design matrix, sample mean and are the published Keskin–Zeevi definitions fisherOf, avgPriceOf, infoMetricOf. Every is "there is such that for all ", with quantified after the model data. Rates are stated for and the regret for . and are total functions constrained on . A root of (3) counts only where for every observed . CVP is a predicate on a realized path that allows every maximizer in (7) and (8).
Disclosed deviations from the page:
Corrected slips: Proposition 2 is stated for , because the printed range fails at (, not ). Theorem 1 keeps the printed range. Eq. (20) is stated for and for beyond an explicit threshold.
The goal does not assume the variance bound, consistency or (20). The policy contains the variance check and the taboo interval, and the regret is the expectation over the actual price process. A statement that assumed any of these, or that dropped the taboo step, would be trivial or false. Contributions are welcome on adaptive least squares (Sherman–Morrison and determinant-ratio bounds), martingale last-time moment bounds, and the implicit-function step (18).
A seller who does not know how demand responds to price has to learn the demand curve from its own sales while it is selling. The most natural policy is certainty equivalent pricing (also called myopic pricing or passive learning): after every period, estimate the unknown demand parameters from all data collected so far, and charge the price that would be optimal if the estimates were the truth. It is simple, uses all data, and is what a price manager would do without further thought.
den Boer and Zwart (Management Science 60(3):770–783, 2014) show that this policy can fail. In the linear-demand, Gaussian-noise model, the prices it produces fail to converge to the optimal price with positive probability: the policy is not strongly consistent. The result motivates the paper's main contribution, controlled variance pricing, which adds just enough price dispersion to keep learning (treated in the companion mission of this series).
The phenomenon has a history in adaptive control:
A monopolist sells one product in periods at prices from an interval with . The demand in period is
where are independent random variables. The parameters are unknown to the seller and satisfy , , , . The expected revenue at price is , maximized at the optimal price
Certainty equivalent pricing charges two different initial prices in . After periods it computes the least squares estimates , the solution of the normal equations , and charges
with when the estimated slope is nonnegative.
The goal states only the failure of convergence, for every admissible parameter and every pair of different initial prices; it does not fix where the prices go.
This is what the paper's argument establishes; since it implies the goal.
The milestones are the displayed steps of the appendix proof, in attack order: the determinant of the coefficient matrix of the linear system (12); the bound for ; positivity of the probability of an explicit event on the noise for large ; the case (the first fitted line pushes to ); the representation of the least squares error; recursive and closed forms of and ; and the deterministic induction that every noise path in keeps the price at forever.
The result is the standard counterexample to certainty equivalence in dynamic pricing. It shows that estimation and optimization cannot be separated naively: a policy that always exploits its current estimate can lock itself into a price at which the data no longer move the estimate enough to correct it. Every later policy in this literature that forces exploration (controlled variance pricing, semi-myopic policies, constrained iterated least squares) is designed against this failure, and its necessity is argued by pointing to results of this kind.
The result is proved in the paper; nothing here is open. To our knowledge it has no machine-checked proof. Formalizing it adds:
The obvious heuristic, "with positive probability the first two observations are so noisy that the fitted slope is wrong", is not enough: one bad estimate is corrected by later data unless the policy stops generating informative data. The proof has to control the whole infinite future. It does so by showing that on a single event, defined through the first two noise values and a uniform bound on all later running means, the price stays at forever, which requires the closed form of the least squares estimate along a price path that is constant from period 3 on. That event involves infinitely many noise variables, so its probability is positive only through a maximal inequality, and independence between and the later noise. A second subtlety is the choice of constants: the size of the band enters the conditions on , so the order in which and the set of admissible are chosen matters (the printed proof picks them in a circular order; a non-circular choice exists).
CVPricing.CertEquiv.Model bundles with the standing assumptions of §2 as fields, including (the paper's neighbourhood assumption specialized to linear demand). The noise is the referenced published definition RobustBooking.Shared.GaussianNoise (measurable, mutually independent, each ); its Lean index is period , so the paper's is ε (i - 1).cePrice is a deterministic recursion on a noise path, so the random price process is obtained by evaluating it at . Periods are 1-based. The least squares estimate is the referenced KeskinZeevi.SufficientConditions.lsEstimateOf, the solution of the normal equations (4), unique whenever . The certainty equivalent rule is the projection of onto when , and when ; the latter is the convention the paper's proof adopts for wrong-signed estimates.The lost-sales inventory problem with lead times is a basic model of operations management. A retailer reviews one product's stock each period and places an order that arrives periods later. Demand that cannot be met from stock on hand is lost, and the retailer pays a holding cost per unit left on the shelf and a penalty per unit of lost demand. The optimal policy depends on the whole pipeline of outstanding orders, so the state space grows with , and the problem is computationally hard for long lead times. Simple base-stock (order-up-to) policies are therefore the standard heuristic, and Huh, Janakiraman, Muckstadt and Rusmevichientong (Management Science 2009) showed they are asymptotically optimal as the lost-sales penalty grows.
Agrawal and Jia (arXiv:1905.04337) study the learning version, in which the demand distribution is unknown and only sales, not demands, are observed. They give an algorithm whose regret against the best base-stock policy is , improving the earlier bound of Zhang, Chao and Shi, which grows exponentially in . The improvement rests on one structural fact: started from two different states, the base-stock system accumulates expected costs that differ by an amount linear in and independent of the horizon. That fact, Lemma 2.5 of the paper, is the goal of this mission.
Fix a lead time and a base-stock level . A state is a vector of real numbers. Its entry is the on-hand inventory after the current period's arrival, and are the outstanding orders, the most recent. Under a base-stock policy with level the states lie in
In each period a demand is drawn, independently across periods, from a distribution on . The sales are and the on-hand inventory is . The policy reorders exactly what was sold, so for the next state is
and for the state never changes. The pseudo-cost of period is , and the value over horizon from the start state is
Along a demand path, is the total sales and the total on-hand inventory.
States are compared by the order of Definition B.1: if with and some such that for and for . Thus holds the same total, shifted toward the shelf. The state dominates every state of .
For every , every horizon , all costs , every demand law and all ,
The constant is the paper's printed one. The proof's last display gives , a stronger bound, which is deliberately not the goal.
All of the following hold for , along any single demand path that drives both chains:
Lemma 2.5 bounds the dependence of the base-stock chain's finite-horizon cost on its starting state, uniformly in the horizon. In the paper it yields three consequences: the long-run average cost (the loss) of a base-stock policy does not depend on the initial state (Lemma 2.6), the bias of the chain is bounded by (Lemma 2.8), and finite-horizon average costs concentrate around the loss (Lemma 2.10). These feed the regret bound of Theorem 1.3. The lemma is also a statement about the base-stock lost-sales system alone, without any learning, so it is of independent interest for coupling arguments on lost-sales chains.
The paper's proof is complete on paper, but nothing in it has a machine-checked proof. Neither the lost-sales base-stock chain with lead times started from an arbitrary pipeline state nor any of the coupling lemmas of Appendix B is formalized elsewhere. This mission produces a checked proof of the goal and of the pathwise comparison lemmas. Theorem 1.3 is not posed: its supporting lemmas rely on limits whose existence the paper settles only by an informal discretization (Remark 4).
The obvious argument couples the two chains on a common demand path and waits until they coalesce. Coalescence is guaranteed only after consecutive periods of zero demand, an event of probability exponentially small in , so this argument gives a bound exponential in . That is the bound of earlier work.
The linear bound needs a finer pathwise accounting. The two coupled chains do not stay ordered: the one that starts with more inventory on the shelf sells more at first, then runs short and sells less. The order between the two states alternates along a sequence of times, and the sales gained in one phase must be shown to be lost again in the next, so that the cumulative difference stays bounded by a constant multiple of for every horizon. Turning this alternation into a bound requires tracking how the pipeline vectors evolve between alternation times, including the boundary cases in which the chains coalesce or the horizon ends inside a phase.
All declarations live in the namespace LostSalesLearning.ValueGap. A state is a function Fin (L + 1) → ℝ, a demand path is a function ℕ → ℝ≥0, and time is 0-based: traj s d 0 is the paper's , traj s d t is , and is a sum over Finset.range T. The demand law is a probability measure on ℝ≥0, and the demand path has the product law Measure.infinitePi (fun _ => F). The value is the expectation of the summed pseudo-costs, which equals Definition 2.4 by the tower property and is the form used in the paper's proof.
Committed conventions:
alternationTimes; an absent next crossing is none.Two trivializing formalizations are ruled out. A comparison of the two values on different or fixed demand paths would be a different statement: the goal compares two expectations under the same law, and each pathwise milestone uses one common path. A Bochner integral of a non-integrable function would be . The integrand here is measurable and bounded by on , so the values are genuine expectations.
A complete development needs the elementary dynamics of the chain, including invariance of and the shift of trajectories, which is reusable for other lost-sales models. It also needs the alternation times of Definition B.4, and measurability of the trajectory in the demand path. Proofs of individual milestones, alternative proofs of the goal, and sharper constants as separate statements are all welcome.
Many large convex programs have far more constraints than can be handled at once, but each constraint on its own is simple: a single linear equation or inequality. Row-action methods exploit this by touching one constraint per iteration. L. M. Bregman's 1967 paper (DOI 10.1016/0041-5553(67)90040-7) introduced the general framework behind most of them. A strictly convex function induces the "distance" , now called the Bregman distance, and the method moves from point to point by -projections onto one constraint at a time. For this reduces to Hildreth's method for quadratic programming; for entropy-type it gives the balancing (matrix scaling) methods used for transportation and traffic problems. The later literature on Bregman projections, mirror descent and entropic regularisation starts from this paper.
This mission formalizes the last main result of the paper, Theorem 4 (p. 212), which treats linear inequality constraints. Here a plain projection cycle does not minimize . Bregman's fix carries a vector of nonnegative multipliers along with the primal point and lets each step either move towards a violated constraint or relax a multiplier. The result is a primal–dual method.
Timeline. Hildreth (1957) gave the quadratic case. Bregman (1967) proved the general theorem stated here. Censor and Lent (1981) revisited the method for interval constraints under explicit assumptions on Bregman functions (DOI 10.1007/BF00934676).
Let be -dimensional Euclidean space and a convex set. Let be strictly convex on , continuously differentiable over with gradient , and continuous over the closure . Let be an matrix () with nonzero rows , and . The inequality program (2.11)–(2.13) is
with feasible set , assumed nonempty. The Bregman function is (1.4). The -projection of onto the hyperplane minimizes over . The standing hypotheses ("the conditions of Theorem 3") are that satisfies the abstract conditions I–VI of §1 for these hyperplanes, together with condition (2) of Note 1: implies . In addition, -projections of interior points of stay in the interior. Condition V (compact sublevel sets of ) is used for .
Write , where , and . A run of the method is a sequence of pairs with , , , and cyclic indices . Each step with is one of the following:
For every run of the method,
Theorem 4 says that a method using one constraint per step and only 's gradient converges to the minimizer of a strictly convex function over a polyhedron intersected with . Its multipliers form a dual sequence. Note 4 of the paper deduces from the theorem that the optimal value equals over dual-feasible pairs (, ). The theorem is the convergence statement behind Hildreth's algorithm, behind entropy-based balancing for linear inequality systems, and behind the later "interval convex programming" methods.
The theorem is proved on paper, but no machine-checked proof of it, or of any Bregman-projection row-action method, is known to exist. The formalization adds two things. It makes the paper's standing hypotheses explicit, since several are stated once or left implicit. It also forces a complete argument for the convergence of the whole sequence: the printed proof gets this from condition (2) by an argument that assumes a monotonicity property established in §1 for the pure projection method but not for the primal–dual one. A Lean proof of the goal therefore also supplies a complete proof of the paper's claim.
The standard argument for projection methods uses a Fejér-type property: decreases for every feasible . That fails here. In case (c) the point moves away from the hyperplane of a satisfied constraint, and can increase. So any argument has to control primal and dual quantities together. To pass from "every limiting point is feasible" to "the whole sequence converges to an optimal point", complementary slackness has to hold in the limit, and this depends on the cyclic order and on the cap . The naive route, applying the §1 convergence theorems to the hyperplanes , does not apply, because the iterates are not -projections onto fixed sets in case (c).
EuclideanSpace ℝ (Fin p); the rows are vectors , and is . The gradient is explicit data tied to by HasGradientWithinAt on . is not assumed open, and is continuous on .Many decision problems are solved repeatedly against data that arrive over time: routing traffic, allocating budgets, choosing portfolios or combinatorial structures. Online linear optimization models this. At each round a learner picks a decision from a fixed domain , then a reward vector is revealed and the learner earns . Performance is measured by regret, the gap to the best fixed decision in hindsight. When is combinatorial (paths, spanning trees, assignments), the only computationally reasonable access to is a procedure that optimizes a linear function over it, and in practice such procedures are often only approximate.
Follow the Perturbed Leader (FPL), introduced by Hannan (1957) and analysed for linear optimization by Kalai and Vempala (JCSS 2005), uses exactly one call to an exact linear optimizer per round and achieves regret over arbitrary, not necessarily convex, domains. Ben-Tal, Hazan, Koren and Mannor (arXiv:1402.6361, Operations Research 2015) needed a version of FPL that works with an additively approximate linear optimizer, as a building block for oracle-based robust optimization with linearly parametrized uncertainty sets. Their §3.3 analyses this variant and proves Theorem 6, the goal of this mission.
Fix a dimension , a domain (arbitrary: not necessarily convex, closed or bounded) and . An -approximate linear optimization procedure over is a map such that, for every ,
Reward vectors are fixed in advance (an oblivious adversary). Write , with , and .
Follow the Approximate Perturbed Leader with parameter plays at round
Three scale parameters enter the bound: bounds the diameter of , for ; bounds ; and bounds how much each reward varies over the domain, for .
With , for every ,
For every and ,
Theorem 6 shows that perturbed-leader online linear optimization is robust to additive error in its optimization subroutine: an -approximate oracle costs only extra regret, so the average regret is . This allows the algorithm to be run over domains where exact linear optimization is intractable but a good additive approximation is available, and the paper invokes it as the online-learning primitive of its oracle-based scheme for linearly parametrized uncertainty in §3.2 (that application is not part of this mission). Unlike online gradient methods, it requires no convexity of and no projection.
On the formal side, no regret bound for Follow the Perturbed Leader, exact or approximate, is currently formalized on the platform, and the Kalai–Vempala stability argument (comparing a uniform distribution on a cube with its translate) is a reusable piece of measure theory. The mission's statements are proved on paper; the work here is to formalize those proofs, with one correction to a hypothesis, explained under Formalization scope.
Lemmas 7 and 8 are deterministic and combinatorial. The substance is Lemma 9. It compares the expectations of one bounded function of under the uniform law on a cube and under its translate by . The natural first attempt, a pointwise comparison of and , fails: an approximate (even an exact) maximizer can jump arbitrarily under an arbitrarily small change of its input, and is not assumed continuous or even consistent between nearby inputs. Any valid argument must therefore control the two distributions as a whole rather than the decisions point by point, which in the formal development involves Lebesgue measure on , conditioning on a box and translation invariance.
A second subtlety is that the stability bound depends on how is read, which is the reason for the correction below.
Vectors are Fin n → ℝ with dotProduct. All quantities are written as , never with the default norm (the sup norm). Rewards are a function f : ℕ → Fin n → ℝ read at , and is prefixSum f t. The perturbation law is Lebesgue measure conditioned on the cube (ProbabilityTheory.cond volume), a probability measure for . Maxima over are expressed as "for every ", so neither attainment nor boundedness of is presupposed.
Conventions and deviations, each also stated in the affected item:
A trivializing formalization is ruled out: must return points of (otherwise would not bound ), it must be measurable, and the perturbation law is the normalized uniform distribution, not Lebesgue measure restricted to the cube (which is not a probability measure for ).
Needed infrastructure: the overlap estimate for a cube and its translate, , and the integrability of bounded measurable functions of . Both are reusable for any perturbation-based online-learning analysis; contributions of these as standalone lemmas are welcome.