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?
Graham (1966) showed that list scheduling finds a schedule within a factor of optimal for precedence-constrained jobs on identical parallel machines, the first performance guarantee for an approximation algorithm. When the machines run at different speeds (uniformly related machines), the same analysis breaks down, and for two decades the problem resisted a guarantee independent of the speeds better than .
Timeline:
The mission formalizes the makespan half of that paper, up to its Theorem 3.7.
An instance has jobs and machines. Job requires units of processing, and machine runs at speed , so job takes time units on machine . A strict partial order on the jobs gives precedence constraints: means that job may not start until job has completed.
A schedule runs each job without interruption on one machine , from a start time to its completion time . A machine processes at most one job at a time, and forces . Its length is . is the length of an optimal schedule.
Let be the distinct speeds and the number of machines of speed . An assignment names the speed class at which job is to run. Its loads are , and its chain bound is the largest value of over chains of . Speed-based list scheduling is Graham's rule restricted by the assignment: whenever a machine of speed is idle, it starts the first available job on the list with .
The linear program LP has variables , and . It minimizes subject to the following constraints:
From a solution, with , the assignment algorithm gives each job the speed class of largest capacity .
There is an absolute constant such that for every instance with machines and distinct speeds, the better of the two schedules below has length at most
The result gives the first guarantee for , independent of the speeds, and a guarantee depending only on the number of distinct speeds. Through the batching technique of Shmoys, Wein and Williamson it extends to release dates (Corollary 3.8). Since LP also relaxes the preemptive problem, it gives an bound on the ratio between the nonpreemptive and preemptive optima (Corollaries 3.9, 3.10). The "In fact" form, relative to an arbitrary feasible LP solution, drives the paper's algorithm in §4.
The result is proved in the literature but, as far as is known, not formalized. A formal proof requires machine-checking the following:
Later work gave a combinatorial -approximation (Chekuri and Bender, 2001) and an -approximation (Li, 2017). These are not part of this mission.
Graham's argument has two lower bounds:
With different speeds, the first bound fails: a chain may have been run on slow machines, and its length then says nothing about . Forcing every job onto a fast machine repairs chains but can leave most machines idle, so the second bound fails. The paper only guarantees that all machines of one speed are busy at each moment of an idle period. Making this pay off requires an assignment that controls chain lengths and per-class loads simultaneously. That assignment is the delicate part: Theorem 2.1 is the bookkeeping, while Lemmas 3.2 and 3.4 rely on the LP. Two of the formal steps are routine on paper but fiddly in Lean: time-interval accounting over a continuous-time schedule, and the counting of rounded speed classes.
Fin n and machines Fin m with . and . is a strict partial order, and a chain is a finite set of pairwise comparable jobs. is the maximum completion time, or with no jobs.Proofs of any milestone are welcome. Reusable beyond this mission are the following: the model of nonpreemptive schedules on uniformly related machines with precedence, the speed-based list-scheduling predicate with Theorem 2.1, and the LP.
Prove that CLIQUE is NP-complete by reducing the existing 3-SAT language, KSat.KSAT 3, to it. An instance consists of a finite simple undirected graph and an input threshold; it asks whether the graph contains a clique of at least that size.
(https://prove2.me/theorems/d82e8682-c490-4742-a5e5-dd3a0b870b90). The construction specializes Karp’s SAT-to-CLIQUE reduction to 3-SAT.
Fashion and consumer-electronics retailers sell a product at full price early in a season and mark down what is left. Consumers learn the pattern, and some of them wait for the markdown. Such strategic consumers lower the revenue of the full-price period, and the retailer's stocking decision affects how deep the markdown is expected to be. Quick response — a second, more expensive replenishment placed after demand is observed — is usually valued as a way to match supply with exogenous demand (Fisher and Raman 1996; Cachon and Terwiesch, Matching Supply with Demand, 2005). Cachon and Swinney ask how strategic waiting changes that value.
The source is the authors' working paper of April 2007, revised November 25, 2007, not the 2009 Management Science version, whose numbering and wording may differ. Its answer: with strategic consumers the retailer stocks less (Theorem 1), and under an explicit cost condition, quick response is worth more to a retailer facing strategic consumers than to one facing only myopic consumers (Theorem 3).
A retailer sells over two periods. It sells at the exogenous full price in period 1 and at a markdown price chosen at the start of period 2. Leftover units are worth . First-period demand has density and distribution function , and satisfies the monotone scaled likelihood ratio (MSLR) property: for every , is monotonic on the support of .
The market has three segments:
The standing assumptions are and . Let be the fraction of strategic values above .
By a threshold argument (Lemma 1), strategic consumers with value below some buy at and the rest wait. A fraction of demand then buys in period 1, and the inventory left for period 2 is . The period-2 revenue counts the waiting strategic consumers with value at least and, if , the bargain hunters, up to the inventory . The retailer's expected profit at unit cost is
With quick response, units ordered before the season cost and units ordered after observing cost , with . The second order covers all first-period demand and may add stock for the sale. The resulting profit is .
In the sale period, waiting strategic consumers are rationed: they effectively face the inventory , where measures their place in the queue. A strategic consumer with value who waits gains, in expectation,
where is the demand level below which the retailer clears stock at . A rational expectations equilibrium is a pair in which maximizes and is a best response of consumers who correctly expect . The superscript denotes the benchmark with only myopic consumers (): and are the optimal myopic profits without and with quick response.
Assume MSLR and no rationing, , , , and condition (6):
Let be any equilibrium without quick response, any equilibrium with it, and , the myopic optima. Then
The milestones follow the paper's path:
Corollary 1 is the percentage form, .
Theorem 3 identifies a second channel through which quick response creates value. Beyond matching supply to demand, it lets the retailer keep its initial stock low enough that a deep markdown becomes unlikely, so strategic consumers buy at full price. Under (6), all of them do. Quick response thus reduces strategic waiting without withholding availability, unlike the inventory-signalling remedies in the literature, and the theorem quantifies when this effect dominates.
The results are proved in the working paper, partly in a technical appendix. No machine-checked version of them, or of the underlying markdown game, is known. A formalization pins down several statements that the paper states loosely:
It also produces reusable components: the newsvendor with salvage and the reactive-capacity fractile under a general density, and a rational-expectations equilibrium predicate for a retailer–consumer game.
The profit is not concave: with strategic consumers it is concave–convex (Figure 4 of the paper). The newsvendor argument therefore does not give a unique optimal order, and Lemma 3's quasi-concavity rests on MSLR in a short appendix step.
Existence (Theorem 1) needs a fixed point of the map best response, but the consumer best response is a correspondence, not a function, so the printed intermediate-value argument does not apply directly. Theorem 3 needs a statement about every equilibrium with quick response, while Theorem 2's proof only exhibits one. Ruling out an equilibrium with requires comparing the derivative (4) of with the myopic derivative along the whole demand distribution.
Lean represents prices, quantities and valuations as reals, demand by a density on , and expectations as Lebesgue integrals against . The model carries the standing assumptions of §3 as fields, plus the following additions and corrections, each disclosed in the item notes:
Optimal revenues are suprema over all prices (and with quick response). "Optimal order" means a maximizer over all , never a stationary point, and the myopic benchmarks are the same functions at . Defining the optimal revenue by Lemma 2's closed form would make Lemma 2 and the first-order conditions definitional; it is not done.
The fill rate is , set to when no strategic consumer waits. With Lean's instead, would be a best response to every order and Theorem 2's last claim would be trivial.
A complete development needs:
The last two are reusable beyond this mission. Proofs of any milestone, alternative existence arguments, and sorry-free proofs of the newsvendor items are welcome. The comparison ", " of Theorem 2 and §8's numerical study are outside the scope.
In a stochastic multi-armed bandit a player repeatedly chooses one of arms and receives a random reward drawn from that arm's unknown distribution; the aim is to pull suboptimal arms as rarely as possible. Lai and Robbins (1985) and, for general models, Burnetas and Katehakis (1996) showed that any reasonable strategy must pull a suboptimal arm at least times in rounds, where is a minimal Kullback–Leibler divergence defined below. A strategy whose expected number of pulls matches this constant is asymptotically optimal.
For rewards in , classical index policies such as UCB (Auer, Cesa-Bianchi and Fischer, 2002) achieve pulls but with a constant governed by the gap of the means, not by . Cappé, Garivier, Maillard, Munos and Stoltz, Kullback–Leibler upper confidence bounds for optimal sequential allocation, Ann. Statist. 41(3), 2013 (arXiv:1210.1136v4), introduce the KL-UCB family of index policies and prove finite-time bounds whose leading term is the Lai–Robbins/Burnetas–Katehakis constant. This mission formalizes their result for empirical KL-UCB (Algorithm 3, Theorem 2), which is asymptotically optimal in the nonparametric model of finitely supported distributions on . A companion mission covers kl-UCB in one-parameter exponential families (Theorem 1).
Timeline: Lai and Robbins (1985), lower bound for parametric families; Burnetas and Katehakis (1996), lower bound and asymptotically optimal policies for general models; Honda and Takemura (2010, 2011), the DMED algorithm, asymptotically optimal for finitely supported and bounded rewards; Cappé et al. (2013), the first index policy with a non-asymptotic bound whose leading term is optimal in this model.
A bandit has arms with reward distributions in a known model : the set of probability distributions over with finite support. Write , and ; arm is suboptimal if . At each round the player picks an arm based on past observations and observes a reward drawn from . is the number of pulls of arm up to round .
Equivalently, each arm has a reward stack of i.i.d. draws from , all stacks independent, and the -th pull of arm returns . The empirical distribution of the first rewards is , and .
The minimal divergence is
the smallest Kullback–Leibler divergence from to a distribution of the model whose mean exceeds .
Empirical KL-UCB (Algorithm 3) pulls each arm once, then for pulls an arm maximizing
where is the set of probability distributions carried by and . The added point is essential: without it the index is the empirical-likelihood bound, which equals the empirical mean when every observation is .
Assume for all arms and . There is a constant depending only on and such that, for every suboptimal arm and all ,
The constants are the paper's. is the one quantity the main text does not give; it is existentially quantified, before the bandit, so it may depend on nothing but .
Theorem 2 gives a finite-time bound whose leading term, , equals the Burnetas–Katehakis lower bound for the model . Hence empirical KL-UCB is asymptotically optimal among all strategies for finitely supported rewards in , and the regret inherits the optimal constant. Since is at least the Bernoulli divergence of the means, and usually larger, the bound improves on kl-UCB and UCB for the same rewards. Proposition 1 is a non-asymptotic coverage bound for the empirical-likelihood upper confidence bound with the point added, valid for every law on , not only finitely supported ones.
The proofs of Theorem 2 and Proposition 1 are in the paper's supplemental article (Appendix B), not in the main text; no machine-checked proof of either exists. The mission produces formal statements of the theorem and of the proof skeleton (5)–(10) that the paper shares with Theorem 1, and of the two facts about that the bound needs. A formal proof would supply an explicit , which the paper defines only inside the supplement.
The skeleton (5)–(10) is elementary bookkeeping; the difficulty lies in the two sums it leaves, both of which must be shown to be with explicit constants. The second, , needs a deviation estimate for the empirical of a suboptimal arm that is precise enough to keep the leading constant : a bound that only controls the deviation of the empirical mean loses it, since depends on the whole distribution. The first, , concerns the optimal arm after a random number of pulls , which the algorithm itself determines, so fixed-sample bounds such as Proposition 1 do not apply directly. Both need regularity of as a function of a distribution in an infinite-dimensional model, where none of the closed forms of the exponential-family case is available.
Arms are Fin K, and arm of the paper is index . The bandit is the platform's stack-of-rewards model RegretBandits.Stochastic.IsStochasticBandit: (indexed from ) are independent, identically distributed within each arm, with mean . Pull counts and are the platform's pullCount and bestMean. Added to the page, and disclosed in each statement: every reward lies in pathwise (a representation of " is carried by "), every arm choice is measurable, and in the goal the strategy is non-anticipating ( is measurable with respect to the arms and rewards of rounds ). A run of Algorithm 3 is a pathwise predicate: rounds pull distinct arms, and every later round pulls a maximizer of , with ties broken by any rule. KL is Mathlib's InformationTheory.klDiv in , with the empirical distribution as first argument. is kept in and converted to a real number only in the final bounds, where it is finite and positive. Probabilities of events whose measurability is not asserted are outer probabilities. The page's in (10) is stated as the finite sum over that (8) produces. The probability space of Theorem 2 lies in Type.
Trivializing formalizations are ruled out. The index is a supremum over a set that is nonempty (it contains ) and bounded above, so it is never Lean's junk value. and range over , not over all measures. The run predicate has both the initialization and the argmax clause. is quantified before the bandit and the horizon.
Reusable beyond this mission: for , the empirical-likelihood bound of (15), and Proposition 1, a concentration inequality for empirical that applies to any bounded i.i.d. sample. Proofs of any milestone are welcome, as are proofs of the skeleton (5)–(10) that also apply to the companion kl-UCB mission.
Many design problems in control, finance and engineering are convex programs whose constraints depend on an uncertain parameter : a solution must satisfy for every in a possibly infinite set . Enforcing all constraints (robust optimization) is often intractable or overly conservative. The scenario approach draws independent samples of , solves the convex program with those constraints only, and asks how likely it is that the resulting solution violates a fresh constraint. The question matters wherever a randomized design is certified by a confidence statement, from robust control to chance-constrained portfolio selection.
Timeline.
Let be a probability space, with , and let and () be convex closed sets. The violation probability of a point is
For a multi-extraction , the program minimises over . It is assumed that every has a unique solution . A constraint is a support constraint of if its removal changes the solution. A convex has at most support constraints (Proposition 2.2). The problem is fully-supported if, for every , the program built from independent samples has exactly support constraints with -probability one.
Two further objects carry the argument. For of cardinality , is the set of multi-extractions whose support constraints have exactly the indexes in . The violation law is
the distribution of the violation of the solution built from samples.
For a fully-supported problem, every and every ,
The result. Equation (2.3) shows that the scenario bound (2.2) is tight: no bound that depends only on , and can be smaller, because a fully-supported problem attains it. The distribution of is then a Beta law, being the probability that a variable is at least , the same for every fully-supported problem. This is what fixes the sample sizes used in practice: is chosen so that the binomial tail is below a confidence level . Fact (3.2), that has distribution function whatever the problem, is a distribution-free statement of independent interest.
Formalizing it. The result is proved in the source. As far as is known it has no machine-checked proof. The goal statement is already posed on the platform, and this mission supplies the paper's proof structure as milestones. Two milestones are reusable outside the scenario approach: the uniqueness of a distribution on given the moments , and the incomplete-beta identity for binomial tails.
The obvious route would compute the law of directly, but it depends on the geometry of the constraints. The paper never computes it. It obtains the law of only implicitly, through the infinite family of identities (3.4), and recovers it by a uniqueness theorem for moment problems. Two points need care. First, full support holds only almost surely: duplicated samples, for instance, produce programs with fewer than support constraints, so every set identity holds only up to null sets. Second, the claim that removing a non-support constraint keeps the first constraints as the only support constraints uses Proposition 2.2. Two identical non-support constraints show that a constraint can become a support constraint after another is removed, unless the count is bounded by .
Goal. The goal is the already-posed platform statement ScenarioApproach.Generalization.violation_tail_eq_binomial_sum_of_fullySupported (theorem id cffaa932-832c-42ca-9e81-1848ffab7e34), referenced as it stands and not restated. Proposition 2.2 is the platform statement card_support_constraints_le_dim (f70e8aa3-…). This mission adds the PART 1 steps as milestones under ScenarioExact.PartOne.
Representation. Decisions are vectors in EuclideanSpace ℝ (Fin d). A multi-extraction is ω : Fin m → Δ, with 0-based indexes, so is and "" are the indexes . is Measure.pi (fun _ : Fin m => P). , the feasible set, solutions, support constraints and full support are the published definitions violation, feasibleSet, IsSolution, IsSupportConstraint and FullySupported. A support constraint is one whose removal admits a feasible point of strictly smaller cost, which under uniqueness is the paper's "its removal changes the solution". Full support is almost sure, not pointwise.
Hypotheses made explicit. Assumption 1 is entered as existence and uniqueness of the solution for every number of constraints and every sample, together with a family of solution maps θs k, each assumed to solve and to be measurable. Under uniqueness, θs N is the goal's solution map. The paper's "measurability ... is assumed for granted" (p. 4) is replaced by joint measurability of and measurability of the solution maps, the same two hypotheses as the goal. No set is assumed measurable. The nonempty-interior clause of Assumption 1 is unused in PART 1 and is not assumed, so the milestones compose with the goal.
Conventions. is the push-forward measure violationLaw on , with = violationLaw … (Set.Iic α). Integrals against are lower Lebesgue integrals of nonnegative integrands, as extended nonnegative reals: over for , and over for in the partition chain, since that integral comes from the event . The integration-by-parts identity is a real interval integral. Ranges are , , and .
Ruled out. A pointwise "exactly support constraints for every sample" would be unsatisfiable for many problems (repeated samples) and would trivialise the probabilistic content, so it is not used. Assuming measurability of the event or of , or the identity , as a hypothesis would assume part of the conclusion, so none of these is a hypothesis.
Infrastructure. A complete development needs: the support-constraint count (Proposition 2.2, a Helly-type argument), invariance of product measures under coordinate permutations, the change-of-variables formula for push-forward measures, the Hausdorff moment uniqueness theorem on , and the binomial–incomplete-beta identity. The last two are general results, and contributions of them are welcome independently.
MAXCUT asks for a partition of the vertices of a weighted graph into two sets that maximizes the total weight of the edges between them. It is one of Karp's original NP-hard problems, so no polynomial-time exact algorithm is expected, and the natural question is how close a polynomial-time algorithm can come to the optimum. Sampling a uniformly random partition already achieves, in expectation, half of the optimal value. For two decades this factor was essentially the best known.
Goemans and Williamson (J. ACM 42(6), 1995) replaced the combinatorial problem by a semidefinite relaxation, solvable in polynomial time by interior point methods, and rounded its solution with a random Gaussian hyperplane. They proved that the resulting cut has expected weight at least times the maximum. The technique founded the use of semidefinite programming in approximation algorithms. Khot, Kindler, Mossel and O'Donnell (SIAM J. Comput. 37(1), 2007) showed that, assuming the Unique Games Conjecture, no polynomial-time algorithm achieves a better constant. Nesterov (Optim. Methods Softw. 9, 1998) extended the rounding analysis to maximizing any positive semidefinite quadratic form over the hypercube, with the constant .
This mission formalizes the presentation of these results in §6.6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (arXiv:1405.4980v2), pp. 343–347.
Let and let be a symmetric matrix with non-negative entries; is the weight between points and . The graph Laplacian is , where is the diagonal matrix with entries . For the vector encodes a partition, and MAXCUT is (6.7)
Write for the Frobenius inner product and for the symmetric positive semidefinite matrices. Since and has unit diagonal, MAXCUT is bounded above by the SDP relaxation
A solution of the relaxation is any feasible matrix attaining this maximum. The rounding draws , a centered Gaussian vector with covariance , and outputs coordinatewise.
For symmetric with non-negative entries, , any solution of the relaxation, and :
The separately stated Laplacian identity on p. 346 is also included as a theorem item: if for all , then ; for , .
For , a solution of , and :
The result. Theorem 6.11 is a polynomial-time randomized -approximation for MAXCUT: the relaxation is a semidefinite program, and sampling a Gaussian vector and taking signs is cheap. Repeated sampling turns the bound in expectation into a cut of value close to times the optimum with high probability. The same scheme of relaxation followed by randomized rounding underlies approximation algorithms for MAX-2SAT, correlation clustering and quadratic programs over the hypercube, and Nesterov's Theorem 6.13 is the version for an arbitrary positive semidefinite objective.
Formalizing it. Both theorems were proved long ago. To our knowledge neither has a machine-checked proof in Mathlib. The platform has related statements from other books, in different forms: Grothendieck's identity for a standard Gaussian and two unit vectors, and the relaxation guarantee with a Grothendieck constant. This mission states the textbook's results for a Gaussian with a possibly singular covariance matrix, which is the form the rounding uses. A complete development needs Sheppard's formula for a degenerate bivariate Gaussian, an elementary but careful real-variable inequality, and a link between Mathlib's multivariate Gaussian and Gram factorizations of . All three are reusable.
The algebra (the Laplacian identity and milestone 4) is routine. The probabilistic core is Lemma 6.12. The textbook argument reduces it to the probability that a uniformly random direction separates two unit vectors, which is "a quick picture" on paper. In Lean this requires showing that the pair has the law of for a standard Gaussian , and then computing an angular measure in the plane, including the degenerate cases , where the pair is supported on a line. A density-based argument fails there, because has no density when is singular, and singular solutions of the relaxation occur (for instance ). Inequality (6.8) is a statement about a transcendental function on a closed interval with a tight constant ( against the true minimum ), so crude estimates do not suffice near the minimizer .
Matrix (Fin n) (Fin n) ℝ, vectors Fin n → ℝ. is Matrix.PosSemidef, which includes symmetry, and is trace (Mᵀ * X).ProbabilityTheory.multivariateGaussian 0 Σ on EuclideanSpace ℝ (Fin n), defined for every positive semidefinite , singular ones included. Expectations are Bochner integrals against it, and each theorem also asserts integrability of its (bounded) integrand.Real.sign would give , which takes out of ; the two agree almost surely because .Finset.sup') over the Boolean vectors read as vectors, so it is never a junk value. "The solution" of the relaxation means any maximizer, and maximizers exist since the feasible set is compact and contains the identity.Retailers of seasonal goods (fashion, electronics, airline seats) sell a fixed stock over a finite season to customers who arrive over time, and those customers know that prices may fall. A customer who expects a markdown waits, and a seller who ignores this loses revenue. The classical revenue-management literature (Gallego and van Ryzin 1994; Talluri and van Ryzin 2004) models myopic customers who buy on arrival or leave; the literature on forward-looking (strategic) buyers, for instance Aviv and Pazgal (2008), studies particular price paths.
Board and Skrzypacz ask the mechanism-design question: among all selling schemes, which maximizes the seller's expected discounted revenue when buyers arrive over time, have private values and time their purchases strategically? Their answer, published in the Journal of Political Economy in 2016, is that the optimal mechanism has a simple structure: in every period the seller sells to the highest remaining buyer if and only if his value exceeds a cutoff that depends only on the period and the number of units left. When demand is weakly decreasing over time, the cutoffs are characterized by one-period indifference conditions, which in the continuous-time limit can be implemented by posted prices. The source used here is the authors' accepted manuscript of February 6, 2015; all page numbers refer to that manuscript.
A seller has units of a good and sells them over periods ; unsold units are worth zero after period . Payoffs are discounted by . At the start of period a random number of buyers arrives, independently across periods, with a law that may depend on . Each buyer wants one unit; his value is drawn independently from a distribution with continuous density , distribution function and support . The marginal revenue of a buyer with value is
assumed strictly increasing and continuously differentiable, with .
By the standard mechanism-design reduction (§2.1, eq. (2.5)), the seller's problem is to choose when to serve each buyer so as to maximize the expected discounted sum of the served buyers' marginal revenues. The state in period , after the period- entrants have arrived, is the number of units left and the values of the buyers present. The value and the pre-entry value satisfy the Bellman equation (4.3):
where is the set of buyers left after the highest are served and the next period's entrants. Selling one unit to today rather than none gives the difference function
and the cutoff is the smallest with . Comparing selling to today with waiting and selling at least one unit tomorrow (to the best of and the entrants) gives (p. 17). Demand is weakly decreasing in the usual stochastic order if for all and .
If is weakly decreasing in the usual stochastic order then, for every ,
and is the unique root of in for : the seller is indifferent between selling to the cutoff type today and waiting one period to sell that unit tomorrow (the one-period-look-ahead property).
For every and , the optimal rule sells to the highest buyer iff , whatever the values of the lower buyers; ; and is the unique root of .
In attack order:
After the goal, (4.7) gives the period- cutoff equation .
Theorem 1 says that the optimal allocation does not depend on how many buyers are present or what their values are, only on time and inventory. This is what makes the optimal mechanism implementable without eliciting values from buyers as they arrive. Theorem 2 turns the global dynamic program into local indifference conditions. In the continuous-time limit (§5 of the paper) these become differential equations, and the optimum is implemented by posted prices with an auction at the end of the season. Under weakly decreasing demand, therefore, the classical revenue-management practice of posting prices loses nothing against the best possible mechanism.
The paper's results are proved, in prose, with envelope-theorem and coupling arguments. They have not been machine-checked. A formal development would produce a verified backward-induction model of multi-unit dynamic allocation with random arrivals, with the structural results (monotonicity, deterministic cutoffs, monotone comparative statics in inventory and time) that recur across dynamic pricing and optimal stopping. Two printed gaps are recorded below: the positivity of , and the restriction of footnote 12 to .
The obvious argument fails at "deterministic". A priori the cutoff for the highest buyer depends on the values of the lower buyers, because selling a unit today changes which of them will be served later and when. Lemma 3(a) holds only under the induction hypothesis that all future cutoffs are already deterministic and decreasing in inventory, so Lemma 3, Theorem 1 and (A.1) form a single backward induction over periods and units, and none of them can be proved in isolation. The value function is an expectation, over a random number of i.i.d. entrants, of a maximum over sorted values, so continuity and strict monotonicity in (Lemma 3(b), and the same for ) are not available from general facts. The tempting argument for Theorem 2, that cutoffs fall over time simply because fewer buyers arrive later, is incomplete: Lemma 4 has to compare two periods with different arrival laws and different future cutoffs at once.
Periods are natural numbers with , and units are natural numbers. Values, marginal revenues and profits are real numbers. The buyers present form a finite multiset of reals, and an absent buyer is absent, never a value . The value law is the measure with density ; the density is positive and continuous on and zero outside, and is defined from and . Expectations over a cohort are lower Lebesgue integrals against of nonnegative bounded quantities, so no non-measurable or non-integrable integrand can silently become . The value function is defined by the Bellman equation (4.3), with . The sequence problem (4.1) over purchase times is not formalized; the paper says either may be used (footnote 16).
Standing assumptions and handled gaps:
The cutoff is defined from , never as the threshold of an optimal policy, and "optimal" always means maximal in (4.3) over every number of units sold. A formalization that postulates a threshold policy, replaces the random cohort by its mean, or sets absent buyers to value would trivialize or change the statements and is ruled out. The mechanism-design reduction (IC/IR to (2.5)) and the continuous-time results of §5 are out of scope.
The usual stochastic order is the published platform definition StochasticOrders.Usual.UsualOrder. A complete development needs finite-horizon dynamic programming over multisets, expectations of functions of sorted i.i.d. samples, envelope arguments, and monotone coupling for the usual stochastic order on ; these parts are reusable beyond this mission. Proofs of any milestone are welcome, as is a proof that (4.3) agrees with the sequence problem (4.1).
Many optimization problems in machine learning minimize an average of losses, one loss for each observation. A full gradient step examines every observation, while a stochastic gradient step examines one. The latter is cheaper per step, but its sampled gradient can remain noisy even near the optimum. Section 6.3 of Bubeck's monograph studies stochastic variance reduced gradient descent (SVRG), which periodically computes a full gradient at an anchor point and uses it to correct subsequent sampled gradients. The question for this mission is whether that correction gives a geometric reduction of the expected objective gap at the constants printed in Theorem 6.5.
Bubeck places this method alongside full gradient descent and stochastic gradient descent for finite sums. The section records that earlier stochastic average gradient and dual coordinate ascent methods attain a gradient-computation cost of order for the same regime, where is the number of components and is a condition number. The target here is the precise SVRG convergence statement in the book, rather than a comparison of implementation costs. The source's discussion on pp. 334–336 gives the context and the algorithm.
Let be differentiable convex functions, with , and define the finite-sum objective and its gradient by
Each component is -smooth when its gradient is -Lipschitz in the Euclidean norm: for all . The average is -strongly convex, meaning that for all it lies at least above its first-order affine approximation at . The constants and are positive, minimizes over , and .
An epoch begins at an anchor . Its first inner iterate is . For , draw uniformly from , independently across steps and epochs, and update
The next anchor is the average . In particular, this average uses through , while the last updated point is excluded. Starting from an arbitrary and repeating the epoch produces . The expectation of is over all sampled indices in the first epochs.
Theorem 6.5 sets and and asserts, for every ,
The epoch length is a count, so the statement takes and explicitly requires . The goal uses exactly the book's step size, epoch length, and contraction factor.
Lemma 6.4 bounds by . Equation (6.3) bounds the second moment of the corrected sampled direction by the objective gaps at the current point and the anchor. Equation (6.2), the unbiased-direction display, and the one-step display express how that direction changes squared distance to . The later display on p. 338 bounds one epoch for any positive step size with . Finally, equation (6.1) substitutes the stated constants to obtain the factor for one epoch. These seven source claims form the milestone list in reading order.
The theorem gives an explicit accuracy guarantee after a specified number of epochs: an initial gap falls below in expectation. Because each epoch uses a full gradient at its anchor as well as sampled component gradients, the result makes clear which quantity contracts and which operations are counted. It is a concrete linear-rate statement for a method whose individual stochastic gradients need not approach zero at the optimum. Bubeck, §6.3 discusses this issue when introducing the correction term.
The mathematical result is already proved in the monograph. The remaining task is to produce machine-checked proofs of its precise finite-sum model, the single-index estimates, the epoch inequality, and the full repeated-epoch guarantee. The mission drafts those statements and definitions; no proof is claimed for the open theorem items. The finite uniform-average representation and the separation between a conditional one-step average and the full multi-epoch average can be reused in other finite-sum stochastic algorithms.
The sampled component gradient need not be small when is near , so a bound using only its norm does not yield the desired fixed-step contraction. The correction has mean zero relative to the full gradient at the current iterate, but its second moment still depends on both and . The proof must control those two gaps while respecting the fact that depends on earlier samples. A single-index estimate with held fixed and an expectation over complete sample histories are different statements; confusing them would make the goal weaker or false.
The carrier is EuclideanSpace ℝ (Fin n) with its usual inner product and norm. The Fin m components and every sample array are finite. A real-valued uniform average is an ordinary finite sum divided by the number of arrays, and and prevent an empty average. Independent uniform sampling is represented by averaging over every function from step positions to component indices. The multi-epoch sample space has one such block for every epoch. There are no integrals or measurability side conditions.
The component assumptions include differentiability with an explicit gradient map, convexity on all of , and the book's gradient-Lipschitz version of smoothness. Strong convexity is imposed on the average objective alone, using the published OnlineConvexOpt.ConvexBasics.StronglyConvexOn definition on the whole space. The book's standing notation assumes a minimizing exists; this is explicit. Positivity of and , and integrality of , make the displayed divisions and epoch length meaningful. The general epoch bound also requires and . Dimension zero is allowed: the theorem remains a statement about the unique point of and its zero objective gap.
The direction always contains the sampled difference and the full anchor gradient . Replacing that direction with would define gradient descent and would not satisfy this mission's algorithm. Contributions are welcome for the finite averaging identities, the component-gradient estimate, the conditional one-step calculation, the epoch inequality, and the induction across epochs.
Many optimization problems in statistics and machine learning ask to minimize an expected loss , or an average over a large data set. Exact gradients of such an are unavailable or too expensive, but unbiased random estimates are cheap: the gradient of the loss at one sample, or of one randomly chosen summand. The observation that first-order methods still make progress when the gradients are only correct on average goes back to Robbins and Monro (1951) and underlies stochastic gradient descent.
Chapter 6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (2015), studies this setting through stochastic mirror descent (S-MD). Its Section 6.1 shows that in the non-smooth case a noisy oracle costs nothing in rate. Section 6.2 asks what smoothness buys: for a general stochastic oracle it cannot buy acceleration, but Theorem 6.3, whose proof the book takes from Dekel, Gilad-Bachrach, Shamir and Xiao (2012), shows that the rate splits into a noise term of order and a smoothness term of order . The book uses it to justify mini-batch SGD. This mission is the fourteenth of a series that formalizes the section capstones of the book.
Let be a finite-dimensional real vector space with an arbitrary norm . Gradients are linear forms on , the value of at is written , and the dual norm is . Let be compact and convex.
A mirror map is a function on an open convex set with and . It is strictly convex and differentiable on , its gradient takes every value, and as approaches the boundary of . Its Bregman divergence is . The map is 1-strongly convex on if there. A function is -smooth on if for .
A stochastic oracle returns, at a query point , a random linear form . When the query point is itself random, the book requires the conditional expectation given the query point, , to be a subgradient of at . In the smooth case it requires together with the variance bound .
S-MD with step starts at and, writing , iterates
Let , and let minimize on .
Let be convex and -smooth, and let the oracle have variance at most . Then for every , S-MD with step and satisfies
For points and , the smoothness step is
If is the S-MD step, the mirror step is
Combining the two gives a pathwise bound on with the cross term . Taking expectations gives the expected one-step bound
For a convex with , S-MD with satisfies
This rests on the deterministic regret bound (4.10) of mirror descent along arbitrary vectors :
Theorem 6.3 says exactly how much smoothness helps under noise. As it recovers the rate of deterministic smooth optimization. For large the noise term dominates; the book notes, citing Tsybakov (2003), that smoothness brings no acceleration for a general stochastic oracle. Averaging independent oracle answers divides the variance by , so the theorem quantifies the benefit of mini-batches: the noise term shrinks by while the smoothness term is unchanged. Theorem 6.1 is the matching non-smooth statement and the template for stochastic subgradient methods in any norm.
These are classical, proved results. None of them is known to be formalized in Lean, and the platform has no stochastic mirror descent statement. Its stochastic gradient items cover the Euclidean strongly convex case and the non-convex gradient-norm case. This mission adds a reusable stochastic-oracle layer in an arbitrary norm, with conditional expectations given random query points, on top of the mirror-map layer of Chapter 4.
The deterministic steps are short manipulations of Bregman divergences. The difficulty is in the passage to expectations. The query point is random, so unbiasedness enters only through the conditional expectation given . Making the cross term vanish requires pulling the -measurable vector out of a conditional expectation of a dual-valued random variable. Every expectation also has to exist. When blows up at the boundary of , the Bregman terms are not bounded a priori, and their integrability has to be derived from the recursion. A further obstacle is that the minimizer may lie on the boundary of , where is not part of the book's data. Treating informally, or assuming , skips exactly these points.
Φ' f' : E → (E →L[ℝ] ℝ), is g v, and is the operator norm. -smoothness is stated with derivatives relative to . is a total function, constrained only by the mirror-map axioms on .A variance hypothesis stated only at deterministic points would not control the random iterates, and is not used. Run predicates that let be an arbitrary point of would make the theorems false, and are not used either.
A complete development needs: first-order optimality over a convex set, the three-point identity of Bregman divergences, the descent lemma in an arbitrary norm, and continuity of the gradient of a differentiable convex function. On the probability side it needs pull-out and conditional Jensen properties for dual-valued conditional expectations. The probability layer is reusable for every stochastic first-order method in the book, including SVRG and random coordinate descent. Proofs of the milestones are welcome, and so are general lemmas about conditional expectations of continuous-linear-map-valued random variables.
Newton's method is the basic second-order method of continuous optimization: at the current point it replaces the objective by its second-order Taylor model and jumps to the stationary point of that model. Its defining property is speed near a nondegenerate minimum, where the error is squared at every step, so that the number of correct digits roughly doubles per iteration. This local behaviour is what makes Newton's method the inner engine of interior point methods, the polynomial-time algorithms for linear, conic and general convex programming (Nesterov and Nemirovski, 1994). In S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015; arXiv:1405.4980v2), §5.3.2 recalls the traditional local analysis of Newton's method, Theorem 5.3, before turning to the affine-invariant self-concordance analysis used for interior point methods. This mission formalizes that theorem and the four steps of its proof.
Let carry the Euclidean norm , and write for the operator norm of a linear map , so that . Let be a function, with gradient and Hessian , a linear map (the derivative of the gradient map). For a real number , means for all .
The Hessian is -Lipschitz if for all .
Newton's method starts at and iterates, for ,
A point is a local minimum of if for all in a neighbourhood of ; it has strictly positive Hessian if for some .
Assume the Hessian of is -Lipschitz, , and is a local minimum with , . If , then Newton's method from is well defined (every Hessian along the iterates is invertible, so the sequence exists and is unique) and
The theorem gives a quantitative basin of quadratic convergence: an explicit radius , depending only on the curvature at the minimum and the Lipschitz constant of the Hessian, inside which Newton's method needs only iterations to reach accuracy . It is the classical statement whose shortcomings (dependence on a choice of norm, constants that change under linear changes of variables) motivate the self-concordance theory of the following subsections, and it is the local convergence result invoked whenever a damped or globalized Newton scheme is shown to enter its quadratic phase.
On the formal side, Mathlib has the calculus this needs (Fréchet derivatives, interval integrals of vector-valued maps, operator norms) but no convergence theorem for multivariate Newton's method for minimization. A formal proof produces reusable pieces: the integral form of the mean value theorem for gradients, the stability of a positive-definite lower bound under Lipschitz perturbations, and an inverse-operator norm bound from a quadratic-form lower bound. The result itself is classical and fully proved in the literature; what is open here is its machine-checked proof in this form.
The individual inequalities are short, but the argument is an induction in which well-definedness and the rate are proved together: the Hessian at is invertible only because is still in the ball of radius , and stays in that ball only because of the rate. A proof that first assumes the sequence exists and then bounds it is circular. The proof also passes between two kinds of control on the Hessian, a lower bound on its quadratic form and an operator-norm bound on its inverse, and the second is only meaningful once invertibility is established. Finally, the integral manipulations need integrability of the maps , which comes from the continuity of the Hessian.
is EuclideanSpace ℝ (Fin n). The gradient and Hessian are explicit maps and with ContDiff ℝ 2 f, HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every point; the norm on is Mathlib's operator norm, as on the page. is the quadratic-form inequality. A Newton run is a sequence indexed from satisfying the linear system ; no inverse of a possibly singular operator appears in any hypothesis, and "well defined" is a conclusion: a unique run exists from and every Hessian along it is bijective. The rate and are asserted for every run. The error representation is stated with both sides multiplied by , which is equivalent to the printed form once the Hessian is invertible. Milestones 3 and 4 use only the Lipschitz property and are stated for any Lipschitz map .
Added hypothesis: (the radius divides by ; with , Lean's convention would collapse the hypothesis to ). Convexity of is not assumed, as on the page; is a local minimum and is derived, not assumed. Encoding the Newton step with Lean's inverse (which returns on singular maps), or replacing by mere invertibility, would change the theorem and is ruled out.
A complete development needs the fundamental theorem of calculus for vector-valued maps along segments, Hessian-based quadratic-form estimates, and operator-norm bounds for inverses; all are reusable for the analysis of damped Newton, cubic regularization and interior point methods. Proofs of the milestones independently of the goal are welcome.
First-order methods, which query only function values and gradients, are the workhorse of large-scale optimization in machine learning, signal processing and operations research, because each step costs little more than one gradient evaluation. For a function that is both strongly convex and smooth, plain gradient descent converges geometrically, but the number of steps needed to reach accuracy scales with the condition number of the problem. In 1983 Nesterov showed that a gradient method with a carefully chosen momentum term needs a number of steps proportional to instead, and that this is optimal for black-box first-order methods. On ill-conditioned problems, where is in the thousands or millions, the difference between and is the difference between practical and impractical.
This mission is the tenth of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015; arXiv:1405.4980v2). It covers §3.7.1, the smooth and strongly convex case of Nesterov's accelerated gradient descent, and its main result, Theorem 3.18.
Work in with the Euclidean inner product and norm . Let be differentiable with gradient .
Nesterov's accelerated gradient descent starts at an arbitrary point and iterates, for ,
The point is a gradient step from , and moves beyond in the direction by the fixed momentum factor .
The analysis in the book uses auxiliary quadratic functions (an estimate sequence), defined from the points by
together with their centres (with and the recursion (3.21) of the book) and their minimum values .
For every run of the method and every ,
The geometric form in milestone 3 is slightly stronger than the goal, which follows from .
Theorem 3.18 gives -accuracy after gradient evaluations. Projected gradient descent with step on the same class contracts only at the rate (Theorem 3.10 of the book). The lower bound of Theorem 3.15 shows that no black-box first-order method can do better than , so the accelerated rate is optimal up to constants. The estimate-sequence argument is the template for many later accelerated methods: proximal, stochastic and variance-reduced variants such as Katyusha, and accelerated coordinate descent.
The result is classical and fully proved on paper. No machine-checked proof of the accelerated rate for strongly convex smooth functions is known to exist in Lean's Mathlib. This mission produces one, with the estimate sequence , its centres and its minimum values as reusable objects, and with every algebraic identity of the book's proof stated separately.
The algorithm is two lines, but its analysis is not a one-step contraction: neither nor decreases by the factor at every step. A Lyapunov argument for gradient descent, applied directly to , gives only the rate . The book obtains the rate through the auxiliary functions . The inequality (3.18) is easy, but (3.19), that the minimum of never drops below , depends on the exact choice of the momentum factor. It holds only through the identity , which ties the centre of to the iterates. Formally, the obstacles are the bookkeeping of the recursive quadratics on and the algebra in , and .
EuclideanSpace ℝ (Fin n). The gradient is an explicit map g with HasGradientAt f (g x) x at every point, which is part of the smoothness predicate IsBetaSmooth f g β. Strong convexity is the published definition OnlineConvexOpt.ConvexBasics.StronglyConvexOn Set.univ f g α, which is the book's (3.13).IsNesterovSCRun g α β x y on two sequences indexed from , with arbitrary. Every theorem holds for every run, that is, every starting point.kappa α β = β / α. All theorems assume and . The second is implied by the other hypotheses for ; no hypothesis is added.ConvexOptAlg.NesterovStrong. β-smoothness duplicates the predicate of other missions of the series and will be merged afterwards. Contributions welcome: proofs of the milestones, and general lemmas on quadratics that the algebraic milestones need.Regularized logistic regression and the support vector machine (SVM) are two of the most widely used linear classifiers. Both are usually introduced as empirical risk minimization plus a norm penalty whose size is tuned by cross-validation, with the penalty justified heuristically as a guard against overfitting. Distributionally robust optimization (DRO) offers a different reading: instead of minimizing the average loss on the training sample, minimize the worst average loss over all distributions close to the empirical one. Blanchet, Kang and Murthy (arXiv:1610.05627v4; J. Appl. Probab. 56(3), 2019) show that, for a suitable notion of closeness based on optimal transport, the robust problem and the penalized problem coincide exactly. The penalty is then the price of robustness against perturbations of the predictors, and the regularization parameter becomes the radius of an uncertainty set, which the same paper later chooses by a statistical criterion (the robust Wasserstein profile).
Related earlier work: Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015) studied Wasserstein-robust logistic regression with a metric that charges a finite price for flipping a label, and obtained regularized logistic regression only in the limit . The result formalized here is the exact statement at , together with the analogous statement for the hinge loss.
Training data are pairs with predictors and labels , . Their empirical distribution is , a probability measure on .
For a cost , the optimal transport cost between probability measures and on is
The cost used here is the label-preserving cost: for ,
Every distribution with has the same label distribution as ; only the predictors are perturbed. The exponent is the conjugate of , .
The losses are the log-exponential loss and the hinge loss , for a coefficient vector . The worst-case expected loss at radius is , the supremum over probability measures on .
For every and every ,
and consequently the two identities obtained by taking on both sides, which is how the paper prints the theorem.
The theorem identifies two standard estimators as exact solutions of a robust decision problem. Consequences: the penalty has a quantitative meaning (the adversary's transport budget), the regularization parameter can be chosen by the paper's robust Wasserstein profile instead of cross-validation, and the norm of the penalty is tied to the geometry of the perturbations (perturbations measured in give an penalty). The same identity is the input of the paper's coverage bound (Proposition 6) for .
The result is proved on paper; no machine-checked version is known. The formalization adds a precise statement of the objects involved (couplings with both marginals fixed, an infinite cost across labels, expectations of nonnegative losses with values in ), a checked version of the duality step specialised to this cost, and the treatment of boundary cases (, , ) that the paper does not discuss.
The identities are short once Proposition 1 is available, so the weight of the mission lies in two places. First, Proposition 1 itself is a strong duality theorem for optimal transport over all probability measures on , with a cost that takes the value and an unbounded loss, and with attainment of the dual minimum; it is quoted from Blanchet and Murthy (Math. Oper. Res. 2019) and not proved in this paper. The weak-duality inequality is routine; the reverse inequality requires constructing near-optimal distributions from the dual, which needs measurable selection of near-maximizers and does not follow from finite-dimensional convex duality. Second, the inner suprema require an exact Hölder-attainment argument for the pair of conjugate norms and , including and , and for the hinge loss a minimax exchange over . Bypassing duality by a direct construction of the worst distribution is possible for the upper value but not obviously for the lower bound at the boundary .
Fin d → ℝ, a data point is (Fin d → ℝ) × ℝ with the product Borel σ-algebra, and samples are indexed by Fin n with 0 < n. Labels are real numbers with the hypothesis , which Theorem 2 inherits from Example 2; the cost is defined on all of .PiLp q, with q p : ℝ≥0∞ and p.HolderConjugate q; and are included, and no further restriction on is imposed.WassersteinDRO.Regularization.empiricalDistribution.PiLp, and calculus for the logistic function. Contributions to any of these are welcome, as are proofs of the inner suprema, which are independent of Proposition 1.Upper bounds for an optimization method say how fast it converges; oracle complexity lower bounds say how fast any method of a given kind can possibly converge. Chapter 3 of S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015, arXiv:1405.4980) proves upper bounds for subgradient descent on Lipschitz functions and for gradient methods on smooth functions. Section 3.5 (Lower bounds, pp. 279–283) shows that these rates cannot be improved by more than a numerical constant, as long as the number of queries is smaller than the dimension. For smooth convex functions the matching lower bound is what identifies Nesterov's accelerated gradient descent, with its rate, as an optimal method.
Timeline. The lower bounds first appeared in A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization (Wiley, 1983). The presentation followed by the book, with an explicit tridiagonal quadratic as the hard instance and the "span of past gradients" restriction on the method, is that of Y. Nesterov, Introductory Lectures on Convex Optimization (Kluwer, 2004), §2.1.2. Nesterov's accelerated method (1983) attains the matching upper bound.
Work in with the Euclidean inner product , coordinates , canonical basis and balls . A first-order oracle for answers a query with a subgradient (the gradient when is differentiable). A black-box procedure maps the history to the next query . Section 3.5 restricts attention to procedures with
which covers gradient descent, its accelerated variants and conjugate gradient. A function is -smooth if its gradient is -Lipschitz; -Lipschitz on if every subgradient at every point of has norm at most ; -strongly convex if is convex.
The hard smooth instance uses, for , the symmetric tridiagonal matrix with entries on the first diagonal positions and on the neighbouring off-diagonal positions of the leading block, zero elsewhere, and the quadratics
For and there are a -smooth convex and a minimizer such that every procedure satisfying (3.15) has
The constant is the book's.
For and there are a convex , -Lipschitz on , and a first-order oracle for it such that every procedure satisfying (3.15) has ; and for there are an -strongly convex , -Lipschitz on , and an oracle with gap at least over that ball.
The upper bounds of Chapter 3 (projected subgradient descent at rate , accelerated gradient descent at rate ) become optimal statements only through these lower bounds: no method in the class (3.15) can be faster by more than a constant factor while is below the dimension. The restriction to is necessary, since Chapter 2's cutting-plane methods converge exponentially once the number of queries exceeds the dimension.
The results are classical and proved. Formalizing them yields machine-checked versions of the quadratic-form computation for the tridiagonal matrix, of the Krylov-type support argument under (3.15), and of the explicit minimizer of , each reusable in other lower-bound arguments (Theorem 3.15 in , lower bounds for strongly convex smooth functions, conjugate gradient analyses). The platform held no formal statement of these oracle lower bounds when this mission was drafted.
Each analytic step is elementary; the difficulty is in the bookkeeping. The span argument is an induction that must track, at each step, that the gradient of a tridiagonal quadratic at a vector supported on the first coordinates is supported on the first , and that the span hypothesis transfers this to the next query. The minimizer computation requires solving on the leading block and showing that the coordinates beyond do not affect . A natural first attempt, choosing the hard function after seeing the procedure, proves a much weaker statement and is excluded by the quantifier order: the function is fixed first and must defeat every procedure.
is EuclideanSpace ℝ (Fin n). Coordinates in Lean are 0-based; the definitions provide the book's 1-based coordinate coord x i and basis vector basisVec n i, and the matrix tridiag n k translates book index to Fin n index . The query sequence starts at index . The oracle is a fixed map , so (3.15) reads with . In Theorem 3.14 the oracle is the gradient, given as a map with HasGradientAt everywhere; -smoothness is the Lipschitz bound on that map. In Theorem 3.13 the oracle is part of what is constructed, because the book's proof uses a specific "resisting" subgradient selection and the claim fails for an arbitrary one.
Committed conventions, each stated in the item's Formalization Note: the minimum over is the bound for every such , and is required; is ; the minimizer is existentially chosen together with (the hard function has many minimizers when , and the bound is false for some of them); the minimum over a ball is the bound against every point of the ball; is the real infimum, asserted to be attained.
A formalization that let the function depend on the procedure, dropped , or took the span over gradients at points other than the queries would state a different and weaker theorem; the statements here keep (and the oracle) before the universally quantified procedure.
Infrastructure needed: quadratic forms of explicit matrices on EuclideanSpace, gradients of quadratics, and span/support lemmas for EuclideanSpace.single-type vectors. Contributions of proofs for any milestone, and of the strongly convex lower bound (Theorem 3.15, not included here), are welcome.
Many planning problems are made in two stages: a first decision (capacity, inventory, a network design) is fixed before an uncertain demand is revealed, and a second decision (recourse, routing, overtime) is taken afterwards. Two-stage stochastic optimization models the demand as random and minimizes expected cost; its second stage is a whole policy , and the problem is intractable in general, especially with integer variables (Dyer and Stougie, 2006). Robust optimization instead picks one static pair that is feasible for every possible demand and minimizes its worst-case cost; it is a single deterministic mixed-integer program and needs no knowledge of the distribution (Ben-Tal and Nemirovski, 2002; Bertsimas and Sim, 2004).
The question this mission addresses is how much is lost by solving the robust problem in place of the stochastic one. Bertsimas and Goyal (Math. Oper. Res. 2010) show that when only the right-hand side is uncertain, the uncertainty set is symmetric and the distribution is centred at its point of symmetry, the loss is at most a factor of two, and that this factor is tight.
Fix , and nonnegative costs , . A set of scenarios carries a probability measure , and each scenario has a right-hand side . The uncertainty set is . First-stage variables are nonnegative, with integer values on a designated set of coordinates; second-stage variables are nonnegative reals ().
The stochastic problem , (1.1), chooses and a policy :
The robust problem , (1.2), chooses one for all scenarios:
A set is symmetric (Definition 1.2) if there is with for all ; is its point of symmetry. Hypercubes, ellipsoids and norm balls are symmetric. A probability measure on a symmetric set is symmetric (Definition 1.4) if it gives a set and its reflection the same mass.
If is symmetric with point of symmetry , , and satisfies
then
The result. The robust problem is one mixed-integer program, independent of ; the stochastic problem optimizes over policies and requires the distribution. Theorem 2.1 says that under symmetry the static robust solution used in every scenario is a 2-approximation of the optimal expected cost, for every centred distribution at once. The companion results of the paper show the hypotheses matter: the bound is tight for symmetric sets, the gap is unbounded (at least ) on the non-symmetric simplex (Theorem 2.6), and unbounded when costs are uncertain as well (Theorem 3.1). The theorem also underlies later work on the power of static and affine policies in adaptive optimization (Bertsimas and Goyal, 2012).
Formalizing it. The theorem and its proof are published; nothing in this mission is open mathematics. To our knowledge none of these statements has a machine-checked proof. The mission produces a reusable Lean model of two-stage stochastic and robust mixed-integer covering problems with arbitrary scenario spaces, extended-real optimal values and genuine expectations, together with the elementary geometry of point-symmetric sets. The same objects are used by the other missions of this series (the simplex and cost-uncertainty gaps, and the adaptability gap).
Each step of the published argument is short; the difficulty is in stating it at the right generality. The paper begins "consider an optimal solution" of ; optimal policies need not exist for an arbitrary scenario space, so the statement is about infima and every step must work for an arbitrary feasible pair. Passing from " for all " to "" needs integrability of the policy and of and linearity of the Bochner integral through a matrix. The bound uses symmetry together with nonnegativity of the uncertainty set; symmetry alone does not give it. Integrality of the second stage breaks the argument, since need not be integral.
Fin k → ℝ with the componentwise order, products A *ᵥ x and inner products c ⬝ᵥ x. The mixed-integer domain is "nonnegative with integer values on a set of coordinates", which is the paper's up to relabelling.Set.range b. Constraints hold for every scenario, not almost surely.EReal, equal to when infeasible; no attainment is assumed. A real-valued infimum would return on an infeasible robust problem and make the goal trivial; that formalization is ruled out.Contributions welcome: proofs of the milestones and the goal, and general lemmas on point-symmetric sets and on interchanging Bochner integrals with matrix–vector products, both reusable outside this mission.
Classical inventory theory chooses order quantities against a probability distribution of demand. The resulting dynamic programs are optimal in expectation but need the distribution, and they become intractable once several installations, capacities or fixed costs interact. Robust optimization replaces the distribution by an uncertainty set and asks for the order sequence whose worst-case cost over that set is smallest. Bertsimas and Thiele (Operations Research 54(1), 2006) applied the budget-of-uncertainty approach of Bertsimas and Sim (The Price of Robustness, Operations Research 52(1), 2004) to finite-horizon inventory control. Their main structural result says that robustness does not destroy the structure of the classical problem. The robust problem is a deterministic (nominal) inventory problem with an explicitly modified demand, and the price of robustness is an explicit constant.
A single item is ordered at a single installation over periods . The stock at the beginning of the horizon is . Orders arrive immediately, demand is subtracted, and excess demand is backlogged, so the stock at the end of period is
The demand of period is uncertain: with a nominal demand , a maximal deviation and a scaled deviation . A budget of uncertainty limits the total scaled deviation up to period . The budgets satisfy and .
Each period costs . The purchasing cost is for and , with and . The holding/shortage cost is , with and . The nominal problem with demand minimizes over for a fixed demand sequence .
For each , is the optimal value of the linear program
It is the worst-case deviation of the cumulative demand up to from its nominal value, with . Write for the nominal stock. The robust formulation (14) minimizes over subject to the following constraints for every :
The variables are the dual of (13). Formulation (14) is equivalent to requiring the holding and shortage constraints of period for every demand whose scaled deviations satisfy and .
Let the modified demand be
Write for the nominal cost of under demand . Then:
The milestones are the steps of the paper's proof, in order:
The theorem reduces robust inventory control to nominal inventory control. Every structural fact known for the deterministic problem then transfers to the robust one. These include the optimality of base-stock policies without fixed cost and the threshold structure with a fixed cost. The robust base-stock levels are explicit: they shift the nominal levels by , upward when shortage is more expensive than holding. The extra cost quantifies the price of protection as a function of the budgets. The paper uses the same reduction for capacitated orders (Theorem 3.3) and for supply networks (§4).
The result has been proved since 2006, and no machine-checked proof of it, or of any budgeted robust counterpart, is known to exist. This mission provides several formalizations for reuse:
The algebraic core, identity (23), is elementary. The work is in the reductions around it. The first is that (14) really is the worst case of (10)–(11): this needs strong duality for (13), together with attainment on both sides, and the observation that the minimizing and maximizing deviations of a constraint pair differ. The second is that the minimum of (14) over the auxiliary variables, for fixed orders, is (21). This requires the dual optimum to be attained with the value of (13), and so that the cost is monotone in . The third is the base-stock part, which needs Lemma 3.1(b), a global optimality statement for a -period problem with backlogging. The paper proves that lemma by an explicit dual certificate. An argument through first-order conditions in each period is not enough, because orders in one period affect every later stock level.
All data are real numbers and sequences are ℕ → ℝ; only indices matter. stock w u k denotes , the stock at the end of period . The standing assumptions of §3.1 are fields of the model:
The conventions and corrections are:
A trivializing formalization is ruled out: the robust cost is formulation (14) with its variables , and is the value of LP (13). Neither is the closed-form objective (21) nor an arbitrary sequence. Contributions are welcome on the LP duality of (13) (a fractional knapsack), on the robust counterpart milestone, and on Lemma 3.1(b), each of which is independent of the others.
Many constrained optimization problems in machine learning and statistics have a feasible set over which a linear function is cheap to minimize but a Euclidean projection is expensive: the -ball, the simplex, the nuclear-norm ball, the convex hull of a combinatorial family. Projected gradient descent needs a projection at every step. Conditional gradient descent, introduced by Frank and Wolfe in 1956 for quadratic programming, replaces the projection by a call to a linear minimization oracle over , and its iterates are convex combinations of oracle outputs, which makes them sparse when is a polytope.
This mission is the seventh of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015, arXiv:1405.4980v2). It covers Section 3.3, whose main result, Theorem 3.8, is the rate of the method in the form given by Jaggi (2013), going back to Dunn and Harshbarger (1978).
Let be a finite-dimensional real vector space with an arbitrary norm . For a linear form on , written , the dual norm is . Let be nonempty, compact and convex, with diameter .
Let be differentiable with gradient , a linear form on . For , is β-smooth with respect to on if
A point with is fixed throughout, and .
Given step sizes , a run of conditional gradient descent is a pair of sequences with and, for every ,
The minimizer need not be unique; any choice is allowed.
If is convex and -smooth with respect to and for , then every run satisfies, for every ,
Theorem 3.8 is the basic guarantee for projection-free first-order optimization. Its rate does not depend on the dimension, and it depends on the geometry only through the product , both measured in the same norm, which may be chosen to fit : for the -ball, smoothness in with dual norm gives much better constants than the Euclidean analysis. The book applies it this way to a LASSO-type problem (Section 3.3, pp. 274–276), and the same bound underlies the sparse-approximation corollary on the simplex (p. 273) and the many later variants of the method (away steps, stochastic and online conditional gradient).
The result is classical and proved in the book. What this mission adds is a machine-checked statement and proof in an arbitrary finite-dimensional normed space, with the dual norm as the operator norm on linear forms, and a reusable encoding of norm-smoothness and of conditional gradient runs. On Prove2Me a related result is already proved: Lan's Theorem 7.1 (First-order and Stochastic Optimization Methods), which bounds by with a different indexing; after the diameter bound it yields at Bubeck's iterate , which is weaker than Theorem 3.8 by one step.
The difficulty is in the bookkeeping of norms and indices, not in a deep idea. Inequality (3.4) is proved in the book only for the Euclidean norm, where and the Cauchy–Schwarz inequality is used; in a general norm it needs the pairing between a linear form and a vector and the bound . The rate is attained only by starting the induction at , where the step erases the dependence on the starting point; at the bound can fail, since is arbitrary. A first attempt that runs the induction from with an arbitrary does not give the stated constant.
is a type with [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]; nothing is specialised to the Euclidean norm. The gradient is an explicit derivative map f' : E → (E →L[ℝ] ℝ) with HasFDerivAt f (f' x) x for every x; is f' x v, and is the operator norm, which equals . is Metric.diam X, which equals the supremum of over because is compact. Sequences are indexed by ℕ with the first iterate at index 1.
Committed conventions: compact, convex and containing (hence nonempty); convexity of and the Lipschitz bound on the gradient are assumed on only, which is weaker than the book's global assumptions; ; the existence of the minimizer is the book's standing assumption (p. 242); the conclusion is stated for , as in the book. Runs are predicates: is any minimizer of the linear form over and is required, so the goal quantifies over every run with . A formalization in which need not lie in , or in which smoothness is assumed only along the iterates, states a different theorem and is excluded.
A complete development needs the descent inequality (3.4) for Fréchet derivatives in a normed space (reusable for every smooth method in the series and beyond), the fact that the iterates stay in , and a scalar induction. Proofs of the milestones are welcome independently; milestone 4 is a statement about real sequences only.
Gradient descent is a basic method for minimizing a differentiable function when evaluating its gradient is practical but solving the optimization problem directly is not. The rate at which its iterates approach an optimizer depends on the assumptions about the function. For a convex function with a Lipschitz gradient, the value error decreases at a sublinear rate. Adding strong convexity changes the behavior: the distance from the optimizer contracts at each step, giving an exponential bound on the value error. This section of Bubeck's monograph identifies a fixed step size that uses both the smoothness and curvature constants and gives the corresponding rate.
The result matters when a high-accuracy answer is needed. A sublinear bound makes each extra digit progressively more expensive; an exponential bound says that a fixed number of additional gradient evaluations reduces the error by a fixed factor. The theorem is a textbook result, already proved mathematically. This mission asks for its precise machine-checked statement and the source's supporting inequalities, rather than for a new optimization method.
Work in Euclidean space with , equipped with its usual inner product and norm. A differentiable function has gradient . It is -smooth when its gradient is -Lipschitz: for every . It is -strongly convex when, for every ,
The first condition limits how rapidly the gradient changes. The second gives a quadratic lower bound on the function around any point. Here and . In positive dimension, the two conditions together entail , so the condition number is at least one. The case remains part of the target.
A point is a global minimizer when for every . The book assumes such a point exists as a standing convention. A gradient descent run is a sequence satisfying at each positive index. Its first iterate is arbitrary. The step size in this mission is fixed at , rather than chosen by line search or adapted along the run.
The central target is Theorem 3.12 of Bubeck, p. 279. For every integer , the gradient descent run satisfies
At this is a smoothness bound on the initial value gap. For subsequent iterations it gives a linear convergence rate with the explicit exponential factor stated in the book. No initial-radius bound or bounded domain is imposed: the actual squared distance appears in the conclusion.
The milestones trace the mathematical claims stated in the source. Equation (3.6) is the co-coercivity inequality for gradients of convex smooth functions. The proof of Lemma 3.11 introduces , and identifies it as convex and -smooth. Lemma 3.11 combines curvature and smoothness into a sharper inequality for two gradients. The proof of Theorem 3.12 then gives a value-gap bound, a one-step distance contraction, and its iterated exponential form. These statements are separately useful: the co-coercivity and contraction bounds can be reused in analyses of related first-order methods.
The theorem states a complete guarantee for the algorithm: an explicit rule, the hypotheses on the objective, and a bound valid for every iteration count. It makes the role of visible. When is close to one, the contraction is strong; when the smoothness constant is much larger than the curvature constant, more iterations are needed for the same error reduction. The stated dependence supports comparisons with projected and accelerated gradient methods elsewhere in the same monograph.
Formalizing the result requires a common interface for actual gradients, smoothness, strong convexity, and algorithm runs. The strong-convexity predicate is an existing published definition, while the local smoothness and run definitions use Bubeck's conventions. Once these interfaces and the inequalities are proved, later missions can use the resulting declarations to compare rates without translating between informal meanings of “smooth” or changing the iterate index. The source provides a mathematical proof; these draft Lean theorems carry sorry and do not yet constitute machine-checked proofs.
The main issue is getting the sharp contraction factor from two assumptions that control different parts of the gradient step. A direct Lipschitz estimate on the update map does not by itself express the mixed inner-product term with the constants needed for the stated factor. Lemma 3.11 is the source's precise bridge between the gradient difference, the point displacement, and their inner product. The case also needs to remain valid: a proof route that divides by cannot cover that boundary by the same calculation.
The last display in the proof of Theorem 3.12 joins a one-step inequality involving to an exponential inequality involving . The latter is the cumulative statement after steps. Keeping these as separate milestones makes each quantified claim explicit while preserving the theorem's bound.
Lean represents as EuclideanSpace ℝ (Fin n), with . The gradient is an explicit map required to be the actual gradient of at every point. Smoothness is the gradient Lipschitz condition, not a quadratic upper bound used as a definition. Strong convexity uses the published OnlineConvexOpt.ConvexBasics.StronglyConvexOn predicate on the whole space; its formula is the book's (3.13). Iterates are indexed from one, and index zero imposes no condition. The norm, inner product, constants, and real exponential follow the printed formulas.
The added explicit conditions are , , and where Equation (3.6) divides by . Positive dimension excludes a degenerate space where curvature imposes no restriction on smoothness. The positivity of makes meaningful; the source treats it as a positive strong-convexity parameter. The minimizer hypothesis is the book's standing convention. There is no assumption that : that property follows from global minimality and differentiability. A gradient map unrelated to would trivialize the model, so the smoothness definition includes the gradient identity.
The local development needs Euclidean inner-product identities, convexity, differentiability, Lipschitz gradient bounds, and real exponential estimates. The auxiliary function and the two co-coercivity inequalities are reusable outside this chapter. Contributions should prove the exact milestone statements and the final theorem, including and , without weakening constants or substituting another gradient descent step.
A shortest path problem asks how to reach a destination at minimum cost. In a stochastic shortest path problem, a decision at a state selects a probability distribution over successor states, so both the route and its total cost are random. Costs may have either sign. This makes the problem relevant to finite-state control models where rewards and expenses occur before eventual termination. Bertsekas and Tsitsiklis analyze this setting without requiring all one-stage costs to be nonnegative or all to be nonpositive. Their condition instead rules out an improper stationary policy whose costs stay finite from every initial state. Bertsekas and Tsitsiklis (1991), pp. 580–583.
Earlier treatments established Bellman-equation and algorithmic conclusions under positive or nonnegative costs. The 1991 paper traces the finite-control development from Eaton and Zadeh and the compact-control extension from Kushner, then removes the sign restriction while retaining finite state space. It also explains why the Bellman mapping need not contract when an improper policy is available. Bertsekas and Tsitsiklis (1991), pp. 581, 585. A separate, proved Prove2Me theorem from Bertsekas's textbook treats the special case in which every policy is proper and controls are finite; the result here permits improper policies and compact control spaces.
There are states. State is the destination. At state , a control incurs a real cost and moves the process to state with probability . A selector chooses one control at every state. A policy may change selectors over time; a stationary policy repeats one selector. The matrix has entries , and is the vector of one-stage costs. Bertsekas and Tsitsiklis (1991), p. 582.
The cost vector is the coordinatewise limit inferior of expected partial costs, including the possibility of infinite values. The optimal cost is the infimum of over all policies, including nonstationary ones. Optimality of a policy means it attains that infimum from every initial state. The fixed-selector operator is ; the Bellman operator takes the coordinatewise infimum of these vectors over selectors. Bertsekas and Tsitsiklis (1991), pp. 582–583, equations (2)–(6).
A stationary policy is proper when its probability of reaching state tends to one from every starting state. Assumption 1 says state is absorbing and cost-free, at least one proper stationary policy exists, and every improper stationary policy has a partial-cost coordinate tending to . Assumption 2 makes each control space compact, each cost function lower semicontinuous, and each transition-probability coordinate continuous. Work takes place in . Bertsekas and Tsitsiklis (1991), pp. 583–584.
Under Assumptions 1 and 2, the optimal cost is finite and is the unique fixed point of in . Every initial has
A stationary selector is optimal exactly when ; an optimal proper stationary selector exists. These are all clauses of Proposition 2, rather than separate targets selected from it. Bertsekas and Tsitsiklis (1991), p. 586, Proposition 2.
The milestone list follows the source's Proposition 1, Lemmas 1–3, and the numbered equations used by their proof. Proposition 1 supplies a weighted maximum-norm contraction when every stationary policy is proper. Lemma 1 describes fixed costs of a proper policy and characterizes properness through a Bellman inequality. Lemma 2 gives continuity of . Lemma 3 controls limits of proper policies; its second part detects a limit that becomes improper through diverging costs. Appendix equations (22) and (24), and the policy-improvement equation (15), provide the paper's intermediate targets. Bertsekas and Tsitsiklis (1991), pp. 585–587, 591–592.
Proposition 2 identifies the cost of the best policy by a finite-dimensional Bellman equation even though the definition of optimal cost ranges over all, possibly nonstationary, policies. Its convergence clause justifies value iteration from any vector whose destination coordinate is zero. Its policy criterion and existence clause connect a fixed point to an implementable stationary decision rule. The paper applies these conclusions to successive approximation and policy iteration in §4. Bertsekas and Tsitsiklis (1991), pp. 586, 590–591.
The paper proves these statements. This mission seeks machine-checked proofs of their exact finite-state formulation and of the listed intermediate results. The resulting finite stochastic-matrix, hitting, and policy-cost infrastructure can also support other undiscounted control problems. The related proved Prove2Me result for the all-proper finite-control case does not settle this mission's compact-control or improper-policy cases.
When every stationary policy is proper, a common weighted maximum norm makes the Bellman mapping contract. An improper policy can destroy this route: Figure 2 has an absorbing destination and satisfies both assumptions, yet is not a contraction in any norm on . The main result therefore needs a way to retain fixed-point uniqueness and convergence without a uniform contraction rate. Compactness matters because a sequence of proper selectors may converge to an improper selector; Lemma 3 explains the associated cost behavior. Bertsekas and Tsitsiklis (1991), pp. 585–586, 591–595.
States are Fin n, with the paper's state represented by 0; the model requires . A control set is a type with a metric, with compactness asserted for its whole carrier. Transition rows explicitly have nonnegative entries summing to one. These are the probability-vector conditions implicit in the word “probability.” Assumption 1 supplies a selector and therefore nonempty control sets. The paper writes ; where a theorem uses only Assumption 1, finite real Bellman infima are made explicit through TRealValued. Under Assumption 2, compactness and lower semicontinuity give real attained minima. Bertsekas and Tsitsiklis (1991), pp. 582–584.
Policy costs and their infimum use extended reals so that an improper policy's cost is represented without a default finite value. Proposition 2 concludes, rather than assumes, that has real coordinates. Its policy infimum ranges over every sequence of selectors. Matrix products use the identity at time zero; is the identity. The destination-zero restriction is retained in every fixed-point and iteration claim. Defining optimal cost as a Bellman fixed point, or restricting the infimum to stationary policies, would remove the result the paper proves. Solvers can contribute the finite-chain, matrix-inverse, semicontinuity, and convergence arguments needed by these targets.
Gradient descent goes back to Cauchy (1847). It is the simplest method for minimizing a differentiable function, and most of the first-order methods in large-scale optimization and machine learning are variants of it. Its appeal in high dimension is that its oracle complexity, the number of gradient evaluations needed to reach a given accuracy, can be bounded independently of the dimension. For a merely Lipschitz convex function the projected subgradient method needs on the order of steps to reach accuracy (Theorem 3.2 of the book). Under a smoothness assumption gradient descent does much better, because the gradients shrink near the optimum and the steps adapt automatically.
This mission formalizes the basic result of that kind: Theorem 3.3 of S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015; arXiv:1405.4980v2). It states that gradient descent with step size on a convex -smooth function on has optimality gap after steps. The result and its proof are standard; versions appear in Nesterov's Introductory Lectures on Convex Optimization (2004, §2.1.5). It is the fourth mission in a series that formalizes the capstone results of Bubeck's monograph.
Write for Euclidean space with inner product and norm . Let be differentiable with gradient .
The optimality gaps are .
If is convex and -smooth with , is a minimizer, and is gradient descent with , then for every
These are the statements the book's proof uses, in the book's order:
Under the same hypotheses, for every .
Theorem 3.3 is the reference rate for first-order methods on smooth convex problems. Several later results in the book are measured against it. Nesterov's accelerated gradient descent (§3.7) improves to , the lower bounds of §3.5 show that cannot be beaten by any black-box first-order method, and adding strong convexity (§3.4) upgrades to a linear rate. Its ingredients are reused throughout the book and the optimization literature: the descent lemma (Lemma 3.4), the one-step improvement (3.5) and co-coercivity (3.6). Co-coercivity is the finite-dimensional case of the Baillon–Haddad theorem.
The result is classical and fully proved on paper. To our knowledge Mathlib does not contain this rate for gradient descent on convex smooth functions, and no published Prove2Me theorem states it. The mission provides it, together with Lemma 3.4 and co-coercivity as reusable statements on EuclideanSpace ℝ (Fin n). These are the facts that later missions of the series on projected gradient descent, strong convexity and acceleration need. Formalizing the improved constant of footnote 4 is a welcome addition.
Two steps are not routine. The first is Lemma 3.4, where the book integrates the gradient along a segment. In Lean this needs a mean-value or fundamental-theorem-of-calculus argument for a function on a Euclidean space, together with a Cauchy–Schwarz estimate, and Mathlib's HasGradientAt interface has to be connected to one-variable derivatives along lines.
The second is the monotonicity of . The natural first attempt is to telescope the one-step improvement (3.5) together with the convexity bound . That gives a recursion involving , which is not controlled by without further work. Making the recursion uniform requires co-coercivity (3.6), which comes from Lemma 3.5. That lemma's hypothesis is the two-sided inequality (3.4), not smoothness directly. The final numerical step divides by the gaps , so zero gaps need separate handling.
EuclideanSpace ℝ (Fin n), and is ⟪x, y⟫_ℝ.∀ x, HasGradientAt f (g x) x.IsBetaSmooth f g β) is the book's definition: , the gradient-existence hypothesis, and the Lipschitz bound . The book's "continuously differentiable" follows from it.ConvexOn ℝ Set.univ f. A minimizer is a point xstar with ∀ y, f xstar ≤ f y; its existence is the book's standing assumption, and is derived, not assumed.IsGDRun g η x) is a sequence x : ℕ → ℝⁿ with and for every . The book's is x 1, and index is unused. Every theorem quantifies over all runs with .Disclosed side conditions:
A trivializing formalization is ruled out. Smoothness is the Lipschitz condition on the gradient, so Lemma 3.4 and (3.4) are not restatements of the definition, as they would be if the quadratic upper bound (3.4) were taken as the definition of smoothness. The run predicate also fixes the step size .
A complete development needs:
HasGradientAt functions;Lemma 3.4, Lemma 3.5 and (3.6) are reusable well beyond this mission. Proofs of any milestone are welcome independently.
Two observers, Alice and Bob, share a quantum system. Alice performs some intervention (a measurement, possibly followed by discarding part of her apparatus) and Bob, somewhere else, performs his own. If the statistics of Bob's outcomes could depend on what Alice chose to do, Alice could send Bob a message through the shared system alone, and if the two interventions are spacelike separated this would be a signal faster than light. Quantum mechanics and special relativity coexist peacefully only because this does not happen: the no-communication theorem guarantees that Bob's marginal statistics are independent of Alice's intervention whenever the two interventions are "local" to different parts of the system.
The review article of Peres and Terno, Quantum information and relativity theory (Rev. Mod. Phys. 76, 2004), develops the operational toolkit of quantum information (Kraus matrices, positive-operator-valued measures, completely positive maps) in Sec. II.D and then derives, in Sec. II.E, a sufficient algebraic condition for the absence of instantaneous information transfer: all of Alice's Kraus matrices commute with all of Bob's (their Eq. (9)). This mission formalizes that derivation together with the facts about Kraus matrices and complete positivity that the same pages state.
A quantum state on a finite-dimensional Hilbert space is a density matrix : a positive semidefinite complex matrix with .
An intervention with outcomes is described by Kraus matrices , where the label ranges over a finite set indexing the subsystems discarded at the end of the interaction. When outcome occurs, the state is updated (Eq. (6)) to the unnormalized matrix
and the probability of outcome is . The matrices
(Eq. (8)) are the POVM elements; the intervention is complete when .
A map on matrices is positive if it sends positive semidefinite matrices to positive semidefinite matrices, and completely positive if , acting blockwise on matrices over , is positive for every ancilla dimension .
For the no-communication theorem, Alice's Kraus matrices and Bob's Kraus matrices act on the same finite-dimensional space. The probability that Bob obtains , irrespective of Alice's outcome, is (Eq. (10))
If for all , Alice's POVM is complete, and is a density matrix, then for every outcome of Bob
so all of Alice's operators disappear from Bob's statistics.
The no-communication theorem is the consistency check between quantum measurement theory and relativistic causality, and it is the starting point of the relativistic measurement theory developed in Sec. III of the review. The commutation condition (9) is exactly what local quantum field theory provides for spacelike separated regions, so this algebraic form is the one later used for microcausality arguments. The Kraus representation (milestones 4-5) is a basic structural theorem of quantum information theory, and the failure of complete positivity for transposition (milestones 6-7) underlies the partial-transpose entanglement criterion.
The results are classical and their proofs are known; the mission produces machine-checked versions on top of Mathlib's matrix library. The finite Kraus representation theorem (milestone 5) requires Choi-matrix machinery that is not, to the knowledge of this proposal, available in Mathlib in this form; it is reusable well beyond this mission.
The goal and milestones 1-3 and 8 are finite-dimensional trace manipulations; the care needed is in keeping the order of products right, using the adjoint of the commutation relation, and summing over indices in the correct order. Milestone 7 needs an explicit entangled witness on . Milestone 5 is the substantial one: the obvious approach of writing in a basis does not produce Kraus operators directly; a positivity argument (via the Choi matrix of and its spectral decomposition) is needed.
All Hilbert spaces are finite dimensional: matrices are indexed by arbitrary finite types with complex entries. Outcome sets and discarded-subsystem label sets are finite types; Alice's and Bob's label sets may depend on the outcome. Kraus matrices for the single-intervention milestones may be rectangular (), reflecting that the system after the intervention may differ from the original one; in the no-communication theorem both observers' matrices are square on a common space. The order on used for "nonnegative probability" is the standard partial order ( iff is real and nonnegative). Complete positivity quantifies over ancillas for every , with acting blockwise. Time reversal is encoded by the linear map ; on Hermitian matrices this coincides with complex conjugation, and only the linear extension gives a meaningful complete-positivity statement.
The goal keeps the hypotheses of the source setting (both POVMs complete, a density matrix); none of them can be dropped silently by a degenerate encoding, and the conclusion is an identity of complex numbers, so no hypothesis is vacuous: for instance, single-outcome trivial interventions with satisfy all of them.
Note: the sentence on p. 100 of the source claiming that commuting POVM elements are necessarily orthogonal projections is not included; as stated it fails (e.g. ).
Airlines sell the seats of one flight leg at several prices. Cheaper fare classes tend to book earlier, so the seller must decide, as low-fare requests arrive, how many seats to hold back for later and more valuable passengers. The standard control is nested protection levels: a number of seats is reserved for the most expensive classes together, and a request of class is accepted only while more than seats remain. Littlewood (1972) gave the optimal rule for two classes; Belobaba's EMSR heuristic (1987, 1989) extended it to many classes without an optimality guarantee.
S. L. Brumelle and J. I. McGill, Airline Seat Allocation with Multiple Nested Fare Classes (Operations Research 41(1), 1993) treat any number of classes with independent random demands and characterize optimal protection levels by first-order conditions on the expected revenue: Theorem 1 states that a policy with in the subdifferential of the expected revenue of the highest classes at , for every , is optimal. Their Theorem 2 addresses the question practitioners face first: seats and bookings are whole numbers. If demand is integer valued, is an optimal policy available among integer protection levels? The theorem answers yes. This mission formalizes that theorem and the chain of results in its proof.
Timeline.
Classes are numbered , class paying the highest fare. Class has a random demand and fare , with . The demands are mutually independent on a probability space . A protection-level policy is a sequence with ; the dummy level is never used.
For a demand vector and available seats, the revenue of the highest classes is defined recursively (Eqs. (8)–(9), p. 130):
The expected revenue is . A policy is optimal if it maximizes for every and every (p. 130).
For a function and , and are the right and left derivatives, with , and the subdifferential is (p. 131). Condition (20) is
A function is CLBI (Concave and Linear Between Integers, p. 132) if it is concave on and linear on each interval ,
If every is integer valued and the fares are positive, there is a policy with such that
and satisfies (20). The competitor ranges over all real protection levels.
and the analogous formula for at . 4. Corollary 1 (p. 131): concavity of and give concavity of . 5. CLBI propagation (p. 133): if is CLBI and integer satisfy (20), then is CLBI. 6. (30): for large enough, . 7. Theorem 1 (p. 131): a policy satisfying (20) is optimal.
The result. Theorem 2 justifies computing protection levels in whole seats: with integer demand, restricting to integer policies loses nothing against arbitrary real protection levels. The construction also shows that (20) is solvable at every level, so the sufficient condition of Theorem 1 is never empty for integer demand. Many later revenue-management models assume an optimal nested policy exists and rely on this result or its dynamic-programming analogues.
Formalizing it. The theorem is proved on the page by an induction on the class index, but several steps are compressed: (28)–(29) are printed without the range of on which they hold, and (30) is asserted "by recursive application". To our knowledge none of these statements has a machine-checked proof. A formal development gives a verified account of one-sided derivatives of expectations of piecewise-linear random functions and of the integer covering property. These pieces are reusable for other newsvendor-type and nested-inventory models. The probability-condition characterization (Theorem 3) is the subject of a companion mission in the same series.
Concavity of the expected revenue does not hold for arbitrary policies. It is only guaranteed level by level, when the protection level already chosen at level satisfies (20). Existence of an integer optimum therefore cannot be obtained by rounding a real optimum: the integer levels must be chosen one at a time, and each choice must preserve both concavity and the CLBI shape needed for the next. A second obstacle is analytic. The one-sided derivatives of are expectations of derivatives of a random piecewise-linear function. Exchanging differentiation and expectation, and computing the sums in (28)–(29) exactly at integer and non-integer , is where informal arguments and formal ones diverge. Finally there are infinitely many classes, so the policy is an infinite sequence built by recursion.
Related work on the platform. The two-class, integer-capacity EMSR rule of Belobaba (1987) is formalized as SeatInventory.Nested.emsr_protection_level_optimal. It is a relative of the case of Theorem 2, but it lives in a different model: two classes, a fixed integer capacity, and only integer competitors.
Data-dependent risk bounds in statistical learning theory control the gap between the expected loss of a learned function and its empirical loss by a complexity penalty that is computed from the training data. The first such penalties were the maximum discrepancy of a function class (Bartlett, Boucheron and Lugosi, Model selection and error estimation, Machine Learning 48, 2002) and its Rademacher complexity (Koltchinskii, Rademacher penalties and structural risk minimization, IEEE Trans. Inf. Theory 47, 2001; Koltchinskii and Panchenko 2000). The maximum discrepancy compares the behaviour of the class on two fixed halves of the sample; the Rademacher complexity compares it on two random halves. Bartlett and Mendelson (JMLR 3, 2002), Lemma 3, show that these two quantities are equivalent up to a factor 2 and an additive . This mission formalizes that lemma from the published JMLR article (pp. 463–482); the proof is its Appendix A.
Let be a probability measure on a measurable space and let be independent samples from . Let be a class of measurable functions . Let be independent uniform -valued random variables, independent of the sample.
The Rademacher complexity of is
For even , the maximum discrepancy of is the random variable
with no absolute value, and the expected maximum discrepancy is . The class is closed under negation if implies , and .
The proof works with the conditional supremum function
defined for the values that can take.
For every even ,
and if is closed under negation,
Lemma 3 makes the maximum discrepancy and the Rademacher complexity interchangeable in risk bounds: a bound in terms of one gives a bound in terms of the other with an explicit additive loss. The maximum discrepancy can be computed by a single empirical risk minimization on a relabelled sample, while the Rademacher complexity has the structural properties (monotonicity, convex-hull invariance, contraction) that make it easy to bound for concrete classes; the lemma transfers the second kind of estimate to the first quantity.
The lemma is proved in the paper; no machine-checked proof of it, or of the comparison between fixed and random half-sample splits, is known to exist. Formalizing it requires the exchangeability argument for i.i.d. samples, the conditioning of a uniform sign vector on its sum, and a moment bound for the Rademacher sum , all with explicit constants.
The heart of the proof is that, conditioned on the number of positive signs, a uniform sign vector splits the i.i.d. sample into two random subsets of fixed sizes, and every split of the same sizes has the same law as the fixed split. Making this precise requires a permutation-invariance argument for product measures applied to a supremum over an arbitrary class, where measurability is not automatic. The step from classes closed under negation to general classes is where the printed argument is loose: since has no absolute value, is a maximum of two suprema that may be negative, and the naive bound fails.
The Lean development lives in the namespace RadGauss.Discrepancy. Sign vectors are Fin n → Bool (true ↦ 1, false ↦ -1) and expectations over signs are finite averages over all sign vectors; is the average over the sign vectors with sum . takes values in (a lower Lebesgue integral of an -valued supremum), while , and are real, because the maximum discrepancy is signed. Inequalities of the form are written with real terms embedded by ENNReal.ofReal; this is equivalent to the printed form since for nonempty .
Hypotheses added to the page, all disclosed in each item:
Corrections of printed statements:
A formalization in which or is a junk value (non-integrable or non-measurable suprema, an empty class, an odd sample size with truncated ) would make the goal trivial or meaningless; the hypotheses above rule that out, and the class satisfies all of them.
Welcome contributions include general lemmas on the invariance of under permutations of an i.i.d. sample, conditioning of uniform sign vectors on their sum, and the bound . These are reusable well beyond this mission.
Finding the quickest route between two points of a road network is among the oldest problems of operations research. It is the subproblem inside vehicle routing, network flow and many dynamic programs. Richard Bellman's four-page note On a routing problem (Quarterly of Applied Mathematics, 1958) treats it as a dynamic program. The minimal travel times satisfy a nonlinear system of equations, and that system can be solved by successive approximations that terminate after a number of steps bounded in advance. The iteration is now known as the Bellman–Ford method. A footnote added in proof records that Max Woodbury and George Dantzig had obtained the same scheme independently, and Ford's RAND report of 1956 describes a closely related labelling procedure.
Timeline.
There are cities, numbered . Every two of them are linked by a direct road, and city is the destination. The travel time from to is a real number ; the matrix need not be symmetric. Throughout, for .
A route from to is a sequence of cities in which consecutive cities differ. Its stops are , and its time is . The minimal time (3.1) is the least time of a route from to , and .
The routing equation (3.2) is the system
Approximation in policy space (§5) starts from the direct-route policy (5.2), , and iterates (5.1):
The second scheme (§7, (7.1)) starts instead from and uses the same step.
For every the following hold. Each is the minimal time from to , attained by a route. The vector solves (3.2). Every real solution of (3.2) equals :
This is the claim of the Summary ("converges after at most iterations") and of the last sentence of §5. The paper's bound is kept, although also suffices.
The result. The note turns an enumeration over exponentially many paths into rounds of minimisations each, with a bound fixed before the computation starts. The uniqueness theorem makes the routing equation a characterisation of the minimal times, not merely a property of them. This is the template for later correctness proofs of shortest-path and value-iteration algorithms. The monotone decrease (5.5) is the first instance of policy improvement: every iterate is the value of an actual routing policy.
Formalizing it. The results are classical and proved. What this mission adds is a machine-checked development against the paper's own objects. Routes, their times and minimal times are defined from scratch. The iteration is stated exactly as printed, apart from the corrected initial value at the destination. The (N − 1)-step termination is asserted as an equality, not a limit. Related platform items treat other methods and do not cover these statements. One is the label-correcting method (BertsekasDP.label_correcting_correctness_of_nonneg_arcs, BertsekasDP.label_correcting_terminates). Another is the stochastic shortest path problem under a termination assumption that fails for deterministic routing (BertsekasDP.ssp_main_theorem). There are also the generic candidate-list algorithm (BertsekasNetwork.generic_shortest_path_algorithm), Floyd's Algorithm 97 and Dijkstra's method.
The minimum in (3.2) may be attained at a whose own optimal route passes back through . The routing equation is a fixed-point equation for an operator that is monotone but not a contraction in any fixed norm. The standard contraction argument for discounted dynamic programs therefore does not apply. Uniqueness has to use to exclude zero-time cycles: with , the system (3.2) has infinitely many solutions. The bound depends on the at-most--stops reading of and on the fact that an optimal route never needs to revisit a city. Neither is visible from the recursion alone. For the scheme of §7, the page gives no bound on the number of iterations, and none holds uniformly in .
Cities are Fin (n + 1), so , with standing hypothesis . City is Fin.last n, and travel times are t : Fin (n + 1) → Fin (n + 1) → ℝ with for . Diagonal entries are unconstrained and never used. No symmetry, triangle inequality or integrality is assumed. A route is a list of cities with distinct consecutive entries ending at . Repeated cities are allowed; with positive times this changes no minimum. Minimal times are attained minima over routes (IsMinTime, IsMinTimeWithin), not real infima. The minimum in (3.2) is a Finset.inf' over all , the destination included.
The paper's loose phrases are made explicit as follows.
Two printed slips are corrected. (5.2) is printed for , which would set , and with statements (5.4), (5.5) and the goal would be false. The formalization uses , the value the paper's own justification needs. (7.1) prints "" for . Section 6 (computational aspects) and the closing expectation of §7 that the first method converges faster are not formalized.
The goal cannot be satisfied trivially. The minimal times are defined from routes, not as a solution of (3.2) or as a limit of the iteration, so the goal connects the recursion to the routing problem itself.
The development needs only finite minima, lists and induction; nothing beyond core Mathlib. The route and minimal-time layer is reusable for other deterministic shortest-path results. Proofs of any milestone are welcome, as are proofs of the sharper bound .
Kernel methods, such as support vector machines, predict with functions of the form : finite expansions of a fixed similarity function centred at data points. Their statistical behaviour is governed by the size of the class of such expansions that the method searches. Bartlett and Mendelson, in Rademacher and Gaussian Complexities: Risk Bounds and Structural Results (JMLR 3, 2002), develop risk bounds in terms of the Rademacher and Gaussian complexities of a class, and in §4.3 (pp. 476–478) compute these complexities for the class of kernel expansions whose coefficient vector has quadratic form . The resulting bound depends on the kernel only through its diagonal , which is what makes margin bounds for support vector machines dimension-free. This mission formalizes that computation. The source is the published JMLR article (pages cited by the journal's printed numbers).
Let be a compact topological space. A kernel is a continuous function such that for every and all the Gram matrix is symmetric and positive semidefinite. For the class of kernel expansions is
with centres anywhere in (Lean: kernelClass k B).
For a class of real functions on and a sample , let be independent uniform signs and independent standard Gaussians. The empirical Rademacher complexity and empirical Gaussian complexity (Definition 2, p. 464) are
For a probability measure on and an i.i.d. sample , the Rademacher complexity is and the Gaussian complexity is (Lean: empiricalRademacher, empiricalGaussian, rademacherComplexity, gaussianComplexity).
A feature map of is a map into a real Hilbert space with .
With ,
For any feature map of , , and hence .
For every sample ,
The goal shows that the kernel class has complexity of order , with a constant given by and the quantity , which is the trace of the integral operator on . No dimension of the feature space enters. Fed into the paper's margin-cost risk bound (Theorem 21, p. 476), the sample-wise Lemma 22 gives a data-dependent misclassification bound for support vector machines in terms of the trace of the Gram matrix of the training sample. Bounds of this form are the standard complexity estimate for kernel classes in learning theory textbooks.
The result is proved in the paper; nothing in this mission is open mathematics. What the mission adds is a machine-checked version with the paper's normalization (factor , absolute value inside the supremum), covering both the Rademacher and the Gaussian complexity, for expansions with centres anywhere in . Related statements on the platform (Mohri et al.'s Theorem 5.10 and Proposition 9.3) use the normalization without absolute value, assume a uniform bound , and treat only the Rademacher case, so they do not imply the targets here.
The class is defined through the kernel, not through a feature map, and its expansions have arbitrarily many centres anywhere in . The supremum over is therefore a supremum over an infinite-dimensional family, and must be controlled without assuming a separate numerical upper bound on or that the feature space is finite dimensional. For the Gaussian complexity the supremum sits inside an expectation over a continuous random vector, and the passage from the sample-wise bound to the expected bound must move an expectation inside a square root in the right direction. A bound with in place of is weaker and is not the target.
Conventions committed to in Lean:
ℝ≥0∞); expectations over the Gaussian vector and over the sample are lower Lebesgue integrals against product measures, and the Rademacher expectation is the exact average over the sign vectors . An unbounded class has complexity , so a junk value of for a real supremum or a non-integrable expectation cannot make the bounds trivial.IsKernel k) carries compactness of , joint continuity, and positive semidefiniteness (with symmetry) of every Gram matrix, as in the paper's definition. The goal puts the Borel -algebra on and assumes is a probability measure; is the Bochner integral of the continuous function .FoundationsML.Kernels.RKHS_exists.A trivializing formalization is ruled out: the goal is stated for the kernel class itself, not for the larger ball of linear functionals of a feature map, and not for the subclass with centres at the sample points.
Infrastructure a complete development needs: Gaussian integration over (second moments of a standard Gaussian vector), Jensen's inequality for the square root under a lower Lebesgue integral, and Cauchy–Schwarz for positive semidefinite bilinear forms (or the RKHS feature map). The Definition 2 complexities are shared with the paper's other missions and reusable. Contributions of any of these milestones, and of proofs of the goal that avoid the feature map, are welcome.
Black-box convex optimization asks how many queries to an oracle are needed to minimize a convex function to accuracy . In fixed dimension the answer is of order , and the first algorithm to attain it is the center of gravity method, discovered independently by Levin (1965) and Newman (1965). It is the opening example of cutting plane methods: algorithms that keep a set known to contain a minimizer and shrink it with one half-space per oracle call. The ellipsoid method and Vaidya's method, which underlie the polynomial-time solvability of linear programming and convex feasibility problems, follow the same template with cheaper sets. This mission is the first of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (2015), and covers its §2.1.
Timeline:
Let be a convex body: a compact convex set with non-empty interior. Let be continuous and convex, and let be a minimizer of on . A vector is a subgradient of at if for every . The first order oracle returns, at a query point, some subgradient there; the zeroth order oracle returns the value of .
For a set of finite positive volume, its center of gravity is
The center of gravity method sets and, for , computes , queries the first order oracle at to obtain a subgradient , and sets
After steps it outputs , found with calls to the zeroth order oracle.
The Lean development names these objects IsConvexBody, IsSubgradientOn, centroid and IsCenterOfGravityRun in the namespace ConvexOptAlg.CenterGravity.
For every run of the method and every ,
Theorem 2.1 is a linear rate whose number of queries to reach accuracy , , depends on the dimension only linearly and on the accuracy only logarithmically, and matches the Nemirovski–Yudin lower bound. It is the reference point against which the ellipsoid method ( queries) and Vaidya's method are measured, and the randomized center of gravity method of §6.7 of the book rests on the same analysis. Grünbaum's inequality is a basic fact of convex geometry with uses well beyond optimization, for instance in the analysis of query complexity and of approximate centroid computations by random walks.
On the formal side, the theorem has been proved since 1965 and the lemma since 1960; neither is known to have a machine-checked proof. A complete development adds to Mathlib-based libraries the center of gravity of a set, the volume of homothetic images in the form used here, Grünbaum's inequality, and a reusable predicate for cutting plane runs. The later missions of this series (the ellipsoid method in particular) reuse the shrunk-copy argument of milestones 4 and 5.
The steps (2.2), the shrunk-copy volume and the value bound are short. The volume decay and the final comparison are bookkeeping once one knows that each cut keeps the method's sets convex bodies with positive volume. The difficulty is Lemma 2.2. A half-space through the centroid need not split the volume evenly: for a cone the smaller side tends to of the volume as , so no symmetry argument works, and the bound must hold uniformly in the dimension. The classical proofs rely on tools of convex geometry, such as volume comparisons between a body and a symmetrized body, that are not available in Lean in the needed form. A second source of work is that the method's sets are defined through centroids: it has to be shown that they remain convex bodies of positive volume, so that each centroid is the genuine center of gravity, and this fact is not available before the volume estimates are.
is EuclideanSpace ℝ (Fin n) with Lebesgue measure volume; volumes are kept in in every statement. The function is a total map f : EuclideanSpace ℝ (Fin n) → ℝ with , continuity and convexity required on only; its values off are irrelevant. Subgradients are relative to (Definition 1.2). A run is a predicate on sequences indexed from ; the oracle's choice of subgradient is free, and every theorem holds for all runs. The minimizer is a hypothesis, as in the book's standing notation; it exists here by compactness. The output is any argmin, so the goal bounds the minimum .
Added hypotheses, all disclosed in the statements: in the goal, because the exponent is undefined for ; and in Lemma 2.2, that the centered set is a convex body, because in Lean the integral of a non-integrable function is , which would make every unbounded convex set "centered". The milestone on volume decay assumes , which is the book's own reduction.
The center of gravity is defined with the real volume and is meaningless when that volume is or infinite. The run predicate does not assume the volumes are positive; that every set of a run is a convex body of positive volume is part of what has to be proved, and a formalization in which runs could degenerate to sets of zero volume, or in which the centroid is an arbitrary point, is not the book's method.
Contributions welcome: proofs of any item; a general Grünbaum inequality for convex sets of finite positive volume; lemmas on centroids (membership in the closed convex hull, translation behaviour) that later missions can reuse.