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?
The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the accepted cutoff-87 theorem already covers every , the new work is the range from 85 to 87.
The cutoff came down from 90 to 87 in a day, through moona3k's proofs at 89, 88 and 87. The 89 proof reran the cutoff-90 argument with sharper, second-order estimates. A numerical model of that argument with retuned constants puts its limit between about 86.6 and 87.5: two of its steps pull the same parameter in opposite directions, and below that point no setting satisfies both. So reaching 85 is expected to need a new idea, not just tighter numbers. The goal theorem below gives the exact statement.
This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 85 or lower also settles this mission.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryMaximum pressure policies schedule a stochastic processing network by choosing, at each decision time, an allocation of processors to activities that maximizes a linear "pressure" built from the current buffer levels and the network's input-output matrix. Dai and Lin (Oper. Res. 53(2), 2005) prove that such policies are throughput optimal: they stabilize the network whenever any policy can. The policies descend from the back-pressure rule of Tassiulas and Ephremides (IEEE TAC 37(12), 1992) for wireless networks and are now standard in switching, manufacturing and data-center scheduling.
The general theory lets a processor split its capacity among several activities at once. In many systems this is impossible: a machine works on one job type at a time. Section 7 of the paper shows that with this restriction Harrison's static planning LP no longer characterizes stability, and Section 8 shows that forbidding preemption can make a maximum pressure policy unstable. Both difficulties disappear for one structural class, the reversed Leontief networks, in which every activity needs exactly one processor. This mission formalizes the two lemmas that make that class work: extreme allocations are integral (Lemma 1), and a maximum pressure allocation is found processor by processor (Lemma 3).
A network has buffers , where Buffer is the outside world and are the internal buffers; activities ; and processors . The resource consumption matrix has if activity requires processor and otherwise. The constituency indicator records that activity processes buffer . An input activity processes only Buffer ; a service activity never processes Buffer . Each processor runs input activities only (an input processor) or service activities only (a service processor). Each activity has a mean processing requirement , rate , and a routing matrix .
The input-output matrix is
An allocation is with for every processor and for every input processor; is the set of allocations, its set of extreme points, and the allocations with integer coordinates. For a buffer-level vector , the network pressure is and the activity pressure is , with for the idle Activity .
The network is reversed Leontief if each activity requires exactly one processor. The possible activities of processor are for an input processor and for a service processor. Under an integer allocation , is the activity processor works on, or if is idle.
For a reversed Leontief network, and ,
A further supporting item, not a milestone, states the decomposition of an allocation along one processor (proof of Lemma 1, p. 215).
The result. Lemma 1 says that, in a reversed Leontief network, the maximum pressure policies of the processor-splitting theory are automatically non-processor-splitting, so the paper's throughput optimality theorem holds in the setting where machines cannot be shared. Lemma 3 says that the maximization over the (exponentially large) set decouples into one small maximization per processor: each processor picks an activity of largest activity pressure among its own options. This separability is what makes the nonpreemptive version of the policy well defined and is the key step towards Theorem 9 (throughput optimality of nonpreemptive maximum pressure policies). It also covers multiclass queueing networks with alternate routes (§9.1), which are reversed Leontief.
Formalizing it. Both lemmas are proved in the paper; to our knowledge neither is machine-checked. The mission produces a reusable Lean model of the allocation polytope of a processing network with input processors, its integer and extreme points, and the activity and network pressures. The integrality of is a total-unimodularity-type fact for a block structure that is not available in Mathlib in this form.
The pressure is linear, so maximizing over equals maximizing over ; the substance is the description of . The polytope is not a box: input processors carry equality constraints and service processors inequality constraints, and in general networks (an activity needing several processors) contains fractional points, as the paper's example in §7 shows. The step that fails for general networks is the decomposition of a fractional allocation along a single processor: it needs every activity of that processor to use no other processor. In Lean, extreme points must be handled through Mathlib's Set.extremePoints, and the argmax over must keep track of the idle option, which exists for service processors and not for input processors.
Indices are 0-based: internal buffers Fin I, buffers with Buffer Fin (I+1) (Buffer is 0, internal buffer is i.succ), activities Fin J, processors Fin K. The idle Activity is none : Option (Fin J), with activity pressure and unit vector . is Set.extremePoints ℝ 𝒜. "Maximizes the pressure over " is stated by domination ( for all ), never through a supremum. is defined by choice of an activity of at level ; it is used only for , where it is unique.
The standing assumptions of §2 are carried as one hypothesis: and are –, constituencies are nonempty, every activity is an input or service activity and needs a processor, processors are input-only or service-only, at least one input activity exists, and . Two disclosed additions: every input processor has at least one activity (otherwise (2) is infeasible and ), and (needed for ). The goal keeps as on the page; two milestones drop it, which strengthens them.
A trivializing formalization would make empty or give input processors an idle option; both are excluded: is the extreme-point set of the real polytope , which is nonempty for a reversed Leontief network under the standing assumptions, and the idle option belongs to only for service processors, as in (60).
Contributions welcome: proofs of the milestones, a general lemma that – points of a subset of the unit cube are extreme, and the separable description of extreme points of products of simplices, which is reusable beyond this mission.
Second-order stochastic dominance constraints let a decision maker require that a random outcome of a decision be preferred to a fixed benchmark outcome by every risk-averse expected-utility maximizer, without choosing a utility function in advance. Dentcheva and Ruszczyński introduced optimization under such constraints in Optimization with stochastic dominance constraints (SIAM J. Optim., 2003), for the case where the decision enters the outcome linearly (the pure-dominance case). Their follow-up paper, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints (Math. Program., 2004), allows the decision to affect many random outcomes in a nonlinear, concave way, and derives optimality and duality theory in which the Lagrange multipliers of the dominance constraints are utility functions.
In applications (portfolio selection against a benchmark index is the paper's own example in §6) the probability space is a finite set of scenarios. Section 5 of the paper specialises the theory to that case. This mission formalizes that section: the reduction of the dominance constraints to finitely many inequalities, and the optimality and duality theorems (Theorems 6 and 7) in which the multipliers become piecewise-linear concave utilities.
There are scenarios with probabilities , , and benchmark constraints, indexed by ; . A decision ranges over a convex set . For each scenario , is the objective contribution and the th outcome, all concave. The benchmark has realizations . Write .
The second-order dominance of a finitely distributed (realizations ) over on an interval reads
The split-variable problem (38)–(41) is
for all , , over and . The Slater condition asks for and satisfying the dominance constraints (39) with for all .
The utility set consists of the functions that are concave, nondecreasing, piecewise linear with break points only at the , and zero on . With multipliers for the splitting constraints , the Lagrangian is
Multipliers of the inequalities (39) generate the utility (46). The dual functional is (47).
Under the Slater condition, optimal for (38)–(41) implies that there are and with
conversely, these conditions together with feasibility imply optimality.
Theorem 6 says that, for finitely many scenarios, the infinite-dimensional multiplier of the general theory (a concave utility in a cone of functions, Theorem 2 of the paper) can always be taken piecewise linear with kinks exactly at the benchmark's realizations. The multiplier space becomes finite-dimensional, is a polyhedral cone, and the dual problem of Theorem 7 is a finite-dimensional convex program. The paper's decomposition (49)–(51) of the dual functional and its numerical method in §6 rest on this. Lemma 2 is the standard reduction that makes dominance against a finitely distributed benchmark a finite set of polyhedral constraints, used throughout the later literature on dominance-constrained portfolio optimization.
The results are proved in the paper; none of them is formalized. The mission produces machine-checked statements of the finite-scenario theory, a Lean model of the utility set and of the correspondence between nonnegative multipliers and piecewise-linear utilities, and a Kuhn–Tucker theorem for concave programs with polyhedral constraints and a relative-interior Slater point.
The obvious route to Theorem 6 is to invoke a Kuhn–Tucker theorem. The available formal versions require every inequality constraint to hold strictly at the Slater point and range over all of . Neither fits: the dominance constraint at the smallest realization has right-hand side and a nonnegative left-hand side, so it can never hold strictly, and may be lower-dimensional (a simplex), so only its relative interior is available. The polyhedral structure of (39) must be used, as in Rockafellar's Theorem 28.2. The second obstacle is the converse direction of the multiplier–utility correspondence: a utility in must be written as a nonnegative combination of the kinks , which requires handling repeated realizations and the one-sided slopes at each break point.
Fin N → ℝ; , , are Fin m → Fin n → ℝ; expectations are finite sums and positive parts are max t 0. No measure theory is used.intrinsicInterior ℝ Z, not the topological interior. In the Slater condition only the splitting constraints are strict; the dominance constraints hold non-strictly.EReal supremum.ConvexOptimization.slater_strong_duality, Boyd–Vandenberghe §5.3.2) assumes a strict Slater point for every constraint and no set constraint, so it does not cover milestone 4.A processing network must decide which activities receive scarce processor capacity while jobs move among buffers. Such decisions matter in manufacturing, service systems, and switches: one activity can consume several processors at once, and a job can be routed to another buffer after processing. A policy that sees current buffer levels but does not need to know arrival or routing rates is easier to operate when those rates are difficult to estimate. Dai and Lin's 2005 paper studies whether a maximum pressure policy, which uses the buffer vector and an input-output matrix, can stabilize every network that is stabilizable in their model. Their Theorems 1 and 2 give, respectively, a necessary planning condition for any stabilizing policy and a sufficient condition for maximum pressure under the extreme-allocation-available assumption. Dai and Lin (2005)
Here pathwise stability means that each internal buffer grows sublinearly in time almost surely. This is a rate statement about sample paths. It does not assert positive recurrence of a Markov chain, nor does it require a stationary distribution. The paper allows general primitive processing and routing processes with almost-sure long-run averages. Dai and Lin (2005), §§2–4
There are internal buffers, activities, and processors. Buffer represents the outside world. The matrix records resource use: when activity requires processor . The matrix records which buffers an activity processes. An input activity processes Buffer ; a service activity does not. Input processors serve only input activities and must be fully used, while all processors have at most unit capacity.
For activity , the processing requirements have mean and the routing counts have long-run matrix . Write . The input-output matrix is
Positive means activity consumes net material from internal buffer ; negative means it produces net material there. An allocation assigns nonnegative activity levels subject to the processor capacity bounds and the equality for every input processor. The finite set consists of the extreme points of this allocation set. At buffer vector , allocation has network pressure . The maximum pressure rule chooses an allocation of greatest pressure among the currently feasible members of . Feasibility depends on jobs actually available to each constituent buffer. Dai and Lin (2005), §§2–3
The extreme-allocation-available assumption (EAA) says that for every nonnegative , a pressure maximizer in can be chosen whose constituent buffers all have positive levels. It links the static pressure maximization to the jobs that a policy can process. The static planning LP asks for activity fractions and a service-processor load such that , every input processor has load one, and every service processor has load at most . Dai and Lin (2005), p. 202
The goal is Theorem 2. For a network satisfying EAA and run by a preemptive, processor-splitting maximum pressure policy, LP feasibility with implies
The milestones follow the paper's route from stochastic paths to deterministic fluid limits. A fluid limit is a uniform-on-compact limit of along positive scales . The milestones state that fluid limits satisfy (14)–(18), weak stability of the corresponding fluid model transfers to pathwise stability (Theorem 3), maximum pressure adds (52)–(55) and (20) (Lemmas 5 and 4), quadratic fluid energy obeys (22)–(23), and LP feasibility with EAA makes the maximum-pressure fluid model weakly stable (Theorem 4). Dai and Lin (2005), pp. 203, 213–214
Theorem 2 identifies a policy whose almost-sure buffer growth rate vanishes whenever the planning LP permits load at most one and EAA holds. Together with the paper's necessary condition in Theorem 1, it characterizes the feasibility boundary for this policy class under EAA. Its scope includes networks in which an activity uses multiple processors and processes multiple buffers simultaneously. It does not claim that all such networks satisfy EAA. Dai and Lin (2005), Theorems 1–2
The result is proved in the 2005 article. This mission asks for a machine-checked proof of that known theorem and its selected intermediate claims. The Lean statements are open draft targets. Reusable outcomes include a model of cumulative routing and service counts, a uniform-on-compact fluid-limit interface, and the weak-fluid-stability transfer theorem for networks without a Markov assumption.
Maximizing pressure over the static allocation polytope does not by itself describe an executable service policy. An allocation can demand work from an empty buffer. EAA addresses the existence of a maximizing allocation supported by positive buffer levels, but the stochastic policy acts on actual jobs and completion times. The proof must connect those discrete, pathwise decisions to the limiting differential equation (20). At a regular fluid time, the maximum-pressure equation is decisive; away from regular times, derivatives need not exist. The fluid model therefore carries a time qualifier that cannot simply be dropped. Dai and Lin (2005), pp. 201–203, 214
The Lean model uses finite index types for buffers, activities, and processors. Internal buffers are Fin I; Buffer 0 is the zero index of Fin (I+1), and an internal buffer maps to its successor index. Activity and processor labels use zero-based Fin. Time is real but all network equations are asserted for nonnegative time. The shared Bell–Williams Paths definition supplies the renewal count in and uniform-on-compact distance using the norm. The completion count is required finite wherever the network equations convert it to a natural number; this prevents infinity from becoming a zero count. Bell and Williams (2001)
The network standing assumptions record binary incidence matrices, nonempty constituencies, processor coverage, activity types, and an input activity. Two refinements are explicit: each input processor has an activity, so its mandatory unit allocation is feasible, and , so is defined as the intended positive rate. Routing counts are cumulative and nonnegative. Their row sums are constrained only for buffers an activity processes: the printed sentence requiring the same sum for every buffer conflicts with its immediately preceding statement that the count vanishes when the activity does not process that buffer. The corresponding rows of sum to one for processed buffers and vanish for unprocessed buffers, as follows from (4). Dai and Lin (2005), pp. 199–200
The policy predicate records allocation-time decomposition (49)–(51) and the non-employment consequence of Definition 1 used in (56)–(58). It checks feasibility of a competing extreme allocation through the paper's threshold at every time of the interval. Individual job states and tie breaking are outside the pathwise interface. The goal retains EAA, the exact bound, and all network and policy equations, so an empty allocation set or an unconstrained service path cannot make the target automatic. Contributions formalizing the finite extreme-point set, fluid-limit compactness, Lemmas 4–5, and the weak-stability transfer are welcome.
Infinite-horizon dynamic programs, including discounted Markov decision processes, stochastic games and semi-Markov models, are usually analysed through a single equation: the optimal return solves the optimality equation , where maximizes the one-step return over decisions. Denardo's 1967 paper (SIAM Review 9(2), 165–177) separated the argument from the particular model. It isolated two properties of an abstract return , contraction and monotonicity, and showed that the standard conclusions follow from them alone. The examples of §8 of the paper cover Howard's discounted model, Shapley's stochastic games and Blackwell's, Jewell's and Fox's models.
The plain contraction assumption (each one-step operator shrinks distances by a factor ) fails in models where the process stops only from a subset of states, or where discounting acts only after several transitions. §5 of the paper handles these with the N-stage contraction assumption: only steps of a policy need to contract, while one step only needs to be nonexpansive. This mission formalizes that section. Its companion mission (part 1 of the series) formalizes the plain contraction case.
Timeline:
Let be a set of points. Each point has a decision set . A policy picks a decision at every point, so the policy space is . Let be the bounded real functions on with the metric ; is complete. Write when for every .
The return assigns a real number to each point , decision and . It defines two kinds of operators on :
and both are assumed to map into . An operator on has modulus or less when for all .
Under these assumptions is a contraction, so it has a unique fixed point , the return function of . The optimal return is . The auxiliary operator is .
Under the monotonicity and N-stage contraction assumptions:
The mission also contains two consequences that are not milestones: is optimal for the mathematical programs s.t. and s.t. (§6, p. 171), and a policy is optimal exactly when it attains at every point (§7, p. 173).
Theorem 4 lets models whose one-step operators are not contractions use the contraction-mapping theory of dynamic programming. Under its hypotheses the optimality equation has exactly one bounded solution, and that solution is the optimal return. Successive approximation converges geometrically from below (part (e)). Lemma 2 shows that is the least with and the greatest with . This gives the linear-programming formulation of finite Markov decision processes (Program I) and the policy-improvement argument of §6. The characterization reduces the search for optimal policies to the decisions that attain the maximum in the optimality equation.
The results are proved in the paper. The work of this mission is to formalize them, in the abstract form that Mathlib does not have: monotone operators on bounded functions that are contractive only after steps, with suprema taken over arbitrary, possibly infinite, decision and policy sets. No machine-checked proof of Theorem 4 or of Lemma 2 is known. The closest formal statements, Propositions 4.1–4.2 of Bertsekas and Shreve under their Assumption C, concern a different model (extended-real costs, nonstationary policies) and are themselves unproved formally.
The obvious argument would apply the Banach fixed-point theorem to . That does not work: under the N-stage assumption, need not be a contraction. The paper gives an example (p. 170) with , , where has modulus for every . The supremum over decisions does not commute with composition, so the contraction of each says nothing directly about . The paper therefore works through the auxiliary operator , which is a contraction. The hard step is to show that , the supremum of the policy returns, is a fixed point of . This is the second half of Lemma 2(a), an -argument that uses both monotonicity and the modulus- bound on .
Part (e) holds only for . It is not a contraction property of on all of .
lp (fun _ : Ω => ℝ) ⊤ (as BFun Ω), and its dist is . The order is pointwise (PLe).IsPolicyOperator, IsMaxOperator and IsNStageSupOperator. Every supremum, including (IsOptimalReturn), is a genuine least upper bound (IsLUB). sSup/⨆ are never used, so no junk value can make a statement trivial.ModulusLE B c. NStageContractionAssumption H N c holds , , ModulusLE (H δ)^[N] c and ModulusLE (H δ) 1, with and independent of .v with , the paper's §5 definition. is the conclusion (a), never a hypothesis.IsNStageSupOperator H N E. The milestone Theorem 4 (a)–(c) proves that such an operator exists. is never defined as a fixed point of or . The goal asserts that the pointwise least upper bound of exists in and is the unique fixed point of both.A complete development needs the Banach fixed-point theorem for iterates (Mathlib's ContractingWith, applied to ), suprema of families of real numbers, and induction on iterates. The §3 observation and Lemma 1 are reusable for any monotone operator family on bounded functions. Contributions to every milestone and to the two §6–§7 consequences are welcome.
A stochastic processing network (Harrison 2000) models a system in which processors carry out activities and each activity draws jobs from one or more buffers. Manufacturing lines, call centers with cross-trained agents, and data switches all fit this model. A central question is which scheduling policies are throughput optimal, meaning they stabilize the network whenever any policy can.
Dai and Lin (Oper. Res. 53(2), 2005) show that maximum pressure policies are throughput optimal. These policies generalize the back-pressure rule of Tassiulas and Ephremides (1992) for wireless and switch networks, and at each moment they choose the allocation that maximizes a linear "network pressure". Their main theorem (Theorem 2) has one structural hypothesis, the extreme-allocation-available (EAA) assumption (Assumption 1). It holds for many familiar networks and fails for some (§6.2 gives a counterexample). Theorem 6 identifies a broad class where it always holds: strict Leontief networks, in the sense of Bramson and Williams (2003). This mission formalizes that theorem.
A network has internal buffers , an outside Buffer , activities and processors .
The input-output matrix is
An allocation gives the level at which each activity runs. The allocation set consists of the allocations with for every processor and for every input processor. Write for the set of its extreme points, the extreme allocations. For a buffer-level vector the network pressure is . Buffer is a constituent buffer of if .
Assumption 1 (EAA). For every there is with such that for every constituent buffer of .
A network is strict Leontief if every service activity has exactly one buffer in its constituency, denoted .
The result. Theorem 2 of the paper states that, under EAA, a maximum pressure policy is pathwise stable whenever the static planning problem has a feasible solution with . Theorem 6 removes the EAA hypothesis for strict Leontief networks. In that class maximum pressure is therefore throughput optimal with no further structural condition. The class includes multiclass queueing networks with alternate routes and networks of input-queued data switches (§9), so Theorem 6 is the step that turns the abstract main theorem into a statement about these concrete systems.
Formalizing it. The theorem is proved in the paper and, to our knowledge, has no machine-checked proof. Formalizing it fixes the exact standing assumptions of the model, several of which the paper uses without stating (see below). It also yields a reusable Lean vocabulary for stochastic processing networks with input activities: from (5), the allocation polytope with the input-processor equality (2), extreme allocations, network pressure and EAA. The companion missions of this series on maximum pressure policies build on the same vocabulary.
The naive argument stops at "take a maximizing extreme allocation". A maximizer may run a service activity whose buffer is empty, in which case EAA fails at . Removing such activities gives , which has the right support and pressure but is in general not extreme. The pressure inequality depends on the sign pattern of , which holds only because every service activity has a single buffer. In the network of §6.2 this sign pattern fails and so does EAA. Returning from to an extreme allocation without losing the support property needs a convex-geometry argument about the polytope . In Lean this means relating Set.extremePoints of a compact polyhedron to maximizers of a linear functional and to supports.
Indexing. Internal buffers are Fin I. Buffers including Buffer 0 are Fin (I+1), with Buffer as 0 and internal buffer as i.succ. Activities and processors are 0-based.
Standing assumptions (§2), one predicate Network.Standing.
Disclosed additions to the page.
Conventions.
Set.extremePoints ℝ 𝒜.sSup. Without attainment the statement would be vacuous.Trivializing formalizations ruled out. EAA must not be weakened to a supremum over a possibly empty , and Buffer must not be counted as a constituent buffer. Either change would make the goal trivially true or impossible.
Infrastructure. Solvers need two results:
IsCompact.extremePoints_nonempty and Krein–Milman;Both are reusable beyond this mission. Contributions proving them as general Mathlib-style lemmas are welcome.
Stochastic processing networks (Harrison 2000) model manufacturing lines, data switches, call centers and multiclass queueing networks in one framework: jobs wait in buffers, activities process jobs from one or several buffers at once, each activity may need several processors simultaneously, and routing after service may depend on the activity used. A central control question is which dynamic policy keeps such a network stable whenever any policy can.
Dai and Lin (Oper. Res. 53(2), 2005) answer it with maximum pressure policies, a generalization of the back-pressure policy of Tassiulas and Ephremides (1992) for wireless networks. At each decision time the policy picks an extreme allocation maximizing a linear "network pressure" in the current buffer levels; it needs no arrival-rate information. Their main result (Theorem 2) is pathwise stability whenever Harrison's static planning LP has a feasible solution with . The proof goes through the fluid model: a deterministic, continuous analogue of the network whose stability implies stability of the stochastic system.
This mission formalizes Theorem 5 of the paper, the strong form of the fluid-level result: under a strict load condition and a mild structural assumption, every solution of the maximum pressure fluid model empties in finite time, uniformly over bounded initial states. Fluid stability in this sense (Definition 4) is the property that the standard fluid-limit machinery (Dai 1995) turns into positive Harris recurrence of the stochastic network.
The network has buffers , where Buffer is the outside world and are the internal buffers, activities and processors .
The input-output matrix is . An allocation is with for every processor and for every input processor; is the set of allocations and the set of its extreme points. The network pressure of at buffer level is .
The static planning LP asks for and with , for service processors and for input processors. Assumption 1 (extreme-allocation-available, EAA) says that for every some maximizer of over has on all its constituent buffers. Assumption 2 says there is with componentwise.
A fluid model solution is a pair of paths , buffer levels and cumulative activity times , satisfying (14)–(18): (written out over buffers), , input processors always busy, every processor's busy time at most elapsed time, and nondecreasing with . A time is regular if both paths are differentiable there. Under a maximum pressure policy the solution also satisfies (20): at each regular ,
for every solution of (14)–(18) and (20). The constant depends on the network only.
The result. Theorem 4 of the paper gives only weak stability (a fluid model started empty stays empty) under , which suffices for pathwise stability. Theorem 5 gives a uniform emptying time under , the hypothesis that standard arguments (Dai 1995; Dai and Meyn 1995) need to conclude positive Harris recurrence and moment bounds for the stochastic network. The emptying-time bound is explicit and linear in the initial fluid level.
Formalizing it. The theorem is proved in the paper; to our knowledge no machine-checked proof exists. The closest formalized result on Prove2Me is ProcessingNetworks.BackPressure.bp_maximal_stability (Dai and Harrison's book, Theorem 9.12), which uses the same Lyapunov idea in a different model: exogenous arrival rates, the planning problem , no input activities and no Buffer 0. The present mission formalizes the Dai–Lin model with input processors, where the planning LP has and the equality constraints (2). The definitions file (network, , , pressure, fluid model, (20)) is shared in content with the other missions of this series.
Each algebraic step is short; the work is in the analysis. The obvious route reads as an ordinary differential inequality and integrates it. That requires the inequality almost everywhere, but it is only available at regular points. So one needs: Lipschitz continuity of and on from (16)–(18), almost-everywhere differentiability (Rademacher), and a comparison argument for an absolutely continuous function, , whose derivative bound holds only where . The step "by (20)" also needs the maximum over to dominate every allocation in . That is the vertex property of a bounded polyhedron, which in Lean means compactness of plus a Krein–Milman type argument. The published Dini-derivative extinction criterion ProcessingNetworks.LyapunovCriteria.dini_extinction_criterion (Dai–Harrison Lemma 8.11) is a possible tool for the last step, applied to .
Fin I, buffers as Fin (I+1) with Buffer 0 the index 0 and internal buffer i the index i.succ, activities Fin J, processors Fin K.ℝ → (Fin n → ℝ) constrained only at . Derivatives are deriv, used only at regular points.IsGreatest of the set of pressures over , so the maximum is attained and an empty cannot pass through a junk supremum. is Mathlib's Set.extremePoints.Network.Standing. Two disclosed additions are needed for the objects to make sense: every input processor has an activity, and . The row sums of are not imposed.Contributions of reusable lemmas are welcome, in particular almost-everywhere differentiability of Lipschitz paths on , the vertex property of bounded polyhedra, and extinction of nonnegative absolutely continuous functions with on .
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.
A probability model for a random element is rarely known exactly. Distributionally robust performance analysis replaces the single expectation by its worst case over all models within a prescribed distance of . When the distance is an optimal-transport cost, the neighbourhood contains models whose support differs from that of . That matters in stochastic-process applications such as ruin probabilities for insurance reserves, where the natural alternatives (a compensated Poisson process against a Brownian motion) are mutually singular and likelihood-based divergences such as Kullback–Leibler are infinite.
Blanchet and Murthy (arXiv:1604.01446, Math. Oper. Res. 2019) prove that the worst-case expectation over an optimal-transport ball equals a one-dimensional dual problem. They assume only that the underlying space is Polish, the cost lower semicontinuous and the performance function upper semicontinuous and integrable.
Timeline. Esfahani and Kuhn (arXiv:1505.05116, 2015/2018) obtained a dual reformulation for Wasserstein balls around empirical measures on . Gao and Kleywegt (arXiv:1604.02199, 2016) proved a general duality whose proof, as Blanchet and Murthy note, uses the local compactness of the space. Blanchet and Murthy (2016, v2 2017) removed local compactness and continuity of the cost. This covers path spaces such as and .
Let be a Polish space with Borel σ-algebra , and let be a probability measure on (the baseline model).
The primal feasible set consists of the probability measures on whose first marginal is and whose transport cost satisfies . The second marginal of is the alternative model. The primal objective is , and the primal value is
The universal σ-algebra is the intersection of the completions of under all probability measures. Write for the -measurable functions . The dual feasible set consists of the pairs with , and for all . The dual objective is , and the dual value is . Finally,
Under (A1) and (A2):
The "if" direction is stated without the finiteness assumption.
Weak duality (5). Lemma 15. Strong duality with a primal optimizer on compact , first for continuous costs (Proposition 5), then for lower semicontinuous ones (Proposition 6). Universal measurability of (§4.2). Lemma 16. The restricted dual bound of Proposition 7. Lemma 8. The univariate formula (9):
The result. Formula (9) turns an infinite-dimensional optimization over probability measures into a one-dimensional convex minimization that involves only the baseline . A modeller can therefore evaluate it by sampling from . Theorem 1 is the input for the worst-case probability formula for closed sets (Theorem 3 of the paper) and for the existence of worst-case transport plans (Corollary 1). Its complementary slackness conditions describe the structure of every worst-case plan: mass is moved from to maximizers of , and the budget is exhausted whenever .
Formalizing it. The result is proved on paper. To our knowledge it has no machine-checked proof. The only related statement on Prove2Me is a special case (empirical baseline, bounded continuous loss, power-of-norm cost on ). A complete development would contain duality on compact spaces via Fenchel duality, the extension to σ-compact supports, and measurable-selection arguments for universally measurable functions. The measurable-selection part reuses Bertsekas–Shreve's analytic-set theory, which is already posed on the platform.
The obvious route copies Kantorovich duality. That route fails here because the feasible set fixes only one marginal, so it is not tight on a non-compact space. Prokhorov compactness is available only on compact pieces . The duality must then be transported to the whole space by a limiting argument that keeps control of the dual multipliers.
A second obstacle is measurability. For a merely lower semicontinuous cost on a non-locally-compact space, need not be Borel measurable, so the dual must range over universally measurable functions. Removing the restriction from the envelope (Lemma 8) needs a measurable selection theorem. Arguments that assume closed balls are compact do not apply in the target spaces and .
S carries [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S]. The cost is a real-valued curried function c : S → S → ℝ; (A1) is the structure AssumptionA1; (A2) is UpperSemicontinuous f together with Integrable f μ; and 0 < δ is assumed throughout.EReal. The integral of an extended-real function is with lower Lebesgue integrals, and evaluates to . A coupling with therefore never raises , which is the paper's reading in footnote 2.BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable. For such the lower integral equals the integral against the completion of .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.