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 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.
In a stochastic multi-armed bandit a player repeatedly chooses one of distributions ("arms") and observes a reward drawn from it; the goal is to collect as much reward as possible, which amounts to pulling suboptimal arms as rarely as possible. Lai and Robbins (1985) showed that any reasonable strategy must pull a suboptimal arm at least times up to horizon , where is a Kullback–Leibler divergence between arm and the best arm, and Burnetas and Katehakis (1996) extended the bound to general models. Strategies matching this rate are called asymptotically optimal.
The popular UCB algorithms of Auer, Cesa-Bianchi and Fischer (2002) use Hoeffding-type confidence bounds and are not asymptotically optimal outside special cases. Cappé, Garivier, Maillard, Munos and Stoltz (Ann. Statist. 41(3), 2013; arXiv:1210.1136) analyse kl-UCB, which replaces the Hoeffding radius by a Kullback–Leibler confidence region, and prove a finite-horizon bound whose leading term is exactly the Lai–Robbins constant. This mission formalizes that result for one-parameter exponential families (Theorem 1), the main-text steps of its proof skeleton, and its two corollaries for bounded rewards.
Timeline: Lai and Robbins (1985) lower bound and asymptotically optimal index policies; Agrawal (1995) sample-mean based index policies; Auer, Cesa-Bianchi and Fischer (2002) finite-time analysis of UCB1; Garivier and Cappé (2011) kl-UCB for bounded rewards; Cappé et al. (2013) the unified analysis formalized here.
A canonical exponential family is given by a dominating measure on and a function , with densities . The parameter set is the natural parameter space , assumed to be an open interval (the family is regular), and is twice differentiable. The mean of is , an increasing function, so is determined by its mean in the open interval . The divergence (11) is
extended by continuity to the closure , possibly with the value .
There are arms with laws and means ; . At each round the player picks an arm based on the past and receives a reward drawn from . is the number of pulls of arm in rounds , and the mean of the rewards obtained from arm so far.
kl-UCB (Algorithm 2) with a nondecreasing exploration function pulls each arm once and then, for , pulls an arm maximizing the index
With for and , for every suboptimal arm and every horizon ,
where and is the derivative in the first argument.
Corollary 1 (p. 17, kl-UCB with the Bernoulli divergence for arbitrary rewards in ) and Corollary 2 (p. 18, UCB with radius ), stated as separate theorems.
Theorem 1 shows that kl-UCB is asymptotically optimal in every regular one-parameter exponential family (Bernoulli, Poisson, Gaussian with known variance, exponential, Gamma with known shape), and it does so with an explicit bound valid at every horizon, not only in the limit. Corollary 2 improves the constants of the classical UCB1 analysis, and Corollary 1 shows that the Bernoulli kl-UCB index is uniformly better than UCB for all bounded rewards.
The result is proved in the paper; its proofs are in the supplemental article (DOI 10.1214/13-AOS1119SUPP, Appendix A), not in the main text. No machine-checked version exists. The platform has a formal analysis of a Bernoulli KL-UCB variant with another exploration function (Lattimore–Szepesvári's Theorem 10.6), which is a different statement. The formalization adds the general exponential-family index, the random-sample-size deviation bound (13) and the full finite-time constant.
The obvious argument bounds by a union bound over the possible values of , which costs a factor and destroys the logarithmic rate. The deviation bound (13) has to control an empirical mean whose number of summands is chosen by the algorithm itself, losing only a factor over the fixed-sample Chernoff bound; this is the step that needs the strategy to be non-anticipating. The second-order terms depend on the curvature of between and , measured by and , and the explicit constants must be tracked through every step. The empirical mean can be an endpoint of (Bernoulli rewards at small sample sizes), where is only defined as a limit.
The rewards are a stack (the -st reward of arm ), mutually independent and i.i.d. per arm, the representation of §2.2; this is the platform's RegretBandits.Stochastic.IsStochasticBandit, and the law of is pinned to . Arms are Fin K. The exponential family is the platform's OptimalBAI.OptProportions.ExpFamily (with , i.e. strict convexity, which the page derives); the natural-parameter-space condition is a separate hypothesis. A run of kl-UCB is a pathwise predicate: rounds pull every arm once and later rounds pull an argmax of the index, ties broken by any rule. The arm choices are measurable and non-anticipating (a measurable function of the arms and rewards already observed). The index (12) is a real supremum over a set containing the empirical mean, so it is never a junk value, and the divergence at an empirical mean on the boundary of is computed in . Statement (13) is made for : at its printed right-hand side is .
A trivializing formalization is ruled out: the run predicate forces both initialization and argmax, the index sets are nonempty and bounded, the reward stack is independent under the probability measure, and the Bernoulli divergence is never evaluated at or .
A complete development needs exponential-family calculus (convex conjugate of , continuity of up to the boundary), Chernoff bounds for exponential families, a peeling/maximal inequality for random sample sizes, and the counting arguments of §3.1. The deviation bound and the counting arguments are reusable for every index policy on the platform.
Sparse graphs with small nontrivial eigenvalues, expanders, are basic objects in combinatorics and theoretical computer science. They are used in error-correcting codes, derandomization, sorting networks, and the analysis of random walks. The Alon–Boppana bound says that a -regular graph on vertices has a nontrivial eigenvalue of absolute value at least (Alon 1986; Nilli 1991). Graphs that reach are Ramanujan graphs.
The classical explicit Ramanujan graphs of Lubotzky, Phillips and Sarnak (1988) and Margulis exist only for degrees with prime, and only for very sparse sequences of vertex counts. Constructions with for every degree came from Mohanty, O'Donnell and Paredes (STOC 2020, arXiv:1909.06988), but their graphs also do not have every number of vertices. Alon (arXiv:2003.11673, Combinatorica 41, 2021) asked for near-Ramanujan graphs of every degree and every large size. Theorem 1.3 of that paper answers this up to : for every , every and every large with even there is an explicit -graph with .
A -graph is a -regular simple graph on vertices in which every nontrivial eigenvalue of the adjacency matrix has absolute value at most . The trivial eigenvalue is , with the constant eigenvector . Equivalently, every eigenvalue of with an eigenvector , , satisfies .
Distances are graph distances, and they are between components. The -neighbourhood of a vertex is . The -neighbourhood of an edge is , and is the set of vertices at distance exactly from . A set contains no cycle if the subgraph induced on it is a forest. A ball contains at most one cycle if its induced subgraph has at most as many edges as vertices.
The construction starts from a -regular graph on a vertex set and a set . Write for the set of neighbours of , and let be a perfect matching on . Then is the subgraph induced on , is the graph of matching edges , and .
Let , , . Suppose is an -graph in which the -neighbourhood of every vertex contains at most one cycle, and . Then for every with even and ,
The hypotheses on are what Theorem 3.3 (Mohanty–O'Donnell–Paredes) supplies, and that theorem is not formalized.
Theorem 1.3 shows that the size restrictions of algebraic Ramanujan constructions cost nothing spectrally: up to an arbitrarily small , the Alon–Boppana bound is attained by explicit graphs on every admissible vertex count. The deletion method is local. It turns any near-Ramanujan graph whose short cycles are sparse into graphs of all nearby sizes, so it applies to future constructions as well. Lemma 3.2 is a self-contained delocalization statement in the tradition of Kahale 1995: eigenvectors of eigenvalues at least in absolute value cannot concentrate near tree-like edges.
The result is proved on paper. To our knowledge none of it is formalized; Mathlib has adjacency matrices, extended graph distance and acyclicity, but no theory of expanders. A complete development would give machine-checked versions of a delocalization lemma, of the greedy selection of far-apart vertices away from short cycles, and of the variational eigenvalue bound for induced subgraphs. It would also check two points the paper passes over. The proof of Theorem 1.3 treats only positive eigenvalues . And its claim that the -neighbourhood of a matching edge is cycle-free fails when two deleted vertices are at distance exactly . This mission states the corrected forms (see Formalization scope).
The spectral bound for does not follow from interlacing alone. Deleting vertices is harmless, since by (9) the quadratic form of is controlled by . But the added matching contributes up to to , which can be as large as for an eigenvector concentrated on . The obvious estimate therefore gives only . Closing the gap requires showing that an eigenvector of a large eigenvalue spreads its mass over the layers around each matching edge (Lemma 3.2). That in turn needs those neighbourhoods to be trees in and pairwise disjoint, which is where Lemma 3.1's choice of is used. The combinatorial part, tracking distances and cycles in when mixes edges of with matching edges, is the main formalization burden.
SimpleGraphs with real adjacency matrices adjMatrix ℝ. The (n, d, λ) predicate requires IsRegularOfDegree d, symmetry, row sums , and for every eigenpair with , . Distances use the extended SimpleGraph.edist, never dist (which is across components). Cycle conditions are on induced subgraphs, and "at most one cycle" on a ball is . Deleted vertices are a Finset U; the new graph lives on the subtype {v // v ∉ U}. The matching is a fixed-point-free involution of .Many problems in machine learning and statistics are regularized empirical risk minimization: minimize an average of loss terms, one per data point, plus a regularizer such as . When is large, a full gradient costs component gradients, so stochastic gradient methods that touch one per step are preferred. Variance-reduced methods (SVRG, SAGA) correct the stochastic gradient with a periodically recomputed full gradient and reach the rates of full-gradient descent at the cost of stochastic steps; accelerated full-gradient methods (Nesterov) improve the rate from to on convex problems.
Combining the two directly was open until Allen-Zhu's Katyusha (arXiv:1603.05953, STOC 2017, JMLR 2018). Before it, accelerated stochastic rates were obtained either for special structure (accelerated coordinate and dual methods, which need strong convexity or dual access) or through reductions such as Catalyst and APPA, which wrap a non-accelerated method in an outer proximal-point loop and lose logarithmic factors. Katyusha adds a third momentum term, the Katyusha momentum, that pulls each iterate back to the snapshot point, and obtains the accelerated rate directly. This mission concerns the paper's second main result: the variant Katyusha (Algorithm 2) for objectives that are convex but not strongly convex.
Problem (1.1) of the paper is
where , each component is convex and -smooth, , and the regularizer is convex. A point minimizes .
Katyusha runs epochs of iterations each (the paper takes ). It keeps three sequences , and a snapshot , all starting at , and fixes . Epoch uses the weight and the step , computes once, and performs, for :
At the end of the epoch the new snapshot is the average . The output is . Throughout, and .
The paper states ; the explicit form above is what its proof in Appendix C.1 establishes.
Theorem 4.1 gives the accelerated rate for non-strongly convex composite finite sums with a direct method: error after stochastic gradient evaluations, a factor better than the of non-accelerated variance-reduced methods such as SAGA (Remark 4.2). The non-strongly convex case covers -regularized and unregularized convex losses, where no strong-convexity parameter is available to tune a linear-rate method.
The result is proved in the paper; no machine-checked proof of Katyusha or Katyusha is known to exist. The mission produces a formal statement of the algorithm and its rate with explicit constants, and a formal chain of the paper's intermediate inequalities. A SAGA mission on this platform states SAGA's non-accelerated rate for the same problem class, so the two results become directly comparable in Lean.
Each step uses only convexity, smoothness and the optimality of proximal points, but the steps interlock. The variance of cannot be bounded by as in SVRG's analysis without losing acceleration; the paper's bound (Lemma 2.4) leaves a linear term that is cancelled only by the specific weight of the Katyusha momentum (Lemmas 2.6–2.7). Without strong convexity the per-epoch inequalities do not contract, so the proof must telescope across epochs with epoch-dependent weights : the coefficients of produced by epoch must dominate those consumed by epoch , and the snapshot term must be charged to the previous epoch's iterates. Getting the boundary epoch (whose snapshot is ) and the last epoch right is where the constants come from.
The Lean development works on EuclideanSpace ℝ (Fin d) with components indexed by Fin n (). Gradients are given functions tied to by HasGradientAt; -smoothness is the Lipschitz bound on them with ; convexity is ConvexOn ℝ Set.univ. and are the published SAGA.Convex.fAvg and SAGA.Convex.gradAvg. The regularizer is real-valued and convex, so extended-valued regularizers such as indicator functions of constraint sets are not covered. The two arg-min steps are evaluated through a map assumed to return a proximal point of (the published SAGA.Convex.IsProxPoint) for every positive step; for real-valued convex such points exist and are unique, so the hypothesis is satisfiable. is assumed to minimize (without strong convexity a minimizer need not exist). Randomness is modelled by finite sequences of indices: the expectation is the uniform average over all index sequences (SAGA.Convex.expectIdx), with the indices split into epochs by Mathlib's finProdFinEquiv.
Conventions committed to:
A trivializing formalization is ruled out: the prox map, the gradients and are all tied to , and by hypotheses that a quadratic instance satisfies, and the expectation averages over every index sequence rather than a chosen one. The iteration count stated "in other words" after Theorem 4.1 is not a target.
Contributions welcome: proofs of the milestones in any order; general lemmas about proximal points of convex functions (the three-point inequality behind Lemma 2.5) and the co-coercivity of convex -smooth functions (behind Lemma 2.4) are reusable beyond this mission.
A graph is perfect if every induced subgraph has chromatic number equal to its clique number. Berge conjectured in 1961 that a graph is perfect exactly when it contains no odd hole and no odd antihole. Chudnovsky, Robertson, Seymour and Thomas proved this strong perfect graph theorem in 2006 (Ann. of Math. 164 (2006), 51–229). Perfect graphs matter beyond graph theory: for them the stable set polytope is described by clique inequalities, so maximum weight stable set and colouring problems become polynomially solvable linear programs (Grötschel, Lovász and Schrijver).
The proof reduces the theorem to a decomposition statement (1.3 of the paper): every Berge graph is basic or admits one of a few decompositions. That statement is in turn proved in twelve steps, listed as 1.8.1–1.8.12. Each step excludes one kind of configuration from a Berge graph without the decompositions. This mission is step 1.8.5, restated as 13.4: it deals with Berge graphs that contain a long odd prism but no appearance of . It is the only step of the proof that needs proper 2-joins in the complement and proper homogeneous pairs.
All graphs are finite and simple; is the complement of . A path is an induced subgraph which is a path, and its length is its number of edges. An antipath is a path of . A hole is an induced cycle of length at least , and an antihole is the complement of a hole of . is Berge if every hole and antihole of has even length.
A prism consists of two disjoint triangles , and three paths from to , such that the only edges between different paths are the triangle edges. It is long if some has length , even if all three lengths are even, and odd otherwise.
A subdivision of a graph replaces every edge of by a track, these tracks being disjoint except at their ends. appears in if is isomorphic to an induced subgraph of for some bipartite subdivision of , where is the line graph.
The decompositions in the conclusion (pp. 53–54):
The intermediate objects come from Sections 11–13 of the paper:
Let be Berge with no appearance of in or in , and suppose contains a long odd prism as an induced subgraph. Then
In the order of the paper's argument:
13.4 removes long prisms from the analysis. Combined with 10.6 (the even prism), it shows that a recalcitrant graph contains no long prism in or , which places it in the class (p. 154). The later steps (double diamonds, odd wheels, pseudowheels, wheels) all assume this. The step-connected strip and staircase method developed here is also the paper's model for growing a maximal structure and then classifying how the rest of the graph attaches to it.
The theorem has been proved since 2006; no machine-checked proof of it or of any of its steps is known. The proof of 13.4 also cites these results of the same paper, which are posed in other missions of this series:
The difficulty is the volume of case analysis behind every statement. The paper does not prove the exact analogue of the even-prism result 10.6. It warns (p. 127) that it does not know whether that analogue holds, and adds the two extra outcomes instead. The obvious first idea is to take a long odd prism and analyse attachments to it as in Section 10. The paper does not get the result that way (p. 127): it replaces two of the three paths by a maximal step-connected strip. Controlling how every remaining vertex or connected set attaches to such a strip is what the breaker results do. Maximality is also delicate. "Strongly maximal" refers to staircases of the complement, so and must be handled in one framework.
Graphs are SimpleGraph V on a Fintype vertex type with decidable equality. is Gᶜ.
G.induce X, so is connected. Anticonnectedness is the same notion in Gᶜ.Every hypothesis of the paper is kept. "No appearance of " is in and in for the goal, and in for the milestones. The goal also keeps "Berge", "no even prism" and "no 1-/2-breaker" where the page has them. 12.1's "exactly one" is an exclusive disjunction. 11.4 is a non-existence statement.
A formalization with non-induced paths, with the complement dropped from "one of ", or with a strip, staircase or breaker predicate that no graph satisfies would make the targets empty or false. The definitions here are checked against a concrete graph: the 8-vertex prism with path lengths is a long odd prism, and it carries a staircase. Contributions are welcome: proofs of the milestones, and reusable material on induced paths, holes and line graphs of subdivisions.
Two-stage adaptive optimization models decisions taken in two steps: a first-stage decision is fixed before an uncertain right-hand side is revealed, and a second-stage decision is chosen after it, as a function of . The objective protects against the worst in an uncertainty set . Computing an optimal fully adaptable solution is intractable in general (Feige, Jain, Mahdian and Mirrokni, IPCO 2007), so practitioners restrict the second stage to affine policies , introduced in robust optimization by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 2004). An optimal affine policy is computed by a single convex program, but its cost may exceed the adaptive optimum.
Bertsimas and Goyal (Math. Program. Ser. A, 2012) quantify this loss. Earlier, Bertsimas, Iancu and Parrilo (Math. Oper. Res. 2010) proved affine policies optimal for a class of one-dimensional multistage problems. The present paper shows that affine policies are optimal when is a simplex (Theorem 1), that they can lose a factor in general (Theorem 3), and — the subject of this mission — that when the first-stage constraint matrix is nonnegative they never lose more than (Theorem 4). Nonnegative first-stage matrices occur in network design, facility location, capacity planning and other covering problems.
Let , , , , and let be convex, compact and full-dimensional. The problem is
where the minimum is over first-stage vectors and arbitrary maps . The problem is assumed feasible. The value is the same minimum restricted to affine second stages , which must still satisfy on .
For each coordinate put and fix a maximizer with (display (38)). The scaled sum of over an index set is .
Algorithm (Fig. 1 of the paper) starts with and . While some has scaled sum over larger than , it picks a maximizer of that scaled sum, adds to the running vector on the coordinates of , and moves to every coordinate whose running value has reached . It returns the number of iterations , the vectors , their sum , and the partition .
In the -uncertain variant (60)–(63), only right-hand sides are uncertain and the remaining are fixed at ; all data are nonnegative. Its values are and .
If entrywise, then a feasible affine solution exists and
Theorem 4 is an upper bound on the price of restricting to affine policies, and Theorem 3 of the same paper shows it is tight up to a constant factor: for every there are instances with where the gap is . Together they settle the order of the approximation ratio of affine policies for covering-type two-stage problems. Theorem 5 refines the bound to when only of the right-hand sides are uncertain, which is the regime of many applications. The construction is also the template for the paper's Theorem 6, a -approximation for general obtained from a single dominating simplex.
The results are proved in the paper. To the knowledge of this mission, none of them has a machine-checked proof. Formalizing them produces a reusable model of two-stage adaptive linear programs with affine policies, a verified analysis of a greedy covering procedure (Algorithm ), and an explicit-constant version of an statement.
The obvious attempt scales the fully adaptable solution at the extreme points linearly in : . This is feasible at cost factor only when the scaled sums stay below on (condition (39)); in general they can reach , and the linear rule then costs a factor . The difficulty is to handle the coordinates where has large scaled mass. Algorithm isolates them, and the delicate point is the iteration count: each round must add scaled mass above , while the total scaled mass that can be absorbed before every coordinate leaves is at most . A formal proof must also track the algorithm's state through its recursion, because the argmax choices are not unique and the statements must hold for every run.
Vectors are Fin m → ℝ with the componentwise order, indices are 0-based, and matrices are Matrix (Fin m) (Fin n) ℝ. Nonnegativity of a matrix is stated entrywise. and are infima of the set of worst-case cost bounds achieved by feasible solutions; the goal and Theorem 5 assert the existence of a feasible affine solution, which rules out the trivializing reading in which is the infimum of an empty set (Lean's junk value ) and the inequality holds for free. The goal does not mention , or Algorithm ; these appear only in milestones.
and are given with their defining properties ( is the greatest value of on , and with ). Algorithm is encoded as a recursion on a choice sequence , with step 2(d) read as . A complete run requires the loop test and the argmax property at each iteration and the failure of the loop test at the end. The milestones on the constructed policy are stated for every feasible and every cost bound , so that no attainment of the optimum is assumed.
Standing assumptions of (1) carried by the goal: ; convex, compact, with nonempty interior; feasibility. Milestones drop the ones they do not use. Theorem 5 carries compactness and full-dimensionality of , which §5.1 does not repeat but its proof uses through Theorem 4. Lemma 11 assumes that is finite, since the paper's inequality is between extended reals.
A complete development needs: finite-dimensional linear programming facts (existence of optimal solutions is not needed), compactness arguments for the argmax in Algorithm , and manipulation of finite sums over Finset. The model of (1) and the analysis of Algorithm are reusable by the companion mission on Theorem 6. Contributions of proofs of any milestone, and of supporting lemmas about the recursion of Algorithm , are welcome.
Two-stage adaptive optimization models decisions made in two steps: a first-stage decision is fixed before an uncertain parameter is revealed, and a second-stage (recourse) decision may then depend on the realized value. In the robust version, the uncertain parameter ranges over an uncertainty set and the objective is the worst-case cost. Such models arise in capacity planning, network design and inventory problems with uncertain demand, where the demand is the right-hand side of the constraints.
Computing an optimal fully adaptable second-stage policy is intractable in general: the recourse is an arbitrary function of the uncertain parameter. The standard tractable surrogate, introduced by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 99, 2004), restricts the recourse to an affine policy , whose optimization is a finite convex program. Practitioners report that affine policies often perform well, which raises the question of when they are optimal and how much they can lose.
Bertsimas and Goyal (Math. Program. Ser. A, 2012) answer this for problems with an uncertain right-hand side. Their Theorem 1 shows that affine policies are optimal when the uncertainty set is a simplex, that is, the convex hull of affinely independent points of . Their Theorem 2, the subject of this mission, shows that this is almost tight: one additional extreme point can make the best affine policy almost twice as expensive as the optimum.
Let , , , and let be an uncertainty set. The problem is
Here is the first-stage decision and is the second-stage policy; all inequalities between vectors are componentwise. The value is the same minimum restricted to affine policies with and ; an affine policy must still satisfy for every . Always .
The instance of (6) is defined for and an even integer . It has , , , , and
where , is the -th unit vector for , has entries in its first coordinates and in the others, and has in its first coordinates and in the others. Thus is generated by nonzero points. The last two are also extreme points when ; for or they lie in the convex hull of .
For a permutation of , write . A set is permutation-invariant with respect to if (Definition 2), and is the set (10) of permutations with .
Together with Theorem 1 of the same paper, Theorem 2 delimits exactly where affine policies are optimal for right-hand-side uncertainty: for a simplex they are, and with one more nonzero extreme point the gap can approach . The ratio is measured against the fully adaptable optimum, which is the quantity a practitioner gives up by choosing affine recourse. Later sections of the paper push the same construction to for sets with polynomially many extreme points and prove a matching upper bound; Theorem 2 is the simplest member of this family and isolates the mechanism.
The result is proved in the paper; to our knowledge it has not been machine-checked. The mission produces a formal model of two-stage adaptive linear optimization with uncertain right-hand side, the values and , and a verified lower-bound instance. The symmetrization statement (Lemma 3) is an instance of a general principle, that a convex problem invariant under a group has an invariant optimum, which is reusable well beyond this paper.
The upper bound requires a feasible policy, which can be written down. The lower bound on is a statement about all affine policies, an dimensional family, and cannot be checked policy by policy. The obvious attempt, testing an arbitrary affine policy against a few extreme points, fails because an asymmetric policy can trade cost between coordinates. The argument needs an optimal policy that is symmetric, which in turn needs both the existence of an optimal affine solution (attainment of a minimum over a non-compact set of policies) and the invariance of the instance under the permutations of and the swap of the two halves. Without the attainment step, a contradiction for every policy of cost at most yields only , not the strict inequality.
Vectors are Fin m → ℝ with the componentwise order, matrices are Matrix (Fin m) (Fin n) ℝ, is B *ᵥ x and is d ⬝ᵥ y. Indices are 0-based: the paper's coordinate is index , so "" is (i : ℕ) < m / 2, with natural-number division (exact since is even). is x ∘ τ for τ : Equiv.Perm (Fin m).
and are the infima of the sets of real numbers for which some feasible (respectively feasible affine) solution satisfies for all . This epigraph form avoids a supremum of a possibly unbounded function; on an infeasible instance the infimum would be Lean's junk value , which is why Lemma 1 also asserts the existence of the feasible solution of cost . Optimal solutions are stated by IsOptimalAff: feasible, with worst-case cost bounded by every bound achieved by any feasible affine solution. Affine policies must be nonnegative on , as in (1).
The instance is concrete, so the standing assumptions of (1) (nonnegative costs, compact convex full-dimensional , feasibility) are properties of the data rather than hypotheses. The goal adds no hypothesis to the page: , even and . For the statement is easy but still true. The three Claims are stated for any feasible affine solution with constant intercept and worst-case cost at most , which is exactly what the paper's proof uses about the symmetric optimal solution under its contradiction hypothesis (12). Lemma 1 drops the unused hypothesis . Definition 2 prints ""; the formalization reads as the set .
Replacing by the cost of one particular affine policy, stating the goal with , or bounding only policies with constant intercept would not be Theorem 2, and is ruled out: the goal compares the two optimal values with a strict inequality.
A complete development needs convex hulls of finite point sets in Fin m → ℝ, the existence of a minimizer for the affine problem (a linear program in with infinitely many constraints indexed by , reducible to the extreme points), averaging of optimal solutions over a permutation group, and elementary estimates with . Contributions of general lemmas on attainment of semi-infinite linear programs and on symmetrization of convex programs are welcome.
Sparse graphs whose adjacency spectrum is concentrated near zero, expanders, are used throughout theoretical computer science: in error-correcting codes, derandomization, sorting and routing networks, and the construction of pseudorandom objects (Hoory, Linial and Wigderson, survey). The best possible spectral expansion for a -regular graph is governed by the Alon–Boppana bound , and graphs attaining it, Ramanujan graphs, were constructed explicitly by Lubotzky, Phillips and Sarnak (LPS 1988) and by Margulis. These constructions exist only for special degrees ( with prime) and special numbers of vertices (orders of or ). Applications often need a graph of a prescribed size .
N. Alon's paper Explicit expanders of every degree and size (arXiv:2003.11673v1; Combinatorica 41, 2021) shows how to obtain explicit near-Ramanujan graphs on exactly vertices. This mission formalizes the spectral core of its Theorem 1.2: a Ramanujan graph on vertices can be enlarged to vertices, with degree raised by one, while the nontrivial eigenvalues stay within a constant factor of optimal.
Let be a finite set of vertices. A -graph is a -regular graph on vertices whose adjacency matrix satisfies for every nontrivial eigenvalue , that is, every eigenvalue other than the top eigenvalue of the constant vector . For a symmetric with , the nontrivial eigenvalues are those with an eigenvector satisfying . Graphs may carry loops, at most one per vertex, and a loop adds one to the degree: it is a diagonal entry of .
Fix an integer and let be an -graph on , a -regular Ramanujan graph. Let be new vertices and let be pairwise disjoint sets of vertices each. Put and . The graph on is obtained from by joining each to every vertex of and adding one loop at each vertex of . Its adjacency matrix is
where is the adjacency matrix of (zero on ), that of the stars joining to , and the diagonal matrix of the loops. Every vertex of has degree .
The paper states for ; its proof gives , which is stronger, and the error term it produces is . The goal is parametrised by , and the sets , so it does not depend on how and are chosen.
With the Lubotzky–Phillips–Sarnak graph on vertices for the largest suitable prime with , and , the distribution of primes in arithmetic progressions gives , and the goal yields an explicit -graph with for every sufficiently large . This is within a factor of about of the Ramanujan bound , for every number of vertices, by an elementary modification of an existing graph. The statement is useful independently of LPS: any Ramanujan graph, or any graph with a bound on its nontrivial eigenvalues, can be padded to a nearby size in the same way.
The result is proved in the paper. No formalization of it, of the notion, or of the variational characterization of nontrivial eigenvalues for regular graphs exists on the platform. The mission produces a checked version of the spectral argument, and the variational characterization (milestone 1) is a general fact about symmetric matrices with constant row sums that applies to any spectral expander argument.
The vertices of and lie in the old graph , whose spectrum is controlled, but the new vertices of are not; and a vector orthogonal to on need not be orthogonal to the constant vector on . Bounding by applying the Ramanujan bound for to restricted to therefore fails: the restriction has a component along the trivial eigenvector of , whose eigenvalue is large. The argument must show that this component is small, of order , and must balance the star edges between and against the loops on so that every vertex class gets the same coefficient. The naive bound added to for and for gives a constant larger than ; the stated constant needs the weighted estimate.
On the Lean side, milestone 1 concerns the spectrum of a symmetric matrix on the invariant subspace , while Mathlib states the spectral theorem for the whole space.
SimpleGraph with adjMatrix.An -graph is a -regular graph on vertices in which every eigenvalue of the adjacency matrix other than the top eigenvalue has absolute value at most . Graphs of this kind with small compared with are expanders. They are used in derandomization, error-correcting codes, sorting networks and many other constructions in theoretical computer science. A Ramanujan graph achieves , which is asymptotically optimal.
The classical explicit Ramanujan graphs of Lubotzky, Phillips and Sarnak (LPS, 1988) exist only for special vertex counts, such as for a prime or the size of a quaternion group modulo . N. Alon, in Explicit expanders of every degree and size (arXiv:2003.11673, 2020; Combinatorica 41, 2021), asks for explicit -graphs with for every degree and every number of vertices . His Proposition 1.1 builds such graphs out of LPS graphs, and one ingredient is purely arithmetic. If the available vertex counts of an LPS family are dense enough, so that for every large one is within a factor of , then a few vertices can be added or removed while keeping the spectral bound.
This mission formalizes that ingredient, Lemma 2.2 of the paper (p. 7). It concerns the vertex counts of the LPS graphs for two fixed primes and all exponents . With fixed, the construction needs no large primes, which is why Proposition 1.1 is strongly explicit for every fixed degree.
Fix natural numbers . For natural numbers define the LPS vertex count
When are distinct primes congruent to modulo and , this is the number of vertices of the LPS Cayley graph (§2.3, p. 6). Lemma 2.2 itself only requires to be distinct primes. Both fractions are integers, because is a product of three consecutive integers.
The proof uses the real number , and the fractional part , written in the paper.
For distinct primes there is a function with such that for all sufficiently large there are integers with
Equivalently, the ratio between consecutive elements of tends to . The statement fixes no rate for , matching the paper's .
The result. Lemma 2.2 is the step of Proposition 1.1 that turns a family of Ramanujan graphs with sparse vertex counts into a family whose vertex counts approximate every large up to a factor . The deviation from can then be absorbed by the general packing argument of §2.1 of the paper. Without it, the construction would have to search for large primes depending on , and the result would be explicit but not strongly explicit.
The formalization. The lemma is proved in the paper, in one paragraph. To our knowledge no machine-checked proof exists, and the platform has no statement of it. The only related platform item is the irrationality of , the case , of milestone 1. Formalizing the lemma requires a quantitative inhomogeneous step that the paper leaves implicit ("implying the desired result"). Its last sentence also contains a misprint that the formalization corrects (see below). The Diophantine milestones 1–3 are reusable for any argument about the multiplicative density of , for instance the ratio of consecutive elements of .
Each milestone is short. The difficulty is in making the paper's last sentence ("implying the desired result") into a proof. Taking or large separately does not work: changing or by one multiplies by or , a fixed factor larger than , so the values obtained by varying one exponent leave gaps of a constant ratio. The bound must hold for every large , not just along a subsequence, and the exponents must stay positive throughout. Milestone 2 is the classical fact that the multiples of an irrational number are dense modulo . It needs a pigeonhole argument, not just the irrationality.
Real.log, and the fractional part is Int.fract.IsLittleO along atTop) and, eventually in , with . This is equivalent to the form "for every , every large has with ". The paper's proof yields the second form, with the factor for arbitrary .Int.fract and a pigeonhole or Dirichlet-approximation argument for milestone 2, and real exponentiation and asymptotics for the goal. Contributions of alternative proofs of milestone 2, for instance via Mathlib's Dirichlet approximation theorem, are welcome.Large-scale nonsmooth convex problems, such as minimising a Lipschitz convex function over a probability simplex with millions of coordinates, are routinely solved by first-order methods that use one subgradient per iteration. The classical projected subgradient method reaches accuracy after iterations, where and are measured in the Euclidean norm; on the simplex this hides a factor of order in the dimension. Nemirovski and Yudin's mirror descent algorithm (MDA) replaces the Euclidean geometry by one adapted to the feasible set and, on the simplex, reduces the dimension dependence to .
Beck and Teboulle (Oper. Res. Lett. 31 (2003) 167–175, doi:10.1016/S0167-6377(02)00231-6) showed that mirror descent is a projected subgradient method in which the squared Euclidean distance is replaced by a Bregman-type distance . This viewpoint gives a short convergence proof, and with the entropy as it yields a fully explicit method on the simplex, the entropic mirror descent algorithm (EMDA), the same multiplicative update that underlies exponentiated-gradient and Hedge-type algorithms in online learning.
Timeline. Nemirovski and Yudin (1983) introduce mirror descent with a rate on the simplex. Ben-Tal, Margalit and Nemirovski (SIAM J. Optim. 12 (2001)) analyse MDA with the potential , , whose conjugate requires a one-dimensional root-finding at each step. Beck and Teboulle (2003) derive MDA as a nonlinear projected subgradient method (SANP), prove its efficiency estimate for an arbitrary norm, and show that the entropy gives the same rate with a closed-form update.
Let be with an arbitrary norm , and the dual norm. The problem is under Assumption A: is closed and convex; is convex on and Lipschitz there, ; has a minimiser ; and a subgradient can be computed at every .
Let be strongly convex with parameter and differentiable. The distance-like function (3.10) is
The subgradient algorithm with nonlinear projections (SANP, (3.11)) starts from and sets, with step sizes ,
With this is the projected subgradient method.
On the unit simplex take the entropy (5.27), with . SANP becomes the entropic descent algorithm (EDA):
If is convex and -Lipschitz on for , with subgradients satisfying , and the EDA is started at with step for a horizon , then
For any norm, any -strongly convex and any SANP run,
and with the optimal constant step this gives .
The milestones follow the paper's proof: the three-point identity (Lemma 4.1), the optimality condition (4.16), the lower bound , the one-step inequality (4.21), Theorem 4.1(a), Proposition 4.1 (optimal step), Theorem 4.2 and its version with an upper bound on ; then for the simplex, the 1-strong convexity of for (Proposition 5.1(a), Remark 5.1), the bound (Proposition 5.1(c)), and the identification of the EDA with SANP.
The result shows that for nonsmooth convex minimisation over the simplex an explicit first-order method attains accuracy in iterations, with measured in the dual norm. The general estimate of Theorem 4.2 applies to any norm and any strongly convex potential, and is the template for later analyses of mirror descent, its stochastic and online variants, and mirror-prox methods.
Formalizing the paper produces a norm-agnostic, machine-checked proof of the mirror descent efficiency estimate, in which subgradients are dual-space objects and the dual norm is explicit, and a verified link between the entropy, the geometry and the multiplicative-weights update. To our knowledge none of these statements is formalized; existing formal developments of online mirror descent work in Euclidean space with Legendre potentials and bound regret for linear losses, which is a different statement.
The algebra of Theorem 4.1 is short, but it rests on facts that are not available off the shelf. The first-order optimality condition (4.16) must be derived for a minimiser over a convex set without assuming the set has interior (the simplex has none in ). The bound must be obtained from the chord definition of strong convexity for an arbitrary norm. On the simplex, strong convexity of the entropy with respect to is a form of Pinsker's inequality, and it must hold on the closed simplex, where the entropy is not differentiable at the boundary. Finally, the EDA must be shown to be the exact minimiser of the SANP subproblem over , which is a Gibbs variational principle. A tempting shortcut, working throughout in Euclidean space, fails: it changes the dual norm of the subgradients from to and the strong convexity constant of the entropy, and loses the rate.
Sections 3–4 live in a general real normed space; a subgradient is a continuous linear functional, is its value at , and is the operator norm. is the Fréchet derivative. Iterates are indexed from . A SANP run is a predicate on sequences: each step size is positive, each iterate lies in , is differentiable there, and the next iterate minimises the SANP objective. This encodes the paper's standing assumption that SANP is well defined, and replaces " has nonempty interior" and "". Section 5 works on as functions with explicit and sums; is the relative interior, and the entropy formula is evaluated on only. "" is stated as the existence of with .
Added hypotheses, each disclosed in the item: a bound on the oracle (used by the proofs of Theorems 4.1(b), 4.2 and 5.1, not implied by the Lipschitz condition for subgradients relative to ); in Proposition 4.1, without which the proposition as printed is false; in the step sizes. The step sizes of (4.23) and of the EDA are constant over a fixed horizon , which is what the proof chooses; Theorem 5.1 is stated with , since the free index in the printed bound (5.28) cannot be bound, and is what the proof yields.
Trivializing formalizations are ruled out: is never evaluated where fderiv is a junk value (the run requires differentiability at every iterate), the SANP step is never chosen by Classical.epsilon, the bound of Theorem 5.1 is not stated with a maximum of over the run, and the step is not an anytime schedule .
A complete development needs first-order optimality conditions over convex sets, strong convexity and Bregman distances in normed spaces, Pinsker-type inequalities for finite distributions, and the Gibbs variational principle. These are reusable beyond this mission; proofs of any milestone, and general lemmas that serve several of them, are welcome.