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 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.
In robust optimization, a decision must satisfy a constraint for every parameter value in a prescribed uncertainty set. A nonlinear uncertain constraint can be difficult to use directly because it contains a universal condition over a continuum of parameters. Ben-Tal, den Hertog, and Vial study constraints whose value is concave in the uncertain parameter. Their Theorem 2 replaces the universal condition by one inequality involving a new vector and two conjugate functions. The replacement is the general framework used for the paper's later examples, including uncertainty regions assembled from simpler sets and nonlinear functions whose conjugates have explicit forms. The discussion paper, §§2–4 is the source for this mission; theorem and page numbers refer to that 2012 version.
The paper's result extends a more specialized counterpart for a linear uncertain constraint under a φ-divergence uncertainty region. That 2013 result has a proved formalization on Prove2Me, but its divergence-specific conjugate and uncertainty set are different objects. The same earlier formalization also supplies a proved version of the self-concordant-barrier statement that this paper quotes as Lemma 33, with a differently printed constant. Neither earlier theorem supplies the general concave-constraint result here.
Fix dimensions . The nominal vector is , and maps a primitive uncertainty to an uncertain parameter . Thus the uncertainty set is . The paper assumes that is nonempty, convex, and compact, with in its relative interior . Relative interior is taken inside the affine hull of a set, so may lie in a lower-dimensional plane.
A decision is . For each decision, is the effective domain of the uncertain constraint : is real on and is interpreted as outside it. The function is concave in on for every ; the paper imposes no convexity assumption in the decision . The robust constraint (RC) is for every . In the domain representation used here, this means every . The nominal vector is regular when for every decision , as in Definition 1.
The support function of is . The partial concave conjugate is . Both have extended-real values: an empty support set has support value , and the conjugate can be when its infimum is unbounded below. These values matter in the equivalence; replacing them by a default real number changes the constraint.
The goal is the paper's Theorem 2. Under the standing assumptions and regularity, for every decision ,
The right-hand inequality is the Fenchel robust counterpart (FRC). Its existence claim is essential: equality of primal and dual infima alone would not show that an auxiliary vector satisfying FRC exists.
Four source statements form the milestone path. Remark 5 gives the weak-duality inequality and the FRC-to-RC implication without concavity. Equations (16)–(18) calculate the support function of . Equation (7) states the relative-interior qualification. Equations (13)–(15) state the worst-case/dual-value identity and, through the printed minimum, attainment of the dual infimum. The milestone list quotes those source passages and identifies their printed pages. Theorem 2 and its proof appear on pp. 4–5.
The equivalence gives an exact way to replace an infinite family of uncertain inequalities by an existential constraint. In examples where the support function and concave conjugate can be evaluated or represented with standard optimization constraints, it yields a finite robust counterpart. The conclusion remains a mathematical equivalence even when such an explicit representation has not been found. It is also independent of any convexity of in the decision variable, a point the paper makes after Corollary 3.
This mission supplies reusable, domain-aware support and conjugate definitions and formal statements for the duality path in the paper's central result. The new goal and milestones are open proof obligations: their Lean declarations compile, but they do not yet have machine-checked proofs. The proved 2013 φ-divergence case is narrower and does not close them. A completed development would make the general relative-interior and attained-duality steps reusable for other robust optimization models.
The delicate point is the direction from RC to the existence of an FRC vector. Weak duality gives only a one-sided bound. Identifying the two optimal values still leaves an existence question when an infimum is not attained. The paper invokes Fenchel duality under a relative-interior intersection condition; replacing relative interior by ordinary interior would exclude lower-dimensional uncertainty sets and effective domains that the source permits. A second difficulty is keeping finite and infinite conjugate values distinct while subtracting them in the counterpart inequality. An unbounded-below conjugate must make a finite-support FRC value , not a plausible finite number.
Vectors are functions on Fin m, Fin n, and Fin L; is a real matrix, and dot products use the finite-vector dot product. Mathlib's intrinsicInterior ℝ represents relative interior. The domain map is explicit, with the concavity hypothesis imposed on that domain. The real representative of outside is ignored everywhere. The paper's Notation paragraph calls its generic concave functions closed, but the statements here omit closedness: the finite-dimensional duality qualification used for Theorem 2 needs relative-interior overlap, not that extra regularity. This is a stated strengthening of the source theorem, not a change of its feasible points.
Support functions, conjugates, worst-case values, and dual values use EReal. The paper's “max” in (8), (13), and Remark 5 is read as an extended-real supremum; its “min” in (15) is an infimum accompanied by an attaining vector. The support identity includes , where both sides are , although Theorem 2 keeps the paper's nonempty, convex, compact . On the theorem's hypotheses the support value is finite and is nonempty, so the undefined-looking combinations and cannot occur in FRC. No all-space real-valued substitute for is used, and the theorem still quantifies over every decision and every allowed uncertainty vector.
The proof development needs finite-dimensional relative-interior behavior under affine maps and Fenchel duality with attainment. General convex conjugates and support functions can serve later missions. Corollary 3 and the paper's complexity discussion are outside this mission. Theorem A.1 is not separately made a milestone here: as printed, its domain-restricted dual maximum has a problematic case; the directly used, attained identity (13)–(15) is the target under the main theorem's standing assumptions.
Periodic-review inventory systems face a simple choice each period: how much to order before the next demand is known. When unmet demand is lost, the order can affect the stock available several periods later without preserving a backlog that records earlier shortages. This makes the optimal policy difficult to describe when replenishment takes time. An order-up-to policy offers a practical rule: order enough to bring the inventory position to a fixed level. Huh, Janakiraman, Muckstadt and Rusmevichientong ask when that simple rule performs as well as the best admissible lost-sales policy as the penalty for a lost unit grows. Their working paper, pp. 3–4 and 17–18, proves asymptotic optimality for a particular level obtained from a related backorder system.
The motivating costs are concrete. A lost sale may represent an expedited service part or a missed sale whose cost is much larger than one period of holding inventory. The paper's central comparison concerns the high-penalty regime while holding the demand law, lead time and holding rate fixed. The fixed-level policy can be computed from the distribution of demand over the lead time plus the order period; it does not require solving the full lost-sales control problem. The paper also supplies a finite-penalty bound, which this mission retains as a milestone. Huh et al., pp. 3–4, 17–18.
Let be independent, identically distributed nonnegative demands with finite positive mean. An order takes a fixed integer lead time to arrive. At the start of period , the order placed periods earlier arrives; then a new order is placed, and demand is observed. Unmet demand is lost. At period end, each unit remaining on hand incurs holding cost , and each lost unit incurs penalty . The inventory position counts on-hand units and outstanding orders. An order-up-to- policy raises this position to whenever possible.
Write for the long-run average cost of that policy and for the infimum over admissible policies. The corresponding backorder system retains unmet demand as negative net inventory and charges per backordered unit per period. For an order-up-to level , its stationary average cost is
The newsvendor level is the smallest nonnegative with ; it attains the best backorder order-up-to cost . The paper's Assumption 1 concerns this lead-time demand : if when the conditioning event has positive probability and zero otherwise, then as . Huh et al., pp. 3–4, 9, 11–12.
Fix , and the demand law satisfying Assumption 1. Set . The goal is the equivalent multiplicative form of Theorem 15(b): for every , all sufficiently large satisfy
The infimum over order-up-to levels captures the paper's best such policy. The right-hand comparator remains the infimum over all admissible lost-sales policies. The multiplicative form also covers an almost-surely constant demand law, where both costs can be zero and a literal ratio would be undefined. Huh et al., Theorem 15(b), p. 17.
Theorem 15(a) is a milestone. With and , its factor is
The milestone states the bound where the expected holding quantity in is positive. Earlier milestones state the pathwise comparison of the systems, the two-sided average-cost comparison with penalties and , the lower bound on unrestricted lost-sales optimal cost, the newsvendor formula, and the backorder sensitivity results used by the theorem. Huh et al., Lemmas 5, 9, 13 and Theorems 6, 15, pp. 11–18.
The theorem gives a specific computable stock level whose relative cost loss vanishes in the high-penalty regime. It addresses the gap between a tractable backorder benchmark and the more difficult lost-sales control problem. The finite-penalty factor states how the comparison depends on lead time, holding cost, penalty and the shortage-to-holding ratio; the asymptotic statement alone would not quantify that dependence. The paper establishes these mathematical results; the mission asks for machine-checked proofs of the stated Lean targets. Huh et al., pp. 17–18.
Formalizing the result would also supply reusable infrastructure for coupled inventory systems: measurable demand-path laws, pathwise recursions with delayed delivery, extended nonnegative long-run costs, and a clean comparison between an explicit policy and the infimum over unrestricted policies. The backorder newsvendor and mean-residual-life components can be reused beyond this particular lost-sales model.
The backorder system has a closed stationary cost formula, while a lost-sales order-up-to process generally cannot be replaced directly by that formula. The paper notes that its on-hand inventory distribution need not converge from every starting state, even under a fixed order-up-to policy. One must therefore justify the long-run comparison without assuming stationarity from an arbitrary start. A second difficulty is the benchmark: comparing only against other order-up-to policies is too weak to establish Theorem 15, because the goal uses the optimal cost over all admissible lost-sales policies. Huh et al., pp. 14–16, 18.
Lean reuses the published CappedBaseStock lost-sales model. Its demands are nonnegative and i.i.d. with finite positive mean; and . Period zero in Lean is period one in the paper. Both coupled processes start with zero on-hand stock and an empty pipeline. Inventory is read immediately after delivery, before current demand. Lost-sales costs lie in and use the limsup of expected Cesàro averages; the backorder closed form uses real Bochner expectations under finite-mean demand. The paper's stationary lost-sales cost and this Cesàro cost are identified using its long-run results, but those convergence results are outside this proposal. Huh et al., pp. 14–16.
The paper prints nonnegative rates in Theorem 15, while its displayed newsvendor fraction and shortage-to-holding ratios require positive denominators. Theorem 6(a) therefore states the ratio limit for nonconstant demand laws. The main theorem uses a multiplicative limit bound that also covers constant demand, where the printed ratio is undefined.
The quantity is an infimum over measurable, history-dependent policies with private randomization; no attaining policy is assumed. The backorder optimum is an infimum over nonnegative order-up-to levels. Assumption 1 is imposed on the sum of demands, and the limit is expressed by a positive threshold uniform over all parameter records with the fixed lead time and holding rate. The mission excludes a restricted policy comparator, a fixed penalty, a one-period lead-time specialization, and Assumption 1 on single-period demand. Solvers may contribute proofs of any milestone, along with finite-mean and measurability lemmas needed to connect the model to the backorder benchmarks.
Robust optimization protects a decision against every realization of uncertain data in a prescribed uncertainty set. The standard approach replaces the uncertain constraints by a deterministic robust counterpart and solves that counterpart directly (Ben-Tal, El Ghaoui, Nemirovski, Robust Optimization, 2009). The counterpart is often a harder problem than the original: a robust linear program with ellipsoidal uncertainty becomes a second-order cone program, and a robust quadratic program can become a semidefinite program. A practitioner who has an efficient, specialised solver for the nominal problem may therefore have no efficient solver for its robust version.
Ben-Tal, Hazan, Koren and Mannor (arXiv:1402.6361, Operations Research 2015) ask whether the robust problem can be solved by repeatedly calling a solver of the nominal problem, with the number of calls independent of the dimension. Their first answer, the dual-subgradient meta-algorithm of §3.1, does so whenever the constraints are concave in the noise and the uncertainty set is convex. It is a primal–dual scheme: an online-learning algorithm picks the noise, and the nominal solver answers. This mission formalizes that result, Theorem 3.
Let be a convex domain, a convex uncertainty set, and constraint functions. The robust feasibility problem (3) is
(An objective is handled by binary search on its value, so feasibility is the core question.) A point is an -approximate solution if for all and all .
An -approximate oracle (Figure 1) takes a noise vector and either returns some with for all , or answers "infeasible", which it may do only if no has for all .
The standing assumptions of §3.1 are: each is convex on ; each is concave on for ; for all ; and for , . Write for the Euclidean projection onto .
Algorithm 1 sets and , starts from , and for updates
stopping with "infeasible" as soon as the oracle says so, and otherwise returning . In Lean these are alg1T, alg1Eta, alg1U, alg1X, alg1Output and alg1Calls in the namespace OracleRO.DualSubgrad.
For every -approximate oracle,
and the number of oracle calls is at most .
The result. Theorem 3 turns any approximate solver of the nominal problem into an approximate solver of its robust counterpart, at a cost of solver calls, a number that depends on the geometry of and the sensitivity of the constraints to the noise but not on , or . It is the prototype of the paper's oracle-based reductions: the same primal–dual template, with a different online learner, gives the dual-perturbation algorithm of §3.2–3.3 for non-convex uncertainty sets, and the applications of §4 (robust linear programs, quadratic programs, semidefinite programs) instantiate it.
Formalizing it. The theorem is proved in the paper; none of it is machine-checked. A formal development adds a checked statement of the reduction with an explicit call count in place of the paper's , and a reusable regret bound for projected online gradient ascent on concave rewards (Lemma 1), which the paper quotes from Zinkevich without proof and which many other online-learning results rest on.
The obvious argument for the dual side fails at one point: in round the primal point is computed from , so the reward that the dual player faces depends on its own current move. A regret bound that assumed rewards fixed in advance, or drawn independently of the learner's play, would not apply. Lemma 1 must be used in its adversarial form, valid for every sequence of reward functions, including adaptively chosen ones. A second point is that the projection step requires the variational characterization of a nearest point in a convex set, which a mere "map into " does not provide.
Points are elements of EuclideanSpace ℝ (Fin k), so every norm is the norm. The projection is a predicate IsProjOnto U P (each is a nearest point of to ), not a construction; the oracle is a function (Fin m → E d) → Option (E n) with none for "infeasible", constrained by the predicate IsApproxOracle on inputs in . The goal is quantified over every oracle meeting that specification. The gradient is a given map gradU with HasGradientAt at points of ; no differentiability in is assumed. Rounds are indexed by natural numbers with index for the initialization; the starting primal point , used by the first update and left undefined by the algorithm, is an input. Hypotheses and are added so that and are meaningful. Maxima over are stated as "for every ".
Explicit instantiations and corrections:
Trivializing formalizations are ruled out: an oracle specification under which "infeasible" is never returned, or an output that is not the average of the oracle's answers, would not be Theorem 3. The "infeasible" conclusion is about the robust problem, not the nominal one.
A complete development needs the variational inequality for nearest points in a convex set, the gradient (supergradient) inequality for a concave function differentiable at a point of a convex set, Zinkevich's telescoping argument, and Jensen's inequality for finite averages. The first two and Lemma 1 are reusable beyond this mission. Proofs of the milestones, in any order, are welcome.
A decision maker choosing a random outcome (a portfolio return, a policy's cost savings, a schedule's throughput) often has a reference outcome , the result of a benchmark policy, and wants the new outcome to be preferable to it for every risk-averse decision maker, not just on average. Expected-utility theory (von Neumann and Morgenstern) makes this precise: is preferred to by every decision maker with a concave nondecreasing utility function exactly when dominates in the second order, . Requiring as a constraint in an optimization problem avoids having to elicit any particular utility function, which is rarely possible in practice and impossible when several decision makers must agree.
Dentcheva and Ruszczyński (preprint 2002, published in SIAM J. Optim. 14(2), 2003) introduced optimization problems with stochastic dominance constraints and developed their optimality and duality theory. The central finding is that the Lagrange multiplier of a second-order dominance constraint is itself a concave nondecreasing utility function: the optimal solution maximizes the objective plus an expected utility, for a utility function implied by the problem. This interpretation underlies the later literature on dominance-constrained portfolio optimization, risk-averse stochastic programming, and the dual (quantile) theory of stochastic orders.
Let be a probability space and the space of integrable random variables with its norm topology. For the distribution function is and the second-order shortfall function is
Changing the order of integration gives (2.6), where . The relation means for all , and .
The problem data are a reference outcome , a convex closed set , a functional that is concave and continuous on , and an interval . The paper studies the relaxation in which dominance is enforced on :
The uniform dominance condition (Definition 4.1) asks for some with .
The multiplier class consists of the functions that are concave and nondecreasing, vanish on , and are affine on : for , with a constant . The Lagrangian is
Assume the uniform dominance condition. If is an optimal solution of (3.1)–(3.3), there is with
Conversely, if for some a maximizer of satisfies (3.2) and (4.3), then is optimal for (3.1)–(3.3).
The milestones follow the paper's proof. They are: finiteness of for ; the identity (2.6), already proved on the platform; Proposition 2.3 (convexity and closedness of , and its recession cone); the concavity of the constraint operator with respect to the cone of nonnegative functions; the existence of a nonnegative measure multiplier on satisfying (4.5)–(4.6); the facts that the function (), () of a nonnegative measure lies in and that every is for exactly one ; the key identity
and the weak-duality step: (3.2) implies for every .
With , the dual problem has a solution, its value equals the primal optimal value, and its solutions are exactly the satisfying (4.2)–(4.3).
Theorem 4.2 turns an infinite family of constraints, one for each , into a single scalar trade-off: at the optimum, the decision maker behaves as an expected-utility maximizer for an implicit utility , and the dominance constraint is active exactly in the sense . Theorem 5.1 makes the space of dual variables, which is the starting point of dual decomposition and cutting-plane methods for dominance-constrained problems and of their extensions to several constraints and to higher orders (Sections 6–7 of the paper, not part of this mission).
All results are proved in the paper. Apart from the identity (2.6), which is proved on the platform, none of them is formalized as far as the platform records show. A machine-checked development would provide, on top of the paper, a rigorous treatment of the measure–utility correspondence that the paper obtains from a textbook theorem "after an obvious adaptation", and a careful account of the multiplier class itself (see the scope section on the constant ). The definitions of and of the identity (2.6) are shared with the platform's missions on Dual Stochastic Dominance and Related Mean-Risk Models (Ogryczak and Ruszczyński, 2002).
The necessity half needs a Lagrange multiplier for a constraint taking values in the infinite-dimensional space ; finite-dimensional convex duality does not apply, and the multiplier first appears as a nonnegative measure on , an element of the dual of . A Slater-type point is required: without the uniform dominance condition the multiplier may not exist. This is why the dominance relation, which the paper first poses on all of , is relaxed to a bounded interval : for a reference outcome with a smallest value , , so no can dominate strictly near .
The second obstacle is the translation of that measure into a utility function. The identity (4.9) requires an interchange of integrals over and an integration by parts against the distribution function of an arbitrary integrable , followed by a limit in which the integrability of controls the linear growth of at . The converse direction needs every to be represented by a unique measure, through the left derivative of a concave function.
Outcomes are elements of Mathlib's space Ω →₁[P] ℝ over a probability measure P, coerced to functions inside integrals; no statement is pointwise in . is the published definition DualSSD.Shared.secondPerformance, a Bochner integral of over . The problem data form a structure whose fields include every standing assumption of the paper: convex and closed, concave and continuous on . The constraint (3.2) is stated in its printed expectation form, while Definition 4.1 and the proof objects use , as printed; their equality is (2.6).
Committed conventions:
A trivializing formalization is ruled out: a junk-valued expectation (a Bochner integral of a non-integrable function, which Lean sets to ) cannot occur for , and its integrability is a milestone. Dropping the concavity of or the convexity of would make the necessity half false, so these assumptions are fields of the problem data.
Infrastructure a complete development needs: convex duality for cone constraints in (or a direct separation argument in ), the Riesz representation of nonnegative functionals on , Fubini and integration by parts for Stieltjes measures, and the measure of a left-continuous monotone function. These pieces are reusable beyond this mission. Contributions to any milestone are welcome. The extensions to several dominance constraints and to higher-order dominance are not included.
In online convex optimization a decision maker picks points in a convex set , and after each choice pays for a convex cost function chosen in advance by an adversary. Performance is measured by regret: the total cost paid minus the cost of the best fixed point in hindsight. Zinkevich (ICML 2003) showed that projected gradient descent has regret when the whole function , or at least its gradient at , is revealed after each round.
In many applications only the number is observed: a seller sets a price and sees revenue, a router picks a path and sees its delay, an advertiser places a bid and sees the cost. This is the bandit setting. Flaxman, Kalai and McMahan (arXiv:cs/0408007, SODA 2005) gave the first simple algorithm for bandit convex optimization against an oblivious adversary with general bounded convex costs: a randomized gradient descent that estimates the gradient from a single function value, with expected regret . The same one-point gradient estimate is the starting point of later work on bandit convex optimization and on zeroth-order (derivative-free) stochastic optimization; see, e.g., Bubeck and Cesa-Bianchi's survey (arXiv:1204.5721, Ch. 6) and Hazan's textbook (arXiv:1909.05207, Ch. 6).
Timeline. Zinkevich (2003): regret with full gradient feedback. Kleinberg (NIPS 2004), independently: bandit regret for Lipschitz costs by a different reduction. Flaxman, Kalai, McMahan (2004/2005): for bounded convex costs and for Lipschitz costs, with one function value per round. Later work (Bubeck, Lee, Eldan 2017 and others) reached with more complex algorithms.
Let and be the closed unit ball and the unit sphere, . The feasible set is closed and convex with
The costs are fixed before play (an oblivious adversary); each is convex on with for , where . For , is the nearest point of to .
The bandit gradient descent algorithm (Figure 1 of the paper) keeps an iterate with . At period it draws a unit vector uniformly from , independently of the past, plays
observes only , and updates
The smoothed cost is with uniform on . The expected regret after rounds is
For every , with , and ,
The paper prints the constant . Its own last step bounds the regret by with , , , and with the stated and this equals . The goal states the bound the proof establishes.
The tuning identity (p. 9): at , , for .
Theorem 2 (p. 9). If each is -Lipschitz on , then with , , , and large enough that ,
The theorem shows that bandit feedback costs only a polynomial factor in regret for arbitrary bounded convex costs, with an algorithm that is gradient descent plus one random perturbation per round. Lemma 1 is the general tool behind it: an unbiased estimate of the gradient of a smoothed function from one function value. It is reused across zeroth-order optimization, bandit learning and stochastic approximation. Lemma 2 is a self-contained regret bound for projected gradient descent with noisy gradients, the shape in which Zinkevich's analysis is most often applied.
The results are proved in the paper and are standard. To the platform's knowledge none of them has a machine-checked proof. Related statements from Bubeck and Cesa-Bianchi's survey, for differentiable Lipschitz losses, are open on the platform, and two earlier formalizations of the textbook versions were disproved because of missing regularity or independence hypotheses. Formalizing this mission produces a checked one-point gradient identity for continuous (not differentiable) functions on the sphere, a measure-theoretic regret bound for stochastic projected gradient descent, and the corrected constant of Theorem 1.
The bandit algorithm itself is simple; the difficulty sits in Lemma 1 and in the measure theory around it. The paper derives Lemma 1 from Stokes' theorem, , and the ratio of the volume to the surface area of a ball. Mathlib has neither this divergence identity on balls in nor the explicit link between its spherical measure and the surface integral needed here. The identity must hold for functions that are merely continuous near the ball, since convex costs need not be differentiable.
The obvious first idea, differentiating under the integral sign in , fails because is not differentiable. The second obvious idea, applying Lemma 1 to as given, fails at the boundary of , where is unconstrained. Lemma 2's conditional expectation requires that the direction be independent of the iterate , and the integrability and measurability of the played points come from continuity of convex functions in the interior of .
Points are EuclideanSpace ℝ (Fin d) with , and rounds are numbered . The costs are functions on , and no statement assumes anything about them outside : no global convexity, continuity, differentiability or Lipschitz bound. The standing model is part of the goal's hypotheses: is convex with , the costs are convex on with values in there, and . Additions and conventions:
uniformSphere d). Uniform marginals alone are not enough.IsBGDRun) required for every outcome. Projection uses the published predicate IsNearestPoint, and regret the published pseudoRegret, whose minimum is an infimum over the subtype; it is attained in every use here.A formalization that assumed integrability of the costs along the run, assumed differentiable or globally Lipschitz costs, dropped the independence of the directions, or stated through Mathlib's gradient (which is off differentiability) would trivialize or change the result. All of these are ruled out.
Needed infrastructure: the divergence identity for the ball average (Lemma 1), conditional expectation given for vector-valued variables, continuity of convex functions on the interior of a convex set, and nearest-point projection onto closed convex sets. The first two are reusable well beyond this mission. Contributions toward Lemma 1 in particular are welcome.
The multi-secretary problem is the simplest model of capacity allocation under uncertainty: a decision maker sees candidates one at a time and may hire at most of them, with every decision final. The same structure underlies single-resource revenue management (accepting or rejecting booking requests against a fixed inventory; see Talluri and van Ryzin, The Theory and Practice of Revenue Management, 2004), online knapsack and packing problems, and dynamic assortment of limited stock.
The performance of an online policy is measured against the offline benchmark, the value of the best candidates chosen with full hindsight. The gap between the two is the regret.
This mission formalizes that upper bound.
Abilities take values in a finite set of distinct positive reals, with probabilities , . Write for the mass strictly above , and
The abilities are independent with this distribution. Budget pairs range over the triangle .
For every there is a constant such that for every instance with and all , and
No constant is fixed. Only the shape is asserted: a bound uniform in , , the support size and the distribution, given .
The result. Bounded regret means that the loss from not knowing the future is a fixed number of candidates' worth of value, however long the horizon and however large the budget. The bound holds uniformly over all distributions with the same . It is attained by an explicit, adaptive, non-randomized rule that compares one ratio with fixed thresholds. The companion result of the same paper shows that every non-adaptive policy suffers regret of order in the interior regime. Together they quantify the value of adapting to the remaining budget. Lemma 1 of the paper shows the dependence on cannot be removed.
Formalizing it. The result is proved in the paper, but no part of it is machine-checked; there is no multi-secretary or bounded-regret development on the platform. The mission produces several pieces of machinery: a reusable finite model of sequential selection with online policies and the offline benchmark; an explicit online policy with its stopping-time analysis; and a binomial overshoot bound usable elsewhere. The constant is not made explicit in the paper. A formal proof would give one, and sharper constants are welcome.
The offline decomposition and the sufficient condition are bookkeeping with counts and one concentration bound. The hard step is Theorem 2: showing that the budget ratio stays within of its attracting threshold until a bounded expected number of periods before the end. Near the horizon a single selection moves the ratio by about , so the band becomes easy to leave. Equivalently, the target that the deviation process must exceed shrinks to zero. A standard martingale or drift argument with a fixed band therefore does not give a bound uniform in . The paper combines the mean-reverting drift of the deviation process with an exponential tail bound (its Proposition 4) and a Lyapunov argument. A second subtlety is uniformity: every constant must depend on (and ) only, never on , the , or .
The source is arXiv:1710.07719v2; its printed page numbers equal the PDF page numbers.
Representation.
Fin m, with index 0 the largest value ; Lean index is the paper's .Quantifiers. The constant in the goal is chosen after and before , the instance, and . A statement with chosen after the instance, or after , is trivial (regret ) and is excluded.
Corrections to the printed text, disclosed in the items.
Infrastructure. The model definitions (instance, offline value, online policies, counts, thresholds, action index) and the binomial overshoot lemma are reusable for other finite-support online selection and revenue-management results. All of the following are welcome:
Assortment optimization asks which set of products a firm should offer when customers choose among the offered products according to a discrete choice model; it underlies shelf-space planning in retail and fare-class control in airline revenue management (Talluri and van Ryzin, 2004). Under the nested logit model products are grouped into nests, and a customer first picks a nest and then a product inside it. Davis, Gallego and Topaloglu (Operations Research, 2014; DOI 10.1287/opre.2014.1256) map out how hard this problem is across variants of the model.
When every nest dissimilarity parameter is at most one and a customer who chose a nest always buys there, offering the top-revenue products of each nest is optimal (Theorem 4 of the paper, the subject of an earlier mission of this series). Once a customer may leave a nest without buying — a partially-captured nest — that structure breaks and the problem becomes NP-hard (Theorem 8). This mission targets the paper's response: a small, explicitly constructed family of candidate assortments per nest from which a linear program recovers a solution within a factor of two of optimal.
There are nests and, in each nest, products . Product of nest has a revenue and a preference weight , with . Nest has a dissimilarity parameter and a within-nest no-purchase weight ; is the weight of choosing no nest. For an assortment ,
and the expected revenue of is . The optimal expected revenue is the optimal value of the linear program
and problem (4) is the same program with the second family of constraints imposed only for a chosen collection of candidate assortments in each nest.
Throughout, for every nest and the are arbitrary. For a capacity , the knapsack value is the largest over assortments with (display (9)). Its continuous relaxation (11) allows fractional under the same capacity. The greedy solution of (11) fills the capacity with the products of weight at most in revenue order, each fully while it fits and the next one fractionally, and
Problem (10) replaces the per-assortment constraints of (3) by .
Let be an optimal solution of (4) with candidate collections . Then
Two further statements accompany the goal: the factor-two revenue guarantee obtained from Theorem 10 and Theorem 1 of the paper, and the fact that every is one of the at most assortments , the first products by revenue among the lightest.
Theorem 10 turns an NP-hard assortment problem into a linear program with variables and constraints whose solution is within a factor of two of optimal. The construction is explicit: the candidates are defined by a greedy rule, not by an optimization oracle. The same template, a restricted linear program whose doubled optimum is feasible for the full one, is reused in §6 of the paper for the most general instances, and Lemma 9's knapsack reformulation is the link to the classical approximation theory of knapsack problems (Williamson and Shmoys, 2011).
The theorem is proved in the paper. No machine-checked proof of it, of Lemma 9, or of greedy optimality for the continuous knapsack with an eligibility bound exists on the platform. Formalizing it yields a checked factor-two guarantee and a reusable fractional-knapsack development.
The obvious argument would compare the restricted program (4) with (3) constraint by constraint. That fails: (3) has one constraint per subset of products, and most subsets are not candidates. The comparison has to pass through the knapsack reformulation (10), which requires showing that a maximum over all subsets equals a maximum over a one-dimensional capacity parameter, using and in an essential way. The second obstacle is that the greedy assortment keeps only the fully taken products, so its value can fall short of the continuous knapsack value, and no single candidate assortment need attain the knapsack bound. With dissimilarity parameters above one the monotonicity behind the reformulation is lost, and §6 of the paper needs a different factor.
Products are Fin n (indices ), nests a finite type, and every quantity is real. Powers are Real.rpow; , which gives . An optimal solution of a linear program is a feasible pair whose is minimal among feasible pairs. The constraint "" of (10) is stated in constraint form, for every , so no real supremum is taken. is defined for only; its placeholder value for is never used. Ties in revenue (and, for , in weight) are broken by index. The candidate collection is taken over real ; adds nothing, since every capacity of at least already gives .
Standing assumptions and added hypotheses: for every nest (the section's assumption) on the goal and on every model milestone; the pins , , and the revenue ordering, shared by the series; on Lemma 9, on and on (28)/(29), the paper's nonempty ; and on the factor-two revenue guarantee, where Theorem 1 of the paper fails without it.
The greedy assortments are defined explicitly. Quantifying over arbitrary optimal solutions of (11) instead would change the candidate collection and is not the paper's theorem. The goal states feasibility for the full program (3) and does not mention knapsack values, the greedy solution or the case split. A formalization that weakens the conclusion to feasibility for (10), or that drops the singletons from the candidate collection, is not a solution.
Needed infrastructure: fractional knapsack optimality of the greedy rule with an eligibility bound, monotonicity of and for , and finite maximization over subsets. The fractional-knapsack lemmas are reusable beyond this mission. Proofs of any milestone, and alternative decompositions of the goal, are welcome.
An optimization model often needs a probability distribution for an uncertain cost or demand, while a practitioner has only a finite sample from that distribution. Replacing the distribution by the empirical one can hide uncertainty in its estimated mean and covariance. Delage and Ye use a finite-sample confidence region for these two moments to justify a distributional ambiguity set in data-driven stochastic programming Delage and Ye, 2010. The present mission concerns the confidence region itself: it asks how far the population moments can be from the sample estimates when the normalized random vector has bounded support.
The source for every theorem index and page number here is the authors' draft dated 20 February 2008, not an independently checked pagination of the published article. Its §4 starts from independent observations and Assumption 4, then obtains a sample-mean bound, a covariance bound around the known mean, and finally the joint bound for estimates computed entirely from the sample.
Let have distribution , mean , and covariance . Assume is positive definite. For independent observations , the empirical mean and empirical covariance in this section are
The divisor is , including for the covariance; the paper's earlier discussion of an unbiased estimator with divisor does not govern §4. When the true mean is known, write . Matrix order means is positive semidefinite. The squared Mahalanobis distance of a vector is .
Assumption 4 bounds the normalized observations: for some , with probability one. Equivalently, lies almost surely in a Euclidean ball of radius ; it has mean zero and covariance . The sample law is , the product measure of identical copies. These choices make the probability in each target an assertion about genuinely independent observations.
For , set
Theorem 2 is the goal. Write and , and assume . The target is the simultaneous event
with probability at least . The last denominator is a correction: printed (12c) says , while the authors' union-bound display on draft p. 13 says . The printed version fails, for example, for symmetric observations, whose sample covariance is and for which its claimed lower bound would require an implausibly large sample-mean square. The proof's displayed bound gives the stated draft pp. 13–14.
Lemma 2 bounds the normalized sample mean. Corollary 1 turns it into the Mahalanobis bound for . Lemma 3 gives a two-sided matrix bound for ; Corollary 2 transfers that bound to . A separate theorem item states the centring identity . The final milestone is the rank-one matrix inequality used in Theorem 2's proof. Their statements follow the draft's §4.1–4.2.
The joint region places both true moments inside explicit data-dependent matrix inequalities at a chosen confidence level. That is the statistical input for the paper's later moment-based distributional uncertainty sets. The result is known in the source; this mission asks for machine-checked proofs of its corrected statement and its supporting concentration and matrix results. The Lean items are currently open theorem statements, so a successful draft compilation does not constitute formal verification of the inequalities.
Related platform results include a proved two-sided constant-bound McDiarmid inequality (UnderstandingML.mcdiarmid_inequality_pi) and an open per-coordinate upper-tail version (StabGen.Uniform.mcdiarmid_inequality). Neither is identical to the cited Theorem 1 of this draft, so the milestone list starts with the paper's Lemma 2 and does not restate Theorem 1.
The known-mean covariance estimate is a sum of outer products of normalized observations. Controlling its largest and smallest eigenvalues together requires concentration of a matrix-valued statistic, rather than a separate scalar bound for each entry. Once the true mean is replaced by , the covariance changes by a rank-one matrix; the mean bound must control that correction in Loewner order. A direct replacement of by therefore does not preserve both sides of Corollary 2 automatically.
Vectors are Fin m → ℝ, and matrices are real Fin m × Fin m matrices. The Euclidean squared length is a dot product; Lean's generic norm on functions is a supremum norm and is not used for it. The Loewner order is (B - A).PosSemidef. The distribution has a probability measure and coordinatewise finite moments, so its real-valued mean and covariance integrals are well defined. The true covariance is positive definite, reflecting the section's nonsingularity assumption. Samples have the product law . The chapter's normalized case records zero mean, identity covariance, and the almost-sure ball bound.
Every statistical result assumes ; the logarithms and confidence levels are then in their intended domain. Positive rules out division by zero in empirical averages. Lemma 3 carries the paper's explicit sample-size threshold, and the goal reads “ large enough” as , which keeps the upper covariance denominator positive. The expression under the other square root is nonnegative in every satisfiable positive-dimensional normalized setting, because . It is not an added assumption. The probability conclusions use , which is what the paper's proofs show despite the phrase “greater than.”
The goal assumes the source's distributional and support conditions, not the probability conclusions of its supporting corollaries. This prevents a vacuous route that merely postulates the desired confidence event. A complete proof will need reusable product-measure concentration facts, moment and matrix algebra, and a positive-definite quadratic-form bridge. Contributions to those components and to each milestone are in scope. Corollary 3's data-derived radius is excluded because the draft's conditioning argument does not establish its claimed confidence level. Corollary 4 as a probability statement, Theorem 3, and Corollary 5 depend on it; Remark 2 concerns a separate Gaussian eigenvalue density.
A retailer that sells products in several categories, channels or stores has to decide which products to offer in each. Customers substitute: a product left out of the assortment sends some of its demand to other products, and some of it away. The nested logit model (McFadden 1974, 1981) is the standard choice model for this situation. It groups products into nests, so that substitution within a nest differs from substitution across nests. Assortment optimization under this model asks which products to offer in each nest so as to maximize expected revenue.
Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) split the problem into four cases: dissimilarity parameters at most one or unrestricted, and nests that are fully or only partially captured. The problem is polynomially solvable in the first case and NP-hard in the other three. Every approximation guarantee in the paper for the hard cases (Theorems 7, 10, 11, 12) comes from one general framework, set up in §2: a linear program equivalent to the assortment problem, and Theorem 1, which turns a feasibility certificate for that linear program into a performance guarantee. This mission formalizes that framework.
There are nests and products in each nest. Product of nest has revenue and preference weight , and the products in each nest are ordered so that . Nest has a no-purchase weight and a dissimilarity parameter . The weight of choosing no nest at all is . If the assortment is offered in nest , write
A customer picks nest with probability , and then a product of that nest by the multinomial logit model. The expected revenue is
and problem (2) is .
The linear program (3) in the variables minimizes subject to
Given candidate collections of assortments for each nest, the linear program (4) is (3) with the second family of constraints imposed only for in the collection of nest .
Let be an optimal solution of (4), and let solve , problem (5), in every nest. If is feasible for (3) for some , then, with ,
The theorem fixes no candidate collection and no value of . Each later section of the paper instantiates it with its own collection and its own factor, so a formal proof applies to all of them.
Theorem 1 is the common step behind the paper's four approximation guarantees: the factor or of Theorem 7, the factor 2 of Theorem 10, the factor of Theorem 11, and the of Theorem 12. Each of these reduces to checking that a scaled optimum of a small linear program is feasible for (3). With Theorem 1 formalized, those guarantees reduce to inequalities about candidate collections, which are the subject of the sister missions of this series. The upper bound (16) and Proposition 13 give the instance-specific bound that the paper uses to assess its assortments numerically.
The results are proved in the paper. To our knowledge none of them has a machine-checked proof. The formal work adds two things: the statements below are made exact at the degenerate inputs the prose passes over (an empty assortment, ), and a formal proof certifies the framework once for every later instantiation.
The equivalence of (2) and (3) rests on decomposing a maximum over joint assortments into a sum of per-nest maxima, and on reading the fractional objective as a linear constraint. Both steps need care where a denominator can vanish. The binding argument for (4) is a perturbation argument: lowering must keep every constraint satisfiable, which needs a continuity and monotonicity property of the right-hand side in . The obvious one-line reading of Theorem 1, " and ", is correct only once both of these facts are established with their hypotheses. In particular, it is false when (see below). Proposition 13 requires that the supremum over the box be finite, which comes from the boundedness of on .
Nests are a finite type ι and products are Fin n, indexed . An assortment is a finite set of products per nest, and a candidate collection is a set of such finite sets. Powers are real powers, and Lean's gives . is for an arbitrary optimal assortment ; no supremum over assortments is taken. "Optimal solution of (4)" means feasible with minimal , and " solves (5)" means belongs to the collection of nest and maximizes the objective of (5) over it at .
Standing assumptions and pins. These are and ordered revenues, together with , and . The paper allows zero-weight padding products and , but its own conventions fail there. Theorem 1 and the binding milestone add . The page allows , but then Theorem 1 is false: take one nest with , , and candidates . Then and meet every hypothesis with , yet . The equivalence of (2) and (3) and the bound from (16) keep , as the page does, and assume at least one nest and one product: with neither and , every is feasible for (3).
A formalization that assumes the binding equality, the identity , or the inequality in the goal would trivialize it. Those facts appear only as milestones. Likewise, reading "optimal solution of (4)" as mere feasibility would make the goal false rather than easier.
The development needs only finite sums, real powers and elementary order reasoning. Proposition 13 also needs the boundedness of a continuous function on a box and the convexity of a pointwise supremum of affine functions. Welcome contributions include proofs of the milestones, the goal from them, and reusable lemmas on the per-nest decomposition of maxima, which the sister missions of this series use as well.
Many control problems in queueing, inventory and communication systems run indefinitely, and the quantity of interest is the long-run cost per unit time rather than a discounted total. The average cost criterion is harder to analyse than the discounted one: the discounted dynamic programming operator is a contraction, while the average cost problem has no contraction, and on an infinite state space its behaviour depends on the recurrence structure of the controlled chain. The survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993)) organises the theory around the average cost optimality equation (ACOE) and the conditions under which it has a solution.
Timeline (as recorded in the survey's §3 and §5). Derman studied the ACOE and characterized optimal stationary policies by its solutions (Derman, On sequential decisions and Markov chains, Management Sci. 1962; Denumerable state Markovian decision processes — average cost criterion, Ann. Math. Statist. 1966). Taylor introduced a vanishing discount argument for a replacement problem (Ann. Math. Statist. 1965). Ross extended it to general countable models, showing that uniformly bounded differential discounted value functions yield a bounded solution of the ACOE (Ann. Math. Statist. 1968, two papers; Introduction to Stochastic Dynamic Programming, 1983). Sennott replaced the uniform bound by one-sided bounds and obtained the average cost optimality inequality (Oper. Res. 1989). The survey presents Ross's result as Theorem 5.2, following the 1983 book; this mission formalizes it.
A controlled Markov process on the countable state space consists of a metric space of actions; for each state a nonempty compact set of admissible actions; a cost ; and transition probabilities . For fixed , the maps and are continuous on .
An admissible policy chooses, at each time , a probability distribution on that may depend on the whole past . The class of all of them is , and is the class of stationary deterministic policies, maps with . Each initial state and policy define a law of the trajectory, with expectation . For a discount factor ,
and , . The differential discounted value function is . A pair , , , solves the ACOE if
In the Lean development these objects are CMP, Policy, StationaryPolicy, pathMeasure, discCost, avgCost, discValue (), optAvg (), hRel () and ACOE.
Assume for all and , and that there is with for all such and . Then there are , a bounded and a sequence , , with
The goal does not assert that is the optimal average cost; that follows from Theorem 5.1 and Remark 5.1(a), which are milestones.
Theorem 5.2 is the template of the vanishing discount method. Under its hypothesis the average cost problem has a bounded solution of the ACOE, so (through Theorem 5.1) the optimal average cost is a constant independent of the initial state, it is attained by a stationary deterministic policy, and it is the Abelian limit of the scaled discounted values. Recurrence conditions on the controlled chain, such as uniformly bounded mean return times to a fixed state (Theorem 5.3 of the survey), are verified by checking the hypothesis of Theorem 5.2; the later results of §5 refine its conclusion under weaker hypotheses.
The theorem itself is classical. What this mission adds is a machine-checked statement and, eventually, proof, on a model with history-dependent randomized policies, compact action sets and unbounded costs, together with the supporting verification theorem (Theorem 5.1) and the discounted optimality equation. To our knowledge none of these results has been formalized in Lean; Mathlib has the Ionescu-Tulcea construction of the path measure but no controlled Markov processes.
The obvious argument fixes a sequence , extracts a pointwise convergent subsequence of the bounded functions and of the bounded numbers , and passes to the limit in (5.6). Two steps resist this. First, the limit of a minimum over is not in general the minimum of the limits: the convergence of must be shown to be uniform on the compact set , which requires more than pointwise continuity of each . Second, the subsequential limit could depend on the subsequence, so part (iii), a limit along all , needs an independent identification of , here as the optimal average cost through Theorem 5.1, which in turn needs the comparison with arbitrary history-dependent policies. The discounted optimality equation behind (5.6) also has to be established for unbounded costs, where is not the unique fixed point of .
The state space is ℕ; state 0 is the reference state of . Policies are history-dependent randomized stochastic kernels with the admissibility constraint , and , are infima over all of them. Costs are lower Lebesgue integrals with values in , built from Mathlib's Kernel.trajMeasure. The following choices make implicit hypotheses explicit:
ℕ these are the lower semicontinuous functions bounded below), with convergent series.A formalization in which is an infimum over stationary policies only, in which the ACOE is an inequality or holds for one fixed action, or in which is computed from values through a junk conversion, would trivialize the goal; all three are excluded by the definitions above.
A complete development needs the Ionescu-Tulcea path measure for history-dependent policies, the discounted optimality equation for nonnegative unbounded costs, Scheffé-type uniform convergence on compact action sets, and the martingale identity behind Theorem 5.1. The model file is reusable by the other missions of this series and by any countable-state average cost result; proofs of the milestones are welcome independently of the goal.
A retailer choosing which products to display, or an airline choosing which fare classes to open, solves an assortment optimization problem: pick the set of offered products that maximizes expected revenue when customers choose among what is offered according to a discrete choice model. Under the multinomial logit model the answer has a simple form: an optimal assortment consists of the few highest-revenue products (Talluri and van Ryzin, 2004). The multinomial logit model, however, forces every pair of products to compete in the same way. The nested logit model relaxes this by grouping products into nests (brands, store sections, departure times) and letting a customer first choose a nest and then a product inside it.
Davis, Gallego and Topaloglu (Operations Research, 2014; DOI 10.1287/opre.2014.1256) study how much of the multinomial logit structure survives under the nested logit model. Their first answer is the theorem this mission targets: when the nest dissimilarity parameters are at most one and no customer who chose a nest leaves it without buying, offering the top products of each nest is still optimal. The other missions of this series treat the cases where this fails: dissimilarity parameters above one (the problem becomes NP-hard) and nests with their own no-purchase option.
There are nests and, in each nest, products . Product of nest has a revenue and a preference weight ; products are ordered so that . Nest carries a dissimilarity parameter and a within-nest no-purchase weight , and is the weight of choosing no nest at all.
An assortment is a tuple of subsets . Write
A customer picks nest with probability and then, inside the nest, product with probability . The expected revenue is
and problem (2) asks for over all assortments. The nested-by-revenue assortment collects the highest-revenue products of nest , with and .
This mission works under the standing assumptions of §3 of the paper: competitive products, , and fully-captured nests, , for every nest .
If and for all , there exists an optimal solution of problem (2) such that
A companion item (not a milestone) states the algorithmic consequence at the end of §3: solving the linear program (4) over the candidates and choosing in each nest a maximizer of problem (5) gives an optimal solution of (2).
Theorem 4 reduces problem (2), a search over assortments, to nested-by-revenue combinations, and the paper then finds the best one with a linear program with variables and constraints. It marks the exact boundary of the classical multinomial logit structure inside the nested logit model: the paper's §4 shows that a single nest with already breaks it, and that the general problem is NP-hard. The structural statement is also the base case for the approximation guarantees of §§5–6, which compare against nested-by-revenue assortments.
The theorem is proved in the paper; to our knowledge it has no machine-checked proof. A formal proof would supply a verified reduction from a combinatorial revenue maximization over the nested logit model to a polynomial-size search, with every boundary case (empty nests, , ties in revenues) handled explicitly.
The obvious argument copies the multinomial logit proof: take an optimal assortment and swap a low-revenue product for a missing higher-revenue one. Under the nested logit model this exchange changes the nest's attraction non-linearly, so the revenue of the modified assortment is not an affine function of the change, and a simple swap can lower the expected revenue. The argument must instead control how adding or removing one product moves the nest weight relative to the nest revenue, and this is exactly where enters, through two scalar inequalities in the ratio of nest weights. With these inequalities fail and so does the theorem.
A second subtlety is ties: several optimal assortments may exist, and only some of them are nested by revenue. The statement asserts existence, not that every optimum has this form.
All statements live in the namespace NestedLogitVariants.Competitive and share one definition file. Nests form a finite type ι with decidable equality; products are Fin n, indexed , so is nbr n j with , and gives . Powers are Real.rpow, and , which gives . Optimality of an assortment means its revenue is at least that of every assortment.
Standing assumptions carried as hypotheses: , , revenues ordered within each nest, and §3's and . Three pins are disclosed: (the paper allows zero-weight padding products, under which Proposition 2 fails), , and (the paper's ; its convention fails at ). The section's "without loss of generality " is a hypothesis of Proposition 2, Lemma 3, the threshold, the exchange step and the LP item; the goal itself only assumes , and the case is milestone 1. The two scalar inequalities are stated as inequalities, not as monotonicity claims.
The goal is not trivialized by any hypothesis: it assumes none of the milestones, and stating "some nested-by-revenue assortment exists" (always true) or "every optimal assortment is nested by revenue" (false under ties) would be a different theorem.
Needed infrastructure is light: finite sums, real powers, and concavity of for . The scalar lemmas are reusable for other nested logit results. Proofs of any milestone are welcome independently.