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.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
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?
An elliptic curve has rational solutions that can be added using a canonical group law. A torsion point is a rational solution that returns to the identity after a positive number of additions. These points form the finite part of the rational-point group and constrain which finite arithmetic configurations a curve can carry. Barry Mazur determined the possible groups uniformly over all elliptic curves defined over the rational numbers. The theorem is established mathematics; the remaining task is its complete formal proof, including the assertion that every permitted group occurs. The source is Theorem III.5.1 and its occurrence remark, printed page 156 of Modular curves and the Eisenstein ideal.
A Weierstrass curve over the rational numbers is an equation
where all five coefficients are rational. Its discriminant measures singularity. The curves in this mission have nonzero discriminant, so they are elliptic curves. The group consists of its rational points together with the distinguished point at infinity, which is the additive identity. The rational torsion subgroup is
This subgroup is formed using the actual rational-point group; it is not a separately supplied finite group or a collection of coordinate certificates.
The symbol denotes a cyclic group of order , with its additive operation. A product of two such groups has componentwise addition. An additive group isomorphism is a bijection that preserves addition. Consequently, classifying a subgroup by an isomorphism identifies its complete group structure and its number of elements, rather than only the orders of selected points.
For every elliptic curve , the torsion subgroup must be finite and isomorphic to one of
or
Conversely, for every parameter in either displayed range, there must exist an elliptic curve over whose full rational torsion subgroup is isomorphic to that group. The curve may depend on the parameter. The goal combines unconditional finiteness, classification, and all fifteen occurrence cases. The cyclic case includes curves with trivial rational torsion. Occurrence requires equality of the entire torsion group up to isomorphism; constructing an embedding or a single point of the desired order does not meet that target.
The supporting point-order milestone is Corollary III.5.2, on the same source page: every rational point of positive finite order has order in the eleven-element cyclic list. Infinite-order points are outside that milestone's hypothesis. The four other milestone clauses separate finiteness, group classification, cyclic occurrence, and bicyclic occurrence so their contributions can be reviewed individually.
The final classification theorem will be available in the standard Lean vocabulary for rational elliptic curves, finite-order subgroups, cyclic groups, products, and additive equivalences. Its main downstream consumer is the canonical classification endpoint of the MazurTheorem repository. Occurrence supplies the converse needed for an exact list of possible groups. Together these results also give a torsion-cardinality bound of sixteen and uniformly exclude rational torsion configurations outside the list.
The existing repository contains substantial checked prerequisites and reductions. A prerequisite receives credit according to its actual hypotheses, conclusion, and connection to the acceptance theorem. This campaign does not treat the full classification as already formalized, and it does not treat locally checked source as a platform-verified contribution before transfer and verification. Existing proofs should be reused with their attribution and dependency graph intact. Open definitions and unproved mathematical comparisons must remain visible as obligations.
Finite-abelian-group classification alone cannot establish which groups arise from an arbitrary rational elliptic curve. The crucial arithmetic exclusions require connecting concrete rational points with genuine arithmetic-geometric objects. A theorem about a supplied quotient or Jacobian does not construct that quotient or Jacobian; an interface that assumes a missing comparison leaves that comparison unproved. The foundational work includes represented modular curves, Jacobians and Picard functors, integral models, specialization, and the arithmetic needed to exclude prohibited point orders. These requirements reflect the mathematical source and the repository's current proof architecture.
The occurrence direction has a different verification obligation. Explicit rational points and order computations must be supplemented by a proof that the curve is nonsingular and that its entire rational torsion subgroup has precisely the claimed shape. Machine arithmetic and external tables can guide the selection of examples, but the published occurrence theorem must have a checked proof.
Curves are Mathlib's WeierstrassCurve ℚ with IsElliptic; rational points are (E⁄ℚ).Point. Torsion is AddCommGroup.torsion, the cyclic groups are the additive groups of ZMod, and isomorphisms are additive equivalences. The target definition bundle repeats the repository's fifteen-group vocabulary in a campaign namespace. A checked compatibility bridge identifies its classification predicate with the repository's canonical predicate. This definition boundary exists solely to state platform obligations faithfully; its named consumers are the campaign goal and the repository's classification endpoint.
The goal has no supplied finiteness, rank, reduction, modularity, semistability, point-order classification, or group-classification hypothesis. Finiteness is an explicit conclusion. The numerical expression Set.ncard ≤ 16 is only a corollary: Set.ncard is zero on infinite sets, so that expression alone cannot certify this mission's completion. Checked proofs must have no placeholders, custom axioms, unchecked computation, or proof-strengthening options. The permitted foundational dependencies are propext, Quot.sound, and Classical.choice; open targets are displayed separately from their eventual proofs.
The repository's execution ledger remains the source of contributor assignment. Its selected foundations are the coherent-cohomology-to-Jacobian lane and the represented-modular-curve lane. Contracts marked paused remain paused unless the maintainers explicitly revise their assignment. Platform milestones describe mathematical completion obligations, not automatic authorization to claim every repository task. Contributors can close occurrence examples, reuse checked arithmetic reductions, and advance selected foundational packages with a concrete downstream consumer. Progress must track integrated obligations rather than code volume or the number of generated statements. Licenses, source commits, original authors, and upstream notices must accompany all transferred proofs.
54d43d8dda8a6fcf069cc02a815f850d762c5c0c. Existing uncommitted changes are excluded from source-snapshot claims.Prove that subset sum is NP-complete by reducing the existing 3-SAT language, to it. Given a list of positive integers and a nonnegative target, decide whether some selection of entries sums exactly to the target. Integers are encoded in binary.
Stochastic and online subgradient methods are the workhorse of large-scale learning: each step touches one example, costs time linear in the dimension, and needs no line search. Their weak point is the step size. A single global step size treats every coordinate alike, while in high-dimensional, sparse problems (text, click-through data, bag-of-words features) most coordinates are zero in most examples, and the few informative rare features receive vanishingly small updates.
AdaGrad (Duchi, Hazan and Singer, JMLR 2011; McMahan and Streeter, COLT 2010, independently) chooses a separate step size per coordinate from the gradients observed so far. Its diagonal version is the ancestor of RMSProp and Adam and is one of the most widely used optimizers in machine learning. This mission targets the paper's regret guarantee for diagonal AdaGrad, which explains when per-coordinate adaptation pays off.
Timeline. Zinkevich (2003) proved regret for online projected gradient descent. Nesterov (2009) and Xiao (2010) analysed dual averaging with a regularizer; Duchi, Shalev-Shwartz, Singer and Tewari (2010) analysed composite mirror descent. Auer and Gentile (2000) proved the scalar inequality that makes adaptive step sizes work. Duchi, Hazan and Singer (2011) combined these into adaptive proximal functions with data-dependent regret bounds.
Work in with the Euclidean inner product and . A closed convex set with is fixed, together with a convex regularizer (for example ). In rounds a learner plays , a convex loss is revealed, and the learner observes a subgradient of at : for all . The regret against a comparator is
For each coordinate , let and . Diagonal AdaGrad (Figure 1 of the paper) has parameters , , starts at , and in round uses the proximal function . It updates by one of two rules:
For the primal-dual update with , and every ,
For the composite mirror descent update with , and every ,
Lemma 16 and Propositions 2 and 3 are stated in the paper for general proximal functions; here they are specialised to diagonal quadratic ones, .
The result. The quantity is never larger than and can be far smaller when gradients are sparse or coordinate scales differ. Theorem 5 shows that diagonal AdaGrad does as well as the best fixed diagonal preconditioner chosen in hindsight, up to a constant, without knowing the gradients in advance (Corollary 1 and Corollary 6 of the paper). Through online-to-batch conversion the same bound gives convergence rates for stochastic convex optimization with sparse data. The theorem underpins the theoretical case for per-coordinate adaptive step sizes.
Formalizing it. The result is proved on paper; to our knowledge no machine-checked proof of AdaGrad's regret bound exists, in Lean or elsewhere. The formalization produces checked versions of the two regret templates (composite mirror descent and dual averaging with changing proximal functions), which are reused by most later analyses of adaptive methods, and of the Auer–Gentile inequality. The formal statements also make precise two hypotheses the printed theorem leaves implicit (see Formalization scope).
The obvious argument fixes one proximal function and applies the classical mirror-descent or dual-averaging bound. That fails because AdaGrad's changes every round and depends on the very subgradients whose norms are being bounded: the classical bounds assume a fixed , and with changing new drift terms appear that must be shown to be small. The gradient term has denominators that grow with the data, so it is not bounded term by term; it has to be bounded as a whole sum. For dual averaging there is an additional index shift: round 's subgradient is measured in the dual norm of , which has not yet seen .
Vectors live in EuclideanSpace ℝ (Fin d), so ‖·‖ is the Euclidean norm; is a separate definition supNorm. Rounds are 1-based, with sums over Finset.Icc 1 T; . Losses and the regularizer are real-valued convex functions on all of , so extended-valued regularizers (indicator functions) are excluded, and the constraint is carried by . The subgradient relation is the published platform definition ShorNonsmooth.AlmostDiff.IsSubgradient. Each update is a predicate ( and minimizes the update objective over ), since the minimizer need not be unique; the theorems hold for every run. The factor in follows Figure 1. Dual norms use Lean's division, where is the paper's . The losses are a fixed sequence, which also covers adaptive adversaries because the run is determined by the losses.
Two restrictions relative to the printed Theorem 5, both forced by the paper's own proof:
Proposition 2 is stated with strictly positive weights. The primal-dual part of the goal with is a degenerate case in which every vanishes.
A run predicate without the subgradient link , an argmin without , a comparator outside , or computed without round would each make the statement trivial or different. The definitions rule all of these out.
Needed infrastructure: elementary convex analysis on (first-order optimality of a convex objective over a convex set), finite sums and square roots. Nothing beyond Mathlib is required. The two regret templates (Propositions 2 and 3) and inequality (24) are reusable beyond this mission. Proofs of any milestone, and of the full-matrix analogues, are welcome.
Maximum 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.
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 .
A reentrant line is a queueing network in which every job follows the same route and visits some stations more than once. It is the standard model of a semiconductor wafer fab, where a wafer returns to the same lithography station for each of its layers (Kumar, Re-entrant lines, Queueing Systems 13, 1993). Because jobs at different stages compete for the same server, a network can be unstable (queues grow without bound) even though every station has nominal load below one; the Lu–Kumar and Rybko–Stolyar examples of the early 1990s made this concrete. Deciding stability under the usual load condition therefore needs an argument specific to the network and to the scheduling policy.
Fluid models turn that question into one about deterministic dynamics. Dai (Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Ann. Appl. Probab. 5, 1995) showed that if the fluid model of a queueing discipline is stable, the queueing network under that discipline is positive Harris recurrent. Dai and Weiss (1996) then proved fluid stability, or instability, for several classes of reentrant lines. This mission formalizes their first result, about the smallest reentrant line that revisits a station after visiting another one.
Timeline:
A reentrant line has stations and classes. Fluid enters as class at rate one; class is served at station with mean service time and service rate , and on completion becomes class (class leaves). The constituency of station is , and its nominal workload is .
A fluid model solution is a pair of paths (fluid levels) and (cumulative time spent serving each class) such that, for :
each starts at and is nondecreasing, and the idle time , with busy time , is nondecreasing. These are the paper's equations (1.8)–(1.12). The solution is work conserving if, in addition, (1.13): increases only at times when station holds no fluid. The immediate volume of station is .
A set of fluid model solutions is stable (Definition 1.3) if there is a such that every solution with has for all .
The three-buffer line of Figure 1 has , and route : classes and at station , class at station . The load condition (3.1) is
The goal fixes no emptying time: it asserts only that some works, which is Definition 1.3.
Theorem 3.1 settles stability of the three-buffer line for every work-conserving discipline at once, not only FIFO. Through Dai's 1995 theorem it gives positive Harris recurrence of the queueing network under any such discipline whose fluid limits satisfy (1.8)–(1.13), under that theorem's distributional assumptions. By the paper's remark after the proof, every other three-buffer reentrant line is feedforward, so with this theorem all three-buffer reentrant lines are stable under every work-conserving policy. The method, a Lyapunov function that is the maximum of linear functions of the fluid levels, recurs in the paper's later theorems (Lu–Kumar network, two-station Kelly-type lines) and in the wider fluid-stability literature.
The result is proved on paper; no machine-checked version exists. The mission's contribution is a formal fluid-model layer for reentrant lines (equations (1.8)–(1.13), Definition 1.3) shared with the other missions of this series, two reusable real-analysis lemmas (Lemma 2.2 (ii) and Lemma 3.2), and a complete formal proof of Theorem 3.1. The fluid-limit theorem linking fluid stability to the stochastic network is cited, not formalized.
The obvious approach is to split cases on the relative loads, as the paper notes ( or not), and track the fluid explicitly; this gives sharp emptying times but requires following solutions through regime changes, which is unwieldy when the discipline is arbitrary. The Lyapunov approach avoids this but moves the difficulty into analysis: the fluid paths are only Lipschitz, so derivatives exist only almost everywhere; the maximum of two Lyapunov components is not differentiable where they cross; and work conservation is a statement about where the idle time can increase, which has to be converted into "the busy time grows at rate one" at points where a station holds fluid. Lemma 2.2 (ii) itself needs the fundamental theorem of calculus for absolutely continuous functions.
All declarations live in DaiWeissFluid.ThreeBuffer. Committed conventions:
Fin 3, Fin 2). The paper's class is Lean k - 1; the line is threeBuffer m with station map ![0, 1, 0], and (3.1) reads m 0 + m 2 < 1, m 1 < 1.ℝ → Fin K → ℝ; every equation is imposed only for , and derivatives are taken at (HasDerivAt).A trivializing formalization is ruled out: the work-conserving solution set of the three-buffer line is nonempty for every satisfying (3.1), with (a sorry-free witness was checked), so the goal is not vacuous, and the goal quantifies over all work-conserving solutions rather than one discipline.
Needed infrastructure: Lipschitz and absolute continuity of the fluid paths, the a.e. fundamental theorem of calculus for absolutely continuous functions (in Mathlib), and the derivative of a finite maximum at a regular point (on the platform as display (3.2)). Lemma 2.2 (ii) and Lemma 3.2 are reusable for the other missions of the series. Proofs of any milestone are welcome independently.
Many optimization problems in statistics, machine learning and operations research ask to minimize a smooth convex function over a simple convex set: a box, a ball, a simplex, a cone of positive semidefinite matrices. Projected gradient descent is the most basic first-order method for such problems. It takes a gradient step and then returns to the feasible set by Euclidean projection. Its cost per iteration is one gradient evaluation and one projection, independent of the dimension apart from the cost of manipulating vectors, which is why it remains a workhorse in very high dimension.
This mission is the fifth in a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015; arXiv:1405.4980). Chapter 3 of the monograph treats "dimension-free" convex optimization. Its §3.2 first proves that gradient descent on a convex -smooth function on has rate (Theorem 3.3, the subject of mission IV), and then turns to the constrained case, which is the subject of this mission. The analysis follows Nesterov's Introductory Lectures on Convex Optimization (2004).
Write for the Euclidean inner product on and for the Euclidean norm. The constraint set is compact and convex; this is the standing assumption of Chapter 3. The Euclidean projection of onto is
which exists and is unique for a nonempty closed convex set.
A differentiable function is -smooth on if its gradient is -Lipschitz there:
It is -strongly convex on if for . A minimizer of over is assumed to exist, as everywhere in the monograph.
Projected gradient descent with step size starts at and iterates
For a point with projected step , the gradient mapping is . Without constraints it equals .
For convex and -smooth on , projected gradient descent with satisfies, for every ,
If is in addition -strongly convex on , with condition number , then the strengthened Lemma 3.6, display (3.14), gives for every
Theorem 3.7 shows that a constraint set with a cheap projection costs nothing in the order of convergence: the rate of unconstrained gradient descent survives, with a constant that depends on . Lemma 3.6 is the reusable part. It isolates the gradient mapping as the quantity that measures progress under constraints, and the same inequality, with a strong-convexity term added, gives the linear rate of Theorem 3.10. It is also the starting point of the analysis of proximal gradient methods for composite objectives.
All of these results are classical and proved in the textbook. As far as a search of the platform shows, none of them is formalized there. A related platform theorem on constrained gradient descent for well-conditioned functions (from Hazan's Introduction to Online Convex Optimization) bounds function values with a different exponent. It is not Theorem 3.10, which bounds distances with rate . This mission adds machine-checked statements of the constrained analysis in Bubeck's formulation, with the book's constants. The definitions of -smoothness on a set, the gradient mapping and the run predicate can be reused by later missions on accelerated and proximal methods.
The obvious attempt is to copy the unconstrained proof, which rests on the descent inequality . That inequality fails under constraints: the projection can cut the step short, so the decrease in is not controlled by . At a boundary minimizer, for instance, while no step makes progress. The proof has to replace the gradient by the gradient mapping throughout. It also has to show separately that the iterates do not move away from , a fact that came for free without constraints from co-coercivity of the gradient (display (3.6)).
The closing induction is not routine either. The step from to works only from on, and the step from to needs a direct computation that uses the term in the numerator.
EuclideanSpace ℝ (Fin n), and is ⟪x, y⟫_ℝ.IsCompact X) and convex (Convex ℝ X), the standing assumption of Chapter 3. Every statement about a run assumes a minimizer with for all , the monograph's standing assumption.g with HasGradientAt f (g x) x at every point of , so is defined at boundary points of . -smoothness on (IsBetaSmoothOn X f g β) asks this together with and the Lipschitz bound on only. It is not the quadratic upper bound (3.4), which is a consequence.OnlineConvexOpt.ConvexBasics.StronglyConvexOn X f g α, which is display (3.13) with the same gradient map. Display (3.14) and Theorem 3.10 use .IsMetricProjection X y p: and for every . No choice function is used.IsProjGDRun X g β x: , , and for every the iterate is a projection of . Indices start at as in the book, and x 0 is unused.gradMap β x xplus takes the projected point of the run as an argument.Contributions are welcome on any milestone. Lemma 3.1 and (3.7) need only the variational characterization of the projection. Lemma 3.6 needs the quadratic upper bound for a function whose gradient is Lipschitz on a convex set, together with the first-order characterization of convexity relative to a set. Both are of independent use. The induction milestone is a self-contained statement about real sequences.
Many convex optimization problems in machine learning and statistics have objectives that are convex but not differentiable: hinge losses, penalties, maxima of finitely many affine functions, and the dual functions of Lagrangian relaxations. Methods that rely on gradients do not apply to them directly, while cutting-plane methods such as the ellipsoid method pay a price that grows with the dimension. The projected subgradient method replaces the gradient by an arbitrary subgradient and restores feasibility by a Euclidean projection. Its guarantee depends on the dimension only through two constants, a radius and a Lipschitz constant . This is the reason it, and its descendants (mirror descent, stochastic gradient descent, online gradient descent), are the standard tools for large-scale nonsmooth problems.
The rate analysed here goes back to the subgradient methods of Shor and Polyak in the 1960s and 1970s and to the lower bounds of Nemirovski and Yudin (1983). The book follows the presentation of Nesterov, Introductory Lectures on Convex Optimization (2004). The strongly convex variant with weights proportional to is from Lacoste-Julien, Schmidt and Bach (2012).
This mission is the third of a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015), and covers the preamble of Chapter 3, Section 3.1 and Section 3.4.1.
Let carry the Euclidean inner product and norm . Let be compact and convex, and let be a convex function on with a minimizer .
A vector is a subgradient of at if for every . The set of subgradients at is written . The projection of a point is the point of nearest to .
Fix step sizes . Projected subgradient descent starts at some and iterates, for ,
Any subgradient may be chosen at each step. In Section 3.1 the step is constant, . The set lies in the Euclidean ball of radius centred at , and the subgradients have norm at most .
A function is -strongly convex on if for all and .
For every horizon , projected subgradient descent with the constant step satisfies
If is -strongly convex and its subgradients are bounded by , then with ,
Theorem 3.2 gives an oracle complexity of for reaching an -optimal point, independent of the ambient dimension. Section 3.5 of the book shows this rate is unimprovable for black-box first-order methods once the dimension is large. Theorem 3.9 shows how strong convexity improves the rate to , with the averaging weights changed from uniform to linear. These two bounds are the reference points against which the rest of Chapter 3 and Chapters 4 to 6 (smooth, accelerated, mirror, stochastic methods) are measured.
The results are classical and their proofs are short. Formalizing them produces a reusable, machine-checked account of the basic projected first-order step: the projection inequality, the one-step distance recursion, and the telescoping argument with Jensen's inequality for averaged iterates. To our knowledge, no machine-checked proof of the averaged-iterate bound for the projected subgradient method exists in Mathlib. Related platform items cover other algorithms or other averaging schemes.
The arithmetic is elementary, and the obvious argument works. The care is in the bookkeeping. The projection must be shown not to increase the distance to , which needs convexity of and the variational characterization of the nearest point. The sum must telescope with a horizon-dependent constant step. Jensen's inequality must be applied to a finite convex combination of points of , which requires showing that the average lies in . In Theorem 3.9 the step sizes and the averaging weights are coupled, so neither can be changed independently. In Lean, the iterates are indexed from with natural-number horizons, and the bounds involve , so these casts need care.
is EuclideanSpace ℝ (Fin n). The iterates are sequences ℕ → EuclideanSpace ℝ (Fin n) with the first iterate at index . The projection is the published relation OnlineConvexOpt.FirstOrder.IsMetricProjection ( is a nearest point to ). Subgradients are taken relative to (Definition 1.2). A run is a predicate on the steps , and every theorem holds for all runs, that is, for every choice of subgradients. Compactness and convexity of , convexity of on and the existence of the minimizer are the book's standing assumptions and appear as hypotheses. , and are explicit, because Lean's division by zero would otherwise turn the step size into a junk value.
The book assumes for every subgradient at every point of . With subgradients relative to a compact , that assumption can never hold at a boundary point, since every outward normal can be added to a subgradient. Stated that way the theorems would be vacuous. The mission therefore assumes the bound only for the subgradients that the run uses. This is a weaker hypothesis and gives a stronger, non-vacuous statement. Bounding only these subgradients is a deliberate choice, not a trivialization: the bound still constrains every quantity the conclusion depends on.
Contributions welcome: proofs of the four inequalities and of the two rates, and a reusable lemma that the convex combination of finitely many points of a convex set lies in the set, together with Jensen's inequality in the form used here.
Black-box convex optimization asks how many queries to an oracle are needed to minimize a convex function to accuracy . In fixed dimension the answer is of order , and the first algorithm to attain it is the center of gravity method, discovered independently by Levin (1965) and Newman (1965). It is the opening example of cutting plane methods: algorithms that keep a set known to contain a minimizer and shrink it with one half-space per oracle call. The ellipsoid method and Vaidya's method, which underlie the polynomial-time solvability of linear programming and convex feasibility problems, follow the same template with cheaper sets. This mission is the first of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (2015), and covers its §2.1.
Timeline:
Let be a convex body: a compact convex set with non-empty interior. Let be continuous and convex, and let be a minimizer of on . A vector is a subgradient of at if for every . The first order oracle returns, at a query point, some subgradient there; the zeroth order oracle returns the value of .
For a set of finite positive volume, its center of gravity is
The center of gravity method sets and, for , computes , queries the first order oracle at to obtain a subgradient , and sets
After steps it outputs , found with calls to the zeroth order oracle.
The Lean development names these objects IsConvexBody, IsSubgradientOn, centroid and IsCenterOfGravityRun in the namespace ConvexOptAlg.CenterGravity.
For every run of the method and every ,
Theorem 2.1 is a linear rate whose number of queries to reach accuracy , , depends on the dimension only linearly and on the accuracy only logarithmically, and matches the Nemirovski–Yudin lower bound. It is the reference point against which the ellipsoid method ( queries) and Vaidya's method are measured, and the randomized center of gravity method of §6.7 of the book rests on the same analysis. Grünbaum's inequality is a basic fact of convex geometry with uses well beyond optimization, for instance in the analysis of query complexity and of approximate centroid computations by random walks.
On the formal side, the theorem has been proved since 1965 and the lemma since 1960; neither is known to have a machine-checked proof. A complete development adds to Mathlib-based libraries the center of gravity of a set, the volume of homothetic images in the form used here, Grünbaum's inequality, and a reusable predicate for cutting plane runs. The later missions of this series (the ellipsoid method in particular) reuse the shrunk-copy argument of milestones 4 and 5.
The steps (2.2), the shrunk-copy volume and the value bound are short. The volume decay and the final comparison are bookkeeping once one knows that each cut keeps the method's sets convex bodies with positive volume. The difficulty is Lemma 2.2. A half-space through the centroid need not split the volume evenly: for a cone the smaller side tends to of the volume as , so no symmetry argument works, and the bound must hold uniformly in the dimension. The classical proofs rely on tools of convex geometry, such as volume comparisons between a body and a symmetrized body, that are not available in Lean in the needed form. A second source of work is that the method's sets are defined through centroids: it has to be shown that they remain convex bodies of positive volume, so that each centroid is the genuine center of gravity, and this fact is not available before the volume estimates are.
is EuclideanSpace ℝ (Fin n) with Lebesgue measure volume; volumes are kept in in every statement. The function is a total map f : EuclideanSpace ℝ (Fin n) → ℝ with , continuity and convexity required on only; its values off are irrelevant. Subgradients are relative to (Definition 1.2). A run is a predicate on sequences indexed from ; the oracle's choice of subgradient is free, and every theorem holds for all runs. The minimizer is a hypothesis, as in the book's standing notation; it exists here by compactness. The output is any argmin, so the goal bounds the minimum .
Added hypotheses, all disclosed in the statements: in the goal, because the exponent is undefined for ; and in Lemma 2.2, that the centered set is a convex body, because in Lean the integral of a non-integrable function is , which would make every unbounded convex set "centered". The milestone on volume decay assumes , which is the book's own reduction.
The center of gravity is defined with the real volume and is meaningless when that volume is or infinite. The run predicate does not assume the volumes are positive; that every set of a run is a convex body of positive volume is part of what has to be proved, and a formalization in which runs could degenerate to sets of zero volume, or in which the centroid is an arbitrary point, is not the book's method.
Contributions welcome: proofs of any item; a general Grünbaum inequality for convex sets of finite positive volume; lemmas on centroids (membership in the closed convex hull, translation behaviour) that later missions can reuse.
The vertices and edges of a convex polytope form a graph, and much of polyhedral combinatorics and of the theory of the simplex method is about that graph: how far apart two vertices can be (the Hirsch question), which graphs arise (Steinitz's theorem in dimension 3), and how robust the graph is. In 1961 M. L. Balinski proved that the graph of a full-dimensional polytope in -space cannot be disconnected by deleting fewer than vertices (Pacific J. Math. 11 (1961) 431–434). The result, now called Balinski's theorem, is a standard entry in textbooks on polytopes (Grünbaum, Convex Polytopes, §11.3; Ziegler, Lectures on Polytopes, Thm 3.14) and is the starting point of the study of connectivity of polytope graphs. Its proof uses only linear programming: the improving-edge step of the simplex method and the connectivity of the graph of a face.
Timeline. Steinitz (1922) characterised the graphs of 3-polytopes as the 3-connected planar graphs, so the case is contained in his theorem. Balinski (1961) proved -connectivity in every dimension. Whitney (1932) had shown that -connectivity is equivalent to the existence of disjoint paths between any two points; Balinski gives a new proof of that equivalence through max-flow min-cut and draws the corollary that any two vertices of a full-dimensional polytope in are joined by disjoint edge paths.
Fix integers (the dimension of the space) and (the number of inequalities), vectors (the rows of a matrix ) and . Balinski's system (1) describes
written Hirsch.Hpoly a b in Lean. The paper assumes throughout two standing assumptions (StandingAssumptions a b):
A vertex of is an extreme point. An edge is a segment , , that is an extreme subset of (Hirsch.Adj S u v). The graph (polyGraph S) has the vertices as points and the edges as lines.
A graph is -tuply connected (IsNTuplyConnected G n) if it has at least points and remains connected after dropping out any or fewer points. Two points are joined by disjoint paths (HasDisjointPaths G u v n) if there are distinct paths from to which share no point other than and .
That is, and is connected for every set of at most vertices.
Hirsch.face_connected.The result. Balinski's theorem says that polytope graphs are highly connected, which constrains which graphs can be graphs of -polytopes and is the base case of later results on the connectivity of polytope graphs. Together with Whitney's theorem it gives vertex-disjoint edge paths between any two vertices. The improving-neighbour step is the local optimality criterion of the simplex method.
Formalizing it. The theorem is classical and proved; it has not been formalized. On this platform the case (the graph of a polytope is connected) is proved as Hirsch.graph_connected_general, and connectivity of the graph of each face as Hirsch.face_connected, both by Shuze Chen; LinearOptimization.polyhedron_bounded_convex_hull_extreme proves the convex-hull clause of milestone 1 for a matrix-form polyhedron under the hypotheses "nonempty and bounded", and ConnPreservingHamPath.IsKConnected.le_ncard_neighborSet proves "connectivity at most minimum degree" for its own notion of -connectivity. This mission adds vertex -connectivity in every dimension, the simplex improving-neighbour lemma for H-polytopes, and the corollary on disjoint paths. The corollary needs Whitney's theorem, which is the goal of the companion mission On the Graph Structure of Convex Polyhedra in n-Space II.
An induction on dimension through facets does not directly control where the deleted vertices lie. Balinski's argument leans on several facts the paper calls obvious or clear: that a vertex with no improving neighbour is optimal, that the graph of a face is connected, that points of lie on a common hyperplane while does not, and that has at least vertices. Each needs its own development from the two algebraic assumptions, in particular the passage from (i)–(ii) to a bounded full-dimensional polytope with finitely many vertices, and the identification of extreme segments with edges. Deleting fewer than vertices, which the definition requires and the proof's text does not treat, needs a separate argument. The proof also tacitly needs the affine function to take a nonzero value at some vertex.
EuclideanSpace ℝ (Fin n); rows a : Fin m → EuclideanSpace ℝ (Fin n), b : Fin m → ℝ. The published Hirsch_model names the dimension d and the number of rows n; here is the dimension, as in the paper.Set.extremePoints ℝ S; edges are Hirsch.Adj (extreme segments). is a SimpleGraph on the vertex subtype.Set.encard; " or fewer points" is X.encard < n. A path of the paper is a Mathlib Walk (consecutive points distinct).Hirsch.face_connected; the affine function of the proof is an arbitrary , and only the "maximum"/"" forms are stated (the others follow for ); "at least disjoint paths between any pair of vertices" is a family of pairwise distinct paths without repeated points, sharing only their endpoints, between two distinct vertices.Hirsch walk vocabulary and Mathlib Walks; all are reusable beyond this mission.In robust optimization, a constraint is checked against every parameter value in an uncertainty set. This turns uncertainty into a deterministic optimization problem, but the set must be chosen carefully: a large set can make decisions unnecessarily conservative, while a small one can miss likely outcomes. Bertsimas, Gupta and Kallus use data to calibrate sets through statistical confidence regions. Their question is whether feasibility for every parameter in the set protects a decision against a fresh uncertain outcome with a specified probability. This mission treats the part of their construction based on estimated first and second moments. Bertsimas, Gupta and Kallus, §8.1.
The moment region originates in a concentration result attributed in the paper to Shawe-Taylor and Cristianini. That result bounds the distance between sample and population means and covariances when the uncertain vector is supported in a Euclidean ball. Bertsimas, Gupta and Kallus also discuss replacing those analytic thresholds with bootstrap thresholds; they describe the resulting coverage as approximate. The present target concerns the mathematical relation between a fixed moment region and its uncertainty set, leaving the statistical calibration of the thresholds to its cited source. Shawe-Taylor and Cristianini, 2003; Bertsimas, Gupta and Kallus, pp. 24–25.
Let the uncertain vector take values in . A probability law belongs to the moment confidence region when it is supported in the Euclidean ball of radius , its mean is within of an estimate , and its covariance is within of an estimate in Frobenius norm. The covariance is . The thresholds are nonnegative and can be chosen by either calibration procedure discussed in the paper. Bertsimas, Gupta and Kallus, Theorem 9 and (33).
For a vector , Value at Risk is the smallest threshold for which . The support function of a set is . The authors construct the set
Here is the allowed violation probability, is the identity matrix, and is a matrix factor of the adjusted covariance. The estimates and stay fixed while varies. Bertsimas, Gupta and Kallus, (34)–(35).
The first milestone bounds the quantile for every law in the moment region:
The second milestone evaluates the two linear maxima over the Euclidean balls in and identifies with the quadratic form above. The goal, the deterministic part of Theorem 10, says the displayed bound equals for every , while the set is nonempty, convex and compact. This gives the support-function criterion of Theorem 1 for each law in the region. A companion formalizes Theorem 13(a): the resulting support constraint is separately convex in and in for . Bertsimas, Gupta and Kallus, Theorems 10 and 13(a).
The support formula turns a distributional statement about an entire region of probability laws into a deterministic bound on a linear projection. It gives the robust model an explicit quantity to compare with a constraint threshold. The companion convexity result describes which risk levels allow separate convex optimization in the decision variables and the violation probability. Together they explain why the particular set in (35) is useful beyond the fact that it contains plausible uncertain vectors. Bertsimas, Gupta and Kallus, §§8.1 and 9.
The paper proves the mathematical construction and cites statistical results for the region's coverage. In Lean, the published Value-at-Risk and support-function definitions are already available, while this paper's moment region and set (35) need their own definitions. Formalizing the result therefore establishes a reusable interface between moment bounds, quantiles and set support. The theorem statements in this proposal are open proof targets; compiling them checks their types, not their proofs.
A bound on the mean and covariance does not directly bound a high quantile of every projection. The bound must work simultaneously for every probability law in the moment region, including discrete laws and singular covariances. The factor is essential: replacing it by a standard deviation or a Gaussian quantile would change the claim. On the set side, the ordinary norm of a Lean function vector is a sup norm, whereas both balls in (35) are Euclidean. Getting the norm wrong changes the support function. Bertsimas, Gupta and Kallus, (34)–(35).
Vectors are functions on Fin d, whose coordinates start at zero. enorm and frob explicitly compute the Euclidean and Frobenius norms. The ball-support condition in secures finite first and second moments; no density is assumed. The goal fixes , , , and . This factor relation makes the quadratic form nonnegative; a separate positive-semidefinite assumption on is unnecessary. The matrix need not be triangular because (35) and its support depend on . The uncertainty set's nonemptiness and compactness appear in the goal so the real support-function supremum cannot take Lean's default value for an empty or unbounded set.
Theorem 10's sampling claim is represented by its deterministic criterion for each . The confidence-region coverage of Theorem 9 is cited, and the bootstrap coverage discussed on p. 25 is approximate; neither is asserted as an exact probability theorem here. Equation (34) prints an equality for a supremum over , yet that region restricts support to a ball, and the page does not establish attainment under that restriction. This mission uses the upper-bound direction needed for Theorem 10 and does not assert the equality or Remark 16's exact equivalence. The scope includes a sharp quantile bound, the exact support formula and the convexity range; a definition that merely makes the claim true by construction would miss these targets. Bertsimas, Gupta and Kallus, pp. 24–25 and 29.
A robust linear constraint with ranging over an uncertainty set is tractable whenever the support function is. Robust optimization gains a probabilistic meaning when is chosen so that every robustly feasible decision also satisfies the constraint with probability at least under the true distribution of the uncertain parameter . Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167, 2018) build such sets from data: a statistical hypothesis test yields a confidence region of distributions, and the uncertainty set is any convex set whose support function dominates the worst-case Value at Risk over .
Section 5.2 of the paper applies this schema to the forward and backward deviations of Chen, Sim and Sun (Oper. Res. 55, 2007), one-sided measures of spread that capture skewness. Chen, Sim and Sun assume the mean and deviations are known; the data-driven version replaces them by confidence intervals and must work out the worst case over those intervals. The result is the set of Theorem 6, whose support function has a closed form.
The uncertain parameter takes values in and is its law. For and , the Value at Risk is
For a probability measure on with mean , the forward deviation and the backward deviation are
From a sample, a bootstrap produces thresholds , , . With the sample mean put and . The confidence region consists of the distributions of vectors with independent components , each having bounded support, mean in , and .
The uncertainty set is
For , and , the set is nonempty, convex and compact,
for every , and is at most the right-hand side of (24) for every and every .
Theorem 6 gives a data-driven uncertainty set for which a robust linear constraint is a second-order cone constraint, (24) being an explicit norm expression. By Theorem 1 of the paper, the domination of the worst-case Value at Risk over the region by the support function means that every robustly feasible solution satisfies a chance constraint at level for every distribution in the region. Unlike the Chen–Sim–Sun set, which requires the true mean and deviations, needs only data and allows the mean and the support to be unknown. Theorem 13(b) supports the alternating heuristic of §9 for choosing the levels across several constraints.
The paper's proof is short and leans on "by inspection" and "by Lagrangian strong duality". A formal development makes each of these steps explicit, including the case where the multiplier is not attained, and corrects two printed slips (the optimal values , which should be , and the bound ). The Chen–Sim–Sun bound itself, a Chernoff-type tail bound under one-sided moment-generating conditions, is cited by the paper without proof. None of these results has a machine-checked proof that this mission is aware of.
The support function of (23) is a maximisation over a set defined by a box, two nonnegative orthants and one coupled quadratic constraint. A coordinate-wise argument does not apply directly because the quadratic budget is shared. The worst case over is not a single distribution: the extreme mean and the extreme deviations are chosen coordinate by coordinate according to the sign of . The Value at Risk bound needs independence of the components; without it (22) fails. When or the sign pattern makes the quadratic term vanish, the dual multiplier escapes to zero and the dual minimum is only an infimum.
Vectors are Fin d → ℝ, with 0-based coordinates; is u ⬝ᵥ v. The Value at Risk is the published MultistageStochastic.valueAtRisk at level , and the support function is the published RobustMDP.Shared.supportFunction, a real supremum; the goal includes nonemptiness and compactness of , so the supremum is a true maximum and cannot hold through the value of an empty or unbounded set.
The statement is formalized in the criterion form: for all and every in the region. By Theorem 1 (mission I of this series), for a nonempty convex compact set this criterion is equivalent to the probabilistic guarantee. The page's "with probability with respect to the sample" is the coverage of the bootstrap confidence region, which the paper itself treats as approximate; it is not formalized.
Conventions and added hypotheses:
IsGLB.A trivializing formalization is ruled out: a region without independence would make the goal false, a region without the probability and bounded-support conditions would let junk integrals satisfy the deviation predicates, and a support function of an empty set would make (24) a statement about .
The development needs a Chernoff argument for products of measures, finite-dimensional Lagrangian duality for one convex quadratic constraint (or a direct Cauchy–Schwarz argument), and compactness of the set (23). The definitions file is self-contained and reusable for other forward/backward-deviation sets. Proofs of any milestone, and of the Chen–Sim–Sun bound as a standalone tail inequality, are welcome.
Robust optimization replaces uncertain data by a set of possible values and requires a decision to work for every value in that set. A central question is how to choose the set from data so that robust feasibility also gives a specified chance of satisfying the original constraint. Bertsimas, Gupta, and Kallus study this question for several sampling models in Data-Driven Robust Optimization. Their finite-support construction addresses a practical case: the uncertain vector can take one of finitely many known outcomes, while their probabilities must be inferred from observations. The resulting sets use classical goodness-of-fit tests to account for uncertainty in those probabilities. Bertsimas, Gupta, and Kallus, §§2–4, pp. 2–13.
In this case the support vectors are known in advance, so the problem is not to discover which outcomes are possible. The question is how much confidence to place in their estimated frequencies and how to turn that confidence region into a set of uncertain vectors suitable for a robust constraint. The paper gives two answers, one based on Pearson's chi-square statistic and one based on the likelihood-ratio, or G, statistic. Both answers are meant to work at every requested risk level for the same observed sample. Bertsimas, Gupta, and Kallus, Theorem 4, p. 13.
Let be the listed possible outcomes. A probability vector belongs to the simplex when all are nonnegative and . It determines the finite-support law . From a sample one obtains the empirical frequencies . A nonnegative number records the test threshold; in the paper it is , where is sample size and is the test's significance level. Bertsimas, Gupta, and Kallus, (10), p. 12.
The Pearson confidence region contains candidates satisfying . The G confidence region instead requires , with relative entropy . In either region, a candidate is excluded when : the source's divergence is then infinite. If both entries are zero, that coordinate contributes zero. These conventions matter because ordinary real division and logarithm in Lean have total values at zero. Bertsimas, Gupta, and Kallus, (10), p. 12.
For a direction , value at risk is the lower quantile of the scalar loss . Conditional value at risk is the minimum over real of . The paper's auxiliary set reweights the outcomes with another probability vector constrained by . The two data-driven uncertainty sets and allow such a reweighting for some in the corresponding confidence region. Their support function is the largest over . Bertsimas, Gupta, and Kallus, (11)–(13), pp. 12–13; Theorem EC.1, p. ec2.
The first target is the paper's finite-support CVaR identity and the comparison between the two risk measures:
The goal is Theorem 4's deterministic claim, simultaneously for all . For each in the relevant confidence region, it asks for both bounds
for every , with each uncertainty set nonempty, convex, and compact. A supporting milestone identifies each support function as the supremum of CVaR over its confidence region. The paper also displays conic optimization programs for these support functions in (14) and (15); those programs are outside this mission's drafted statements. Bertsimas, Gupta, and Kallus, Theorem 4, p. 13; proof, p. ec2.
The bounds give a way to certify the directional risk of every candidate distribution accepted by a goodness-of-fit test. For a nonempty convex compact uncertainty set, the paper's Theorem 1 turns this directional condition into a probabilistic guarantee for every constraint concave in the uncertain vector. Theorem 4 adds the sampling claim through coverage of the confidence region: when the true finite-support distribution belongs to that region, the whole family indexed by receives the guarantee. The statistical tests use chi-square approximations, so their advertised coverage is asymptotic rather than an exact finite-sample result. Bertsimas, Gupta, and Kallus, Theorems 1–4, pp. 10–13.
The paper proves the mathematical result. This mission asks for machine-checked proofs of its finite-dimensional definitions, the CVaR identity, the worst-case support identities, and the deterministic risk bounds. The drafted Lean statements are open goals. A completed development would also give reusable facts about finite-support risk measures and support functions under divergence-constrained probabilities. It would leave the test coverage calculation and the explicit programs (14)–(15) for separate work.
The risk comparison alone does not identify a robust uncertainty set: the support function must agree with the worst-case CVaR over an entire region of probability vectors. This brings a finite-dimensional optimization identity into the formal proof, including attainment and the relationship between reweightings and distributions. Boundary coordinates create another difficulty. The Pearson expression divides by , and the G expression contains ; silently accepting Lean's values at zero would enlarge the regions and change the theorem. The support function and CVaR are real infima or suprema, so their nonempty, bounded domains must also be established. Bertsimas, Gupta, and Kallus, (10)–(13), pp. 12–13; proof, p. ec2.
Lean represents outcomes and probability vectors as functions on Fin d and Fin n; indices start at zero. The simplex is Mathlib's stdSimplex. The law is a finite sum of point masses. If two listed vectors coincide, their point masses aggregate; the paper's notation is recovered with the intended distinct listing. Value at risk and the support function reuse published Prove2Me definitions; the finite-vector relative entropy also reuses a published definition, guarded at zero in this mission's G region. CVaR uses a real sInf, equal to the paper's minimum for a simplex law and . No statement applies it outside that domain.
The goal assumes and . These express, respectively, that the center is an empirical probability vector and that the chi-square threshold is nonnegative. It quantifies over every , with the same confidence regions for all levels. The paper's sample size, chi-square quantile, and significance level are compressed into ; coverage of the true distribution by the test is a separate statistical premise and is not formalized here. The source's is represented by for a supported probability vector . The draft does not treat an arbitrary unsupported law as a member of the confidence region.
The nonempty and compact conclusions rule out a zero returned by a support function on an empty or unbounded set. The zero-denominator guards rule out candidates the paper assigns infinite divergence. Contributions needed to close the mission include finite-simplex geometry, the finite-support CVaR identity, continuity of the divergence regions at boundary coordinates, and the risk-bound theorem. Those facts can be reused in later data-driven robust optimization developments.
Robust optimization replaces an uncertain constraint , whose parameter is random, by the requirement that the constraint hold for every in a chosen uncertainty set :
The resulting problem is deterministic and, for many shapes of , tractable (Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization, 2009). The modelling question it leaves open is how to choose . A set that is too large makes every solution conservative; a set that is too small gives no protection. The practitioner's real requirement is usually probabilistic: a robust feasible should violate the uncertain constraint with probability at most .
Bertsimas, Gupta and Kallus (Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167, 2018) build uncertainty sets directly from data so that this requirement holds with high confidence. Their whole construction rests on one characterization, Theorem 1 of the paper, of when a set carries such a guarantee. This mission formalizes that characterization and the two results (Theorems 2 and 3) that turn it into a data-driven recipe.
Earlier work used the "if" direction of the characterization for bi-affine constraints when designing sets for specific distributional assumptions (Ben-Tal et al., 2009; Chen, Sim and Sun, Oper. Res. 55, 2007). The extension to every constraint concave in is due to Bertsimas, Gupta and Kallus.
Let be a probability measure on , the law of , and fix a level . Throughout, is concave in for every value of the decision variable .
The support function of a set is
The Value at Risk of the linear loss at level is
A set implies a probabilistic guarantee at level for (property (P2) of the paper) if for every , every concave in for each , and every ,
A function is bi-affine if it has the form .
In the data-driven setting, is unknown and a sample is drawn i.i.d. from it. The paper's schema fixes , takes the confidence region of a hypothesis test at level , and builds a closed convex set whose support function bounds for every and every .
(a) If is nonempty, convex and compact and
then implies a probabilistic guarantee at level for .
(b) If is nonempty and for some at which is finite, then some bi-affine violates (2).
The proof in the electronic companion (EC.1.1) is a short chain, and its steps are the milestones: the attainment property of VaR, (already proved on the platform); a strict separating hyperplane between and the superlevel set ; the bound for ; its limit ; and, for part (b), the witness at .
Theorem 2: with probability at least over the sample, implies a probabilistic guarantee at level for . Theorem 3: if the region does not depend on , then with probability at least the whole family implies the guarantee simultaneously (a), and every satisfying the level-optimized constraints (9) satisfies the joint chance constraint
(b).
Theorem 1(a) is what certifies every uncertainty set in the paper: the and sets for discrete distributions, the Kolmogorov–Smirnov and forward–backward sets for independent marginals, the marginal-sample box and the moment sets. Each construction reduces to proving one inequality between a support function and a Value at Risk, which is a statement about a single linear functional, and Theorem 1(a) lifts it to every concave constraint at once. Part (b) shows the condition cannot be dropped even for bi-affine constraints. Theorems 2 and 3 separate the statistical input (coverage of a confidence region) from the convex-analytic input (the support-function bound), and Theorem 3(b) is what allows the levels of a system of constraints to be optimized after seeing the data.
The results are proved in the paper. None of them has a machine-checked proof; the only formalized ingredient is the attainment property of VaR, which is on the platform as a proved theorem. The formalization provides a checked bridge from support-function bounds to probabilistic guarantees that the other missions of this series (II–VI) use to state their own results in the criterion form .
The informal argument is short; the difficulty is in the infinite-dimensional bookkeeping that the page leaves implicit. The superlevel set need not be bounded, so the strict separation must use compactness of alone. Closedness of this set and measurability of depend on concave functions on being continuous. The passage is continuity of a measure along an increasing union. The attainment of the infimum in the definition of VaR requires right-continuity of distribution functions. A naive attempt to separate from the zero superlevel set directly fails, because the two sets may touch.
is Fin d → ℝ; is the identity map; is the dot product u ⬝ᵥ v. The Value at Risk is the published MultistageStochastic.valueAtRisk at level , and the support function is the published RobustMDP.Shared.supportFunction. Both are real-valued sInf/sSup, which return on empty or unbounded sets, so every statement assumes , a probability measure, and an uncertainty set that is nonempty and compact (Theorem 1(a), Theorems 2–3) or nonempty with bounded above in the direction considered (Theorem 1(b)). In Theorem 1(b) and its witness this is the paper's own requirement that be finite, which its strict inequality with a real VaR forces and its proof uses by treating as a real number. Part (b) is printed with , a slip for ; the proof's separation step prints both inequalities in the same direction, a slip corrected in the strict separation milestone.
Property (P2) quantifies over the dimension of the decision variable, every function concave in for each , and every . Restricting it to affine or to would trivialize part (a) and falsify part (b), and is ruled out by the definition.
In Theorems 2 and 3 the sample is Fin N → (Fin d → ℝ) with the product law Measure.pi; the confidence region and the uncertainty set are arbitrary maps of the sample, and the coverage is a hypothesis, never the conclusion's event. Step 2 of the schema is stated with directly. The sets are assumed nonempty and compact (Step 3 says closed and convex; a finite support function that bounds VaR forces nonemptiness and boundedness). Theorem 3(b) reads the levels in , where the family is defined. Probabilities of events in the sample space are outer measures, so no measurability hypotheses are needed.
A complete development needs strict separation of a compact convex set from a closed convex set (Mathlib's geometric_hahn_banach_compact_closed), continuity of concave functions on finite-dimensional spaces, and the attainment property of VaR. Contributions are welcome on all milestones; the separation and limit steps are reusable for any chance-constraint argument based on support functions.
Two-stage adaptive optimization models decisions taken in two steps: a first-stage decision is fixed before an uncertain right-hand side is revealed, and a second-stage recourse is chosen afterwards, with the worst case over an uncertainty set to be minimized. The fully-adaptable problem, in which may be an arbitrary function of , is intractable in general. The standard tractable restriction, introduced by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004), requires to be an affine policy ; it turns the problem into a single convex program and is used throughout robust inventory, network design and energy planning.
How much is lost by this restriction? Bertsimas and Goyal (Math. Program. 2012) answer the question for problems with a nonnegative constraint matrix. On one side, affine policies are optimal when is a simplex, and are within a factor of the optimum on every instance of the class, where is the number of constraints. On the other side, the bound is nearly tight: Section 4 of the paper constructs an instance on which the best affine policy costs times the fully-adaptable optimum, for any . This mission formalizes that lower bound.
Timeline: Ben-Tal et al. (2004) propose affinely adjustable robust counterparts; Bertsimas, Iancu and Parrilo (2010) prove optimality of affine policies for one-dimensional multistage problems; Bertsimas and Goyal (2012) give the upper bound and the matching lower-bound example formalized here.
The two-stage problem has data , , , and :
The value is the same minimum over policies of the form ; such a policy must be nonnegative on all of .
The large-gap instance of display (19) has , a parameter with (condition (18)), and
where are the unit vectors and is the indicator vector of a set of coordinates. A permutation of the coordinates acts on vectors by and on matrices by .
The paper writes ; the constant is the one the proof establishes, so the explicit statement is the stronger one.
The result shows that the approximation guarantee for affine policies on problems with (Theorem 4 of the same paper) cannot be improved beyond a factor , so the uncertainty set that looks like a portion of the unit sphere in the nonnegative orthant is essentially the worst case for affine recourse. It also explains why later work moved to piecewise-affine and finitely adaptable policies to close the gap. The example satisfies , and , so the lower bound applies to every larger problem class.
The theorem is proved in the paper; to our knowledge no machine-checked version exists. A formalization adds checked statements of the symmetrization argument (an optimal affine policy may be taken invariant under the symmetry group of the instance), which applies to any symmetric robust linear program, and a checked derivation of the explicit constant.
The upper bound is a direct construction. The difficulty lies in the lower bound on , which must hold for every affine policy, a family with free parameters. Bounding the cost of a policy at a few chosen points of does not suffice without first reducing the parameters, and the reduction requires that an optimal affine solution exists (attainment of the minimum over an unbounded parameter set) and that averaging over the symmetric group preserves both feasibility and optimality. The remaining argument balances three different generators of against each other, and the exponents of must be tracked exactly through ceilings and real powers.
Vectors are Fin m → ℝ with the componentwise order and 0-based indices; matrices are Matrix (Fin m) (Fin m) ℝ. The values and are infima of the sets of worst-case cost bounds achieved by feasible solutions (epigraph form), so they do not rely on a supremum of a possibly unbounded function. Affine policies must be nonnegative on . Optimal solutions are defined as feasible solutions whose worst-case cost is bounded by every achievable bound, so Lemma 8 asserts attainment. Powers are real powers; and exactly as on the page. is the convex hull of its listed generators; the generator count printed in (19) plays no role.
The parameter is not restricted beyond and , as in the paper. Lemma 4's proof on the page uses ; the statement is kept for all , where it remains true with a different witness. The Claims are stated for any symmetric feasible affine policy with cost at most ; their hypotheses are jointly unsatisfiable by Theorem 3, which is inherent in steps of a proof by contradiction.
A trivializing formalization is excluded: the goal mentions only the instance data and the two optimal values, not the symmetric parameters , and the nonemptiness of the feasible sets is established by Lemma 4 and by the existence of a feasible affine policy, so neither value is a junk infimum of an empty set.
A complete development needs: convex hulls of finite point sets in and their extreme points; the action of by coordinate permutation; averaging over the finite group ; and existence of minimizers for linear programs over a polytope. The symmetrization lemmas (5–8) are reusable for other symmetric robust problems. Proofs of any milestone, including partial infrastructure for linear-programming attainment, are welcome.
Local Rademacher averages measure the complexity of a learning problem only near the functions that matter, such as those with small empirical error, rather than over the whole function class. Bartlett, Bousquet and Mendelson (Local Rademacher complexities, Ann. Statist. 33 (2005)) show that error bounds for empirical risk minimization are governed by the fixed point of a sub-root upper bound on such local averages, and that these bounds give fast rates ( rather than ) under variance conditions. A bound is only useful in practice if it can be computed from the data. For classification with the discrete loss, the paper's Corollary 6.2 states the bound in terms of a localized empirical Rademacher average . That average is a supremum over a constrained subclass, and it is not obvious how to evaluate it.
Theorem 6.3 of the paper answers this. An upper bound on can be computed by any algorithm that minimizes a weighted empirical classification error. A similar reduction was known for the global Rademacher average of a classification class: Bartlett, Boucheron and Lugosi (Model selection and error estimation, Machine Learning 48 (2002)) observed that the empirical Rademacher average equals one half minus an expected empirical risk minimum with random labels, and Lemma 6.4 of the paper is adapted from their argument. Theorem 6.3 shows that localization and the use of star-hulls keep this reduction intact.
Fix inputs in a set () and labels . Everything below is deterministic given this sample. A classifier is a function , and is a class of classifiers. The discrete loss is . For a vector write
so is the empirical risk of .
A sign vector plays the role of Rademacher signs, and is the average over all sign vectors. The empirical Rademacher average of the loss functions of the classifiers with empirical risk at most is
For , and , the empirical local Rademacher complexity of the classification loss class is
In Corollary 6.2, . The parameter comes from the star-hull of the loss class: rescaling a loss function by turns the constraint into .
For a sign vector and a multiplier , the weighted empirical risk minimum is
It is the smallest weighted training error when the labels are corrupted to and example has weight .
If some has , then
The multiplier is kept general, and the term appears on both sides as printed.
The theorem turns a quantity defined by a supremum over a data-dependent subclass into one computable by a standard learning primitive. For each sign vector and each multiplier , is the value of a weighted classification problem, which any weighted empirical risk minimizer solves. The expectation over signs can be estimated by repeated sampling. The paper notes that is Lipschitz in , so a finite grid of values suffices, and that a sub-root upper bound on can then be read off. Combined with Corollary 6.2, this yields error bounds for empirical risk minimization in classification that are computable from the training data and that localize: they depend only on the classifiers with small empirical error.
The result is proved in the paper. It has not been formalized; as far as a search of the Prove2Me catalog shows, neither the classification loss class nor exists as a formal object. This mission produces machine-checked statements of the theorem and of its three proof steps. These cover the exact identity between Rademacher averages of the discrete loss class and random-label empirical risk minimization, and a Lagrangian duality bound for constrained empirical risk minimization.
The obvious route is to apply Lemma 6.4 and then exchange the constrained minimum for a Lagrangian. Each step has a point where a careless argument fails.
xs : Fin n → X for an arbitrary type X. Labels and signs are real vectors Fin n → ℝ. Classifiers are functions X → ℝ with values in , a class is a Set (X → ℝ), and the discrete loss is defined on all real pairs. Sign vectors are indexed by Fin n → Bool through the published UnderstandingML.signVec. Every , on both sides of every statement, is the finite average over these vectors; no probability measure is used. The empirical Rademacher average is the published UnderstandingML.rademacher applied to the set of loss vectors.⨆/⨅ over a subtype. The hypotheses make each index set nonempty and each family bounded, so these are true suprema and minima. The convention Real.sign 0 = 0 is used where the paper's sign is undefined; it affects only weight-zero terms.In robust optimization, a decision must satisfy a constraint for every parameter value in a prescribed uncertainty set. A nonlinear uncertain constraint can be difficult to use directly because it contains a universal condition over a continuum of parameters. Ben-Tal, den Hertog, and Vial study constraints whose value is concave in the uncertain parameter. Their Theorem 2 replaces the universal condition by one inequality involving a new vector and two conjugate functions. The replacement is the general framework used for the paper's later examples, including uncertainty regions assembled from simpler sets and nonlinear functions whose conjugates have explicit forms. The discussion paper, §§2–4 is the source for this mission; theorem and page numbers refer to that 2012 version.
The paper's result extends a more specialized counterpart for a linear uncertain constraint under a φ-divergence uncertainty region. That 2013 result has a proved formalization on Prove2Me, but its divergence-specific conjugate and uncertainty set are different objects. The same earlier formalization also supplies a proved version of the self-concordant-barrier statement that this paper quotes as Lemma 33, with a differently printed constant. Neither earlier theorem supplies the general concave-constraint result here.
Fix dimensions . The nominal vector is , and maps a primitive uncertainty to an uncertain parameter . Thus the uncertainty set is . The paper assumes that is nonempty, convex, and compact, with in its relative interior . Relative interior is taken inside the affine hull of a set, so may lie in a lower-dimensional plane.
A decision is . For each decision, is the effective domain of the uncertain constraint : is real on and is interpreted as outside it. The function is concave in on for every ; the paper imposes no convexity assumption in the decision . The robust constraint (RC) is for every . In the domain representation used here, this means every . The nominal vector is regular when for every decision , as in Definition 1.
The support function of is . The partial concave conjugate is . Both have extended-real values: an empty support set has support value , and the conjugate can be when its infimum is unbounded below. These values matter in the equivalence; replacing them by a default real number changes the constraint.
The goal is the paper's Theorem 2. Under the standing assumptions and regularity, for every decision ,
The right-hand inequality is the Fenchel robust counterpart (FRC). Its existence claim is essential: equality of primal and dual infima alone would not show that an auxiliary vector satisfying FRC exists.
Four source statements form the milestone path. Remark 5 gives the weak-duality inequality and the FRC-to-RC implication without concavity. Equations (16)–(18) calculate the support function of . Equation (7) states the relative-interior qualification. Equations (13)–(15) state the worst-case/dual-value identity and, through the printed minimum, attainment of the dual infimum. The milestone list quotes those source passages and identifies their printed pages. Theorem 2 and its proof appear on pp. 4–5.
The equivalence gives an exact way to replace an infinite family of uncertain inequalities by an existential constraint. In examples where the support function and concave conjugate can be evaluated or represented with standard optimization constraints, it yields a finite robust counterpart. The conclusion remains a mathematical equivalence even when such an explicit representation has not been found. It is also independent of any convexity of in the decision variable, a point the paper makes after Corollary 3.
This mission supplies reusable, domain-aware support and conjugate definitions and formal statements for the duality path in the paper's central result. The new goal and milestones are open proof obligations: their Lean declarations compile, but they do not yet have machine-checked proofs. The proved 2013 φ-divergence case is narrower and does not close them. A completed development would make the general relative-interior and attained-duality steps reusable for other robust optimization models.
The delicate point is the direction from RC to the existence of an FRC vector. Weak duality gives only a one-sided bound. Identifying the two optimal values still leaves an existence question when an infimum is not attained. The paper invokes Fenchel duality under a relative-interior intersection condition; replacing relative interior by ordinary interior would exclude lower-dimensional uncertainty sets and effective domains that the source permits. A second difficulty is keeping finite and infinite conjugate values distinct while subtracting them in the counterpart inequality. An unbounded-below conjugate must make a finite-support FRC value , not a plausible finite number.
Vectors are functions on Fin m, Fin n, and Fin L; is a real matrix, and dot products use the finite-vector dot product. Mathlib's intrinsicInterior ℝ represents relative interior. The domain map is explicit, with the concavity hypothesis imposed on that domain. The real representative of outside is ignored everywhere. The paper's Notation paragraph calls its generic concave functions closed, but the statements here omit closedness: the finite-dimensional duality qualification used for Theorem 2 needs relative-interior overlap, not that extra regularity. This is a stated strengthening of the source theorem, not a change of its feasible points.
Support functions, conjugates, worst-case values, and dual values use EReal. The paper's “max” in (8), (13), and Remark 5 is read as an extended-real supremum; its “min” in (15) is an infimum accompanied by an attaining vector. The support identity includes , where both sides are , although Theorem 2 keeps the paper's nonempty, convex, compact . On the theorem's hypotheses the support value is finite and is nonempty, so the undefined-looking combinations and cannot occur in FRC. No all-space real-valued substitute for is used, and the theorem still quantifies over every decision and every allowed uncertainty vector.
The proof development needs finite-dimensional relative-interior behavior under affine maps and Fenchel duality with attainment. General convex conjugates and support functions can serve later missions. Corollary 3 and the paper's complexity discussion are outside this mission. Theorem A.1 is not separately made a milestone here: as printed, its domain-restricted dual maximum has a problematic case; the directly used, attained identity (13)–(15) is the target under the main theorem's standing assumptions.
The Hirsch conjecture, stated by Warren M. Hirsch in a 1957 letter to George Dantzig, asserts that the combinatorial diameter of a -dimensional polytope with facets is at most . The diameter is the largest number of edge steps needed to walk between two vertices of the polytope. The question matters to linear optimization: every edge-following pivot rule of the simplex method, starting at a vertex of the feasible region, needs at least as many pivots as the graph distance to an optimal vertex. A polynomial bound on polytope diameters is a necessary condition for a strongly polynomial simplex method, which is still unknown.
Timeline of the conjecture before the counterexample:
The polynomial Hirsch conjecture, which asks only for a bound polynomial in and , remains open.
A polytope in is written as . A facet presentation is one in which has nonempty interior and no inequality is redundant. For a bounded polytope it then has dimension , and its inequalities correspond one to one to its facets. A step between two vertices crosses an edge (a one-dimensional face). The polytope is non-Hirsch when its diameter exceeds .
A spindle (Santos, Definition 1.4) is a polytope with two distinguished vertices such that every facet contains exactly one of them. Its length is the graph distance from to . The polar objects are prismatoids: polytopes with two parallel facets containing all vertices, whose width is the dual-graph distance between and .
Santos's explicit object is the 5-prismatoid whose vertices are the 48 rows of Table 1 of the paper: with and with . Its polar is a spindle with apices and . Table 2 of the paper lists the 322 facets of , which are the 322 vertices of : and the points of twenty types with sixteen sign patterns each. The symmetry group of has order 64; its index-two subgroup preserves and .
The goal fixes the dimension (43) and the number of facets (86), as the paper does. It does not assert the exact diameter (44, remarked on p. 24).
Corollary 1.7 settles the Hirsch conjecture in the negative. Theorem 1.5 is the reusable part: it turns any spindle whose length exceeds its dimension into a counterexample. That made the later search for small spindles (Matschke–Santos–Weibel) a finite, low-dimensional problem. Theorem 1.6 is the concrete certificate. Its claims about Tables 1 and 2 are finite statements about explicit rational data.
The result is proved, and several pieces are already formalized on Prove2Me. Hirsch.santos_counterexample (Proved) states that some polytope violates the bound , with no dimension or facet count. Hirsch.strong_dstep_spindle (Proved) is the "in particular" clause of Theorem 1.5, counting inequalities rather than facets. Lemmas 2.2 and 2.4 of the paper are Proved in polar form (Hirsch.spindle_inward_row_push_graph, Hirsch.spindle_wedge_vertex_graph_projection), as is the bound for spindles (Hirsch.spindle_n_ge_two_d). This mission adds the dimension-43, 86-facet statement with facets counted exactly, the general length bound with the spindle structure preserved, and a machine-checkable account of Santos's specific spindle.
The obvious first idea for the 5-dimensional milestones is brute computation. This is feasible in principle but heavy in Lean. Showing that 322 given points are extreme requires exhibiting, for each, five linearly independent tight rows among 48. Showing that no other vertex exists requires a complete enumeration argument rather than a membership check. Exact distance 6 requires the full adjacency structure between the 322 vertices, not only a path.
For the general theorems, the difficulty is that the construction is a one-point suspension followed by a perturbation. Edges and facets of the new polytope must be controlled, with the face lattice changing only in a prescribed way. Diameter is not monotone under arbitrary perturbations, and in particular a walk can become shorter. Keeping the facet count exact (not merely the inequality count) adds an irredundancy argument at each step.
Polytopes are H-presentations Hirsch.Hpoly a b with a : Fin n → EuclideanSpace ℝ (Fin d), from the platform definition Hirsch_model. "A -polytope with facets" is boundedness plus IsFacetPresentation: nonempty interior and every row irredundant. Without this predicate, padding with redundant rows would change the bound , and the statement would collapse to the platform's dimension-free Hirsch.santos_counterexample. Diameter and length use the platform's padded walks (Hirsch.DiamLE, Hirsch.Reach). "Length at least " means no walk of fewer than steps, and "length exactly " adds a walk of steps. The junk-valued Hirsch.gdist is never used.
All prismatoid statements of the paper (§3, Theorems 2.6, 3.1, 4.1) are stated for the polar spindle, which the paper licenses (pp. 6, 8, 9). Vertices of become rows, facets of become vertices, the width becomes the apex distance, and become . Natural-number expressions , , are faithful because spindles have . Theorem 1.5's "length " is read as "length at least ", which is equivalent by monotonicity. Tables 1 and 2 are written entry by entry in Lean in the page's order.
Useful contributions include proofs of the finite Table 1/Table 2 facts by certified computation, reusable lemmas on one-point suspensions and on facet presentations under perturbation, and a proof of Corollary 1.7 from milestones 5 and 7.
Two-stage adaptive optimization models decisions made in two steps: a first-stage decision is fixed before an uncertain parameter is revealed, and a second-stage (recourse) decision may then depend on the realized value. In the robust version, the uncertain parameter ranges over an uncertainty set and the objective is the worst-case cost. Such models arise in capacity planning, network design and inventory problems with uncertain demand, where the demand is the right-hand side of the constraints.
Computing an optimal fully adaptable second-stage policy is intractable in general: the recourse is an arbitrary function of the uncertain parameter. The standard tractable surrogate, introduced by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 99, 2004), restricts the recourse to an affine policy , whose optimization is a finite convex program. Practitioners report that affine policies often perform well, which raises the question of when they are optimal and how much they can lose.
Bertsimas and Goyal (Math. Program. Ser. A, 2012) answer this for problems with an uncertain right-hand side. Their Theorem 1 shows that affine policies are optimal when the uncertainty set is a simplex, that is, the convex hull of affinely independent points of . Their Theorem 2, the subject of this mission, shows that this is almost tight: one additional extreme point can make the best affine policy almost twice as expensive as the optimum.
Let , , , and let be an uncertainty set. The problem is
Here is the first-stage decision and is the second-stage policy; all inequalities between vectors are componentwise. The value is the same minimum restricted to affine policies with and ; an affine policy must still satisfy for every . Always .
The instance of (6) is defined for and an even integer . It has , , , , and
where , is the -th unit vector for , has entries in its first coordinates and in the others, and has in its first coordinates and in the others. Thus is generated by nonzero points. The last two are also extreme points when ; for or they lie in the convex hull of .
For a permutation of , write . A set is permutation-invariant with respect to if (Definition 2), and is the set (10) of permutations with .
Together with Theorem 1 of the same paper, Theorem 2 delimits exactly where affine policies are optimal for right-hand-side uncertainty: for a simplex they are, and with one more nonzero extreme point the gap can approach . The ratio is measured against the fully adaptable optimum, which is the quantity a practitioner gives up by choosing affine recourse. Later sections of the paper push the same construction to for sets with polynomially many extreme points and prove a matching upper bound; Theorem 2 is the simplest member of this family and isolates the mechanism.
The result is proved in the paper; to our knowledge it has not been machine-checked. The mission produces a formal model of two-stage adaptive linear optimization with uncertain right-hand side, the values and , and a verified lower-bound instance. The symmetrization statement (Lemma 3) is an instance of a general principle, that a convex problem invariant under a group has an invariant optimum, which is reusable well beyond this paper.
The upper bound requires a feasible policy, which can be written down. The lower bound on is a statement about all affine policies, an dimensional family, and cannot be checked policy by policy. The obvious attempt, testing an arbitrary affine policy against a few extreme points, fails because an asymmetric policy can trade cost between coordinates. The argument needs an optimal policy that is symmetric, which in turn needs both the existence of an optimal affine solution (attainment of a minimum over a non-compact set of policies) and the invariance of the instance under the permutations of and the swap of the two halves. Without the attainment step, a contradiction for every policy of cost at most yields only , not the strict inequality.
Vectors are Fin m → ℝ with the componentwise order, matrices are Matrix (Fin m) (Fin n) ℝ, is B *ᵥ x and is d ⬝ᵥ y. Indices are 0-based: the paper's coordinate is index , so "" is (i : ℕ) < m / 2, with natural-number division (exact since is even). is x ∘ τ for τ : Equiv.Perm (Fin m).
and are the infima of the sets of real numbers for which some feasible (respectively feasible affine) solution satisfies for all . This epigraph form avoids a supremum of a possibly unbounded function; on an infeasible instance the infimum would be Lean's junk value , which is why Lemma 1 also asserts the existence of the feasible solution of cost . Optimal solutions are stated by IsOptimalAff: feasible, with worst-case cost bounded by every bound achieved by any feasible affine solution. Affine policies must be nonnegative on , as in (1).
The instance is concrete, so the standing assumptions of (1) (nonnegative costs, compact convex full-dimensional , feasibility) are properties of the data rather than hypotheses. The goal adds no hypothesis to the page: , even and . For the statement is easy but still true. The three Claims are stated for any feasible affine solution with constant intercept and worst-case cost at most , which is exactly what the paper's proof uses about the symmetric optimal solution under its contradiction hypothesis (12). Lemma 1 drops the unused hypothesis . Definition 2 prints ""; the formalization reads as the set .
Replacing by the cost of one particular affine policy, stating the goal with , or bounding only policies with constant intercept would not be Theorem 2, and is ruled out: the goal compares the two optimal values with a strict inequality.
A complete development needs convex hulls of finite point sets in Fin m → ℝ, the existence of a minimizer for the affine problem (a linear program in with infinitely many constraints indexed by , reducible to the extreme points), averaging of optimal solutions over a permutation group, and elementary estimates with . Contributions of general lemmas on attainment of semi-infinite linear programs and on symmetrization of convex programs are welcome.
Two-stage adaptive optimization models decisions taken in two rounds: a first-stage decision is fixed before an uncertain parameter is revealed, and a second-stage decision is chosen after the parameter is observed, so that the second stage may depend on arbitrarily. The objective is the worst case over an uncertainty set of possible parameters. Such models arise in robust network design, capacity planning and two-stage covering problems, and they generalize the two-stage robust combinatorial problems (set cover, facility location) studied by Dhamdhere, Goyal, Ravi and Singh.
Optimizing over all functions is intractable in general: Bertsimas and Goyal note that the optimal second stage is piecewise linear in with possibly exponentially many pieces (Bemporad, Borrelli and Morari, 2003). A standard remedy, introduced for robust linear programs by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004), restricts the second stage to affine policies (linear decision rules) ; the best affine policy is computable by a single convex program and performs well empirically. The question is when this restriction loses nothing.
Timeline of the relevant results:
Let , , and . The problem of model (1) is
where inequalities between vectors are componentwise. A pair satisfying the constraints is feasible; its worst-case cost is . A feasible pair is optimal when its worst-case cost equals , and an affine policy is a second stage of the form with , , still required to be nonnegative on . The value is the same minimum restricted to affine policies.
A simplex in is the convex hull
of affinely independent points, that is, points for which are linearly independent. The proof works with the matrix , the matrix of display (2), and the affine rule . In Lean these are Qmat v, Ymat v g and interpolant v g, with vertices v : Fin (m+1) → Fin m → ℝ.
If with affinely independent and is feasible, then there exist , and such that
is an optimal solution of , optimal among all (not only affine) two-stage solutions. In particular .
The proof of Theorem 1 has no numbered lemma; the milestones are its displayed steps, in attack order:
The result. Theorem 1 identifies a class of uncertainty sets on which the tractable affine restriction is exact, for every constraint matrix and and every nonnegative cost. It is the positive anchor of the paper: Sections 3 and 4 show that with extreme points the best affine policy can already be worse by a factor , and that on sets with exponentially many extreme points the gap can be ; Section 6 uses a dominating simplex, on which affine policies are exact, to build an -approximation for general . The theorem also says that on a simplex the whole adaptive problem reduces to scenario copies of a linear program.
Formalizing it. The result is proved on paper; no machine-checked version is known on Prove2Me. This mission produces the model (1) in Lean, the barycentric-coordinate identity for a simplex in matrix form, and a statement of optimality that asserts attainment of the minimum in (1), which the paper's proof takes for granted.
Two steps are not routine to formalize. First, the paper starts from "an optimal solution ", that is, it assumes the minimum in (1) is attained. Over arbitrary functions this is not automatic; on a simplex it follows because the problem reduces to a finite linear program on the vertices, whose optimum is attained, but Mathlib has no theory of linear-programming attainment, so this reduction has to be built. Second, the affine-independence step needs the passage from affine independence of points to invertibility of the matrix , and the identity requires the barycentric coordinates and the inverse matrix to be matched index by index. The naive idea of comparing and as real infima does not prove the goal: equality of the two infima says nothing about the existence of an optimal solution.
Vectors in are Fin m → ℝ, with the componentwise order; matrices are Matrix (Fin m) (Fin n) ℝ. The paper's indices start at , Lean's at : is v (j-1) and is v (Fin.last m). The simplex is convexHull ℝ (Set.range v); it is compact, convex and, by affine independence, full-dimensional, so these standing assumptions of (1) are not stated separately. Nonnegativity of is the hypothesis that all vertices are nonnegative (the page writes , a slip for ). Feasibility of (1) is a hypothesis, as the paper assumes. Optimality (IsOptimalAdapt) means: feasible, and every worst-case cost bound achieved by any feasible two-stage solution is achieved by this one. The values and are infima of the sets of achievable bounds; they are provided for reference and the goal does not depend on them.
The goal must not be replaced by , by optimality among affine policies only, or by a version that assumes an optimal solution exists: each of these drops the content "there is an optimal solution and it is affine". The goal does not mention , or the interpolant.
A complete development needs: linear-programming attainment for a finite system of linear inequalities with a cost bounded below (reusable well beyond this mission), the linear-algebra lemmas relating affine independence to an invertible edge matrix (reusable for barycentric coordinates in general), and the convex-hull representation of points of a simplex. Contributions of any of these as separate lemmas are welcome.
Sparse graphs whose adjacency spectrum is concentrated near zero, expanders, are used throughout theoretical computer science: in error-correcting codes, derandomization, sorting and routing networks, and the construction of pseudorandom objects (Hoory, Linial and Wigderson, survey). The best possible spectral expansion for a -regular graph is governed by the Alon–Boppana bound , and graphs attaining it, Ramanujan graphs, were constructed explicitly by Lubotzky, Phillips and Sarnak (LPS 1988) and by Margulis. These constructions exist only for special degrees ( with prime) and special numbers of vertices (orders of or ). Applications often need a graph of a prescribed size .
N. Alon's paper Explicit expanders of every degree and size (arXiv:2003.11673v1; Combinatorica 41, 2021) shows how to obtain explicit near-Ramanujan graphs on exactly vertices. This mission formalizes the spectral core of its Theorem 1.2: a Ramanujan graph on vertices can be enlarged to vertices, with degree raised by one, while the nontrivial eigenvalues stay within a constant factor of optimal.
Let be a finite set of vertices. A -graph is a -regular graph on vertices whose adjacency matrix satisfies for every nontrivial eigenvalue , that is, every eigenvalue other than the top eigenvalue of the constant vector . For a symmetric with , the nontrivial eigenvalues are those with an eigenvector satisfying . Graphs may carry loops, at most one per vertex, and a loop adds one to the degree: it is a diagonal entry of .
Fix an integer and let be an -graph on , a -regular Ramanujan graph. Let be new vertices and let be pairwise disjoint sets of vertices each. Put and . The graph on is obtained from by joining each to every vertex of and adding one loop at each vertex of . Its adjacency matrix is
where is the adjacency matrix of (zero on ), that of the stars joining to , and the diagonal matrix of the loops. Every vertex of has degree .
The paper states for ; its proof gives , which is stronger, and the error term it produces is . The goal is parametrised by , and the sets , so it does not depend on how and are chosen.
With the Lubotzky–Phillips–Sarnak graph on vertices for the largest suitable prime with , and , the distribution of primes in arithmetic progressions gives , and the goal yields an explicit -graph with for every sufficiently large . This is within a factor of about of the Ramanujan bound , for every number of vertices, by an elementary modification of an existing graph. The statement is useful independently of LPS: any Ramanujan graph, or any graph with a bound on its nontrivial eigenvalues, can be padded to a nearby size in the same way.
The result is proved in the paper. No formalization of it, of the notion, or of the variational characterization of nontrivial eigenvalues for regular graphs exists on the platform. The mission produces a checked version of the spectral argument, and the variational characterization (milestone 1) is a general fact about symmetric matrices with constant row sums that applies to any spectral expander argument.
The vertices of and lie in the old graph , whose spectrum is controlled, but the new vertices of are not; and a vector orthogonal to on need not be orthogonal to the constant vector on . Bounding by applying the Ramanujan bound for to restricted to therefore fails: the restriction has a component along the trivial eigenvector of , whose eigenvalue is large. The argument must show that this component is small, of order , and must balance the star edges between and against the loops on so that every vertex class gets the same coefficient. The naive bound added to for and for gives a constant larger than ; the stated constant needs the weighted estimate.
On the Lean side, milestone 1 concerns the spectrum of a symmetric matrix on the invariant subspace , while Mathlib states the spectral theorem for the whole space.
SimpleGraph with adjMatrix.Large-scale nonsmooth convex problems, such as minimising a Lipschitz convex function over a probability simplex with millions of coordinates, are routinely solved by first-order methods that use one subgradient per iteration. The classical projected subgradient method reaches accuracy after iterations, where and are measured in the Euclidean norm; on the simplex this hides a factor of order in the dimension. Nemirovski and Yudin's mirror descent algorithm (MDA) replaces the Euclidean geometry by one adapted to the feasible set and, on the simplex, reduces the dimension dependence to .
Beck and Teboulle (Oper. Res. Lett. 31 (2003) 167–175, doi:10.1016/S0167-6377(02)00231-6) showed that mirror descent is a projected subgradient method in which the squared Euclidean distance is replaced by a Bregman-type distance . This viewpoint gives a short convergence proof, and with the entropy as it yields a fully explicit method on the simplex, the entropic mirror descent algorithm (EMDA), the same multiplicative update that underlies exponentiated-gradient and Hedge-type algorithms in online learning.
Timeline. Nemirovski and Yudin (1983) introduce mirror descent with a rate on the simplex. Ben-Tal, Margalit and Nemirovski (SIAM J. Optim. 12 (2001)) analyse MDA with the potential , , whose conjugate requires a one-dimensional root-finding at each step. Beck and Teboulle (2003) derive MDA as a nonlinear projected subgradient method (SANP), prove its efficiency estimate for an arbitrary norm, and show that the entropy gives the same rate with a closed-form update.
Let be with an arbitrary norm , and the dual norm. The problem is under Assumption A: is closed and convex; is convex on and Lipschitz there, ; has a minimiser ; and a subgradient can be computed at every .
Let be strongly convex with parameter and differentiable. The distance-like function (3.10) is
The subgradient algorithm with nonlinear projections (SANP, (3.11)) starts from and sets, with step sizes ,
With this is the projected subgradient method.
On the unit simplex take the entropy (5.27), with . SANP becomes the entropic descent algorithm (EDA):
If is convex and -Lipschitz on for , with subgradients satisfying , and the EDA is started at with step for a horizon , then
For any norm, any -strongly convex and any SANP run,
and with the optimal constant step this gives .
The milestones follow the paper's proof: the three-point identity (Lemma 4.1), the optimality condition (4.16), the lower bound , the one-step inequality (4.21), Theorem 4.1(a), Proposition 4.1 (optimal step), Theorem 4.2 and its version with an upper bound on ; then for the simplex, the 1-strong convexity of for (Proposition 5.1(a), Remark 5.1), the bound (Proposition 5.1(c)), and the identification of the EDA with SANP.
The result shows that for nonsmooth convex minimisation over the simplex an explicit first-order method attains accuracy in iterations, with measured in the dual norm. The general estimate of Theorem 4.2 applies to any norm and any strongly convex potential, and is the template for later analyses of mirror descent, its stochastic and online variants, and mirror-prox methods.
Formalizing the paper produces a norm-agnostic, machine-checked proof of the mirror descent efficiency estimate, in which subgradients are dual-space objects and the dual norm is explicit, and a verified link between the entropy, the geometry and the multiplicative-weights update. To our knowledge none of these statements is formalized; existing formal developments of online mirror descent work in Euclidean space with Legendre potentials and bound regret for linear losses, which is a different statement.
The algebra of Theorem 4.1 is short, but it rests on facts that are not available off the shelf. The first-order optimality condition (4.16) must be derived for a minimiser over a convex set without assuming the set has interior (the simplex has none in ). The bound must be obtained from the chord definition of strong convexity for an arbitrary norm. On the simplex, strong convexity of the entropy with respect to is a form of Pinsker's inequality, and it must hold on the closed simplex, where the entropy is not differentiable at the boundary. Finally, the EDA must be shown to be the exact minimiser of the SANP subproblem over , which is a Gibbs variational principle. A tempting shortcut, working throughout in Euclidean space, fails: it changes the dual norm of the subgradients from to and the strong convexity constant of the entropy, and loses the rate.
Sections 3–4 live in a general real normed space; a subgradient is a continuous linear functional, is its value at , and is the operator norm. is the Fréchet derivative. Iterates are indexed from . A SANP run is a predicate on sequences: each step size is positive, each iterate lies in , is differentiable there, and the next iterate minimises the SANP objective. This encodes the paper's standing assumption that SANP is well defined, and replaces " has nonempty interior" and "". Section 5 works on as functions with explicit and sums; is the relative interior, and the entropy formula is evaluated on only. "" is stated as the existence of with .
Added hypotheses, each disclosed in the item: a bound on the oracle (used by the proofs of Theorems 4.1(b), 4.2 and 5.1, not implied by the Lipschitz condition for subgradients relative to ); in Proposition 4.1, without which the proposition as printed is false; in the step sizes. The step sizes of (4.23) and of the EDA are constant over a fixed horizon , which is what the proof chooses; Theorem 5.1 is stated with , since the free index in the printed bound (5.28) cannot be bound, and is what the proof yields.
Trivializing formalizations are ruled out: is never evaluated where fderiv is a junk value (the run requires differentiability at every iterate), the SANP step is never chosen by Classical.epsilon, the bound of Theorem 5.1 is not stated with a maximum of over the run, and the step is not an anytime schedule .
A complete development needs first-order optimality conditions over convex sets, strong convexity and Bregman distances in normed spaces, Pinsker-type inequalities for finite distributions, and the Gibbs variational principle. These are reusable beyond this mission; proofs of any milestone, and general lemmas that serve several of them, are welcome.
The newsvendor problem is the basic model of inventory under uncertain demand. A decision maker orders units before demand is observed, and pays a unit backordering cost for each unit of unmet demand and a unit holding cost for each unit left over. When the demand distribution is known, the optimal order is a quantile of it. In practice the distribution is unknown and the decision maker holds historical data, often including features: observable covariates such as the day of the week, the weather or a recent sales trend, recorded alongside each past demand.
Rudin and Vahn (MIT Sloan Working Paper 5036-13, version of February 6, 2014, from MIT DSpace; published as Ban and Rudin, Operations Research 67(1), 2019, doi:10.1287/opre.2018.1757) propose to learn the order quantity directly as a linear function of the features, by minimizing the empirical newsvendor cost over the training data, with or without a regularization penalty. Their question is the one any data-driven decision rule must answer: how much worse can the learned rule do on new data than it did on the data it was fitted to? When the number of features is comparable to the sample size ("big data"), a bound that grows with says nothing, and the paper's Theorem 2 gives one for the regularized rule that does not depend on .
This mission formalizes that bound, Theorem 2 of the working paper, together with the results its proof is assembled from. All page and result numbers refer to the 2014 working paper, not to the published article.
Cost. For an order and a demand , the newsvendor cost is
Write .
Data. A data point is a pair of a feature vector and a demand . Features lie in a domain inside the ball , and demands lie in . A sample consists of independent draws from an unknown probability distribution concentrated on .
Rules and risks. A vector defines the linear decision rule . Its true risk and empirical risk are
The regularized algorithm (NV-reg). For a parameter , the rule minimizes
The objective is strictly convex, so the minimizer is unique. Following Appendix B of the paper, the rules the algorithm outputs on samples from are assumed to map into (the paper's ): the learned order quantity is never negative and never exceeds the demand cap.
Uniform stability. An algorithm is uniformly stable with parameter if removing one observation from any sample changes the loss of its output at any test point by at most (Bousquet and Elisseeff's Definition 6, the paper's Definition 1).
For every and , with probability at least over ,
The dimension appears nowhere in the bound.
The result. Theorem 2 bounds the generalization gap of the regularized feature-based newsvendor rule at rate with constants that depend on the costs, the demand cap, the feature radius and , but not on the number of features. It gives a theoretical basis for regularizing when is not small, and it indicates how to scale with the feature radius. The companion bound for the unregularized rule (Theorem 1) grows linearly in .
Formalizing it. The theorem is proved in the paper, but its proof is short and relies on cited results: Theorem 5 and Theorem 6 are stated with references to Bousquet and Elisseeff and no proof of their own, and the paper's Theorem 6 is a two-sided variant of Bousquet and Elisseeff's Theorem 12 that is only sketched. None of these results has a machine-checked proof. A formalization produces a checked two-sided stability-to-generalization theorem for general algorithms (reusable for any stable learner), a checked stability bound for a regularized piecewise-linear loss, and the newsvendor bound itself, with the constants the proof actually supports.
The bound is not a uniform-convergence argument: the class of linear rules on has complexity growing with , so any bound that holds simultaneously for all rules in the class depends on . The bound must exploit the specific rule produced by the algorithm. The two analytic steps that carry this are the stability of the regularized minimizer, which needs a strong-convexity comparison between the full and the leave-one-out objective, and a concentration inequality of bounded-differences type for a function of the whole sample whose differences are controlled only through stability.
The leave-one-out comparison is a known pitfall. If the leave-one-out problem is run literally on points it carries the weight , and the comparison argument then gives twice the constant of Theorem 4. The stated constant holds for the leave-one-out objective that keeps the weight , which is the form of Theorem 5.
Representation. Features are EuclideanSpace ℝ (Fin p), rules are vectors acting by the inner product, and data points live in EuclideanSpace ℝ (Fin p) × ℝ. The cost is the published newsboy loss with overage cost and underage cost ; the empirical and true risks are the published empirical and generalization errors, and the (NV-reg) objective and its -weighted leave-one-out version are the published regularized objectives of Bousquet and Elisseeff. The regularizer is (the display prints both and ; the text calls the problem a quadratic program). "With probability at least " is stated as: the event on which the gap exceeds the bound has measure at most under the product measure .
Standing assumptions and pinned hypotheses.
Trivializing formalization ruled out. The range assumption is quantified only over feature vectors in and over samples drawn from ; stated over the whole ball , it would force (both and would lie in ) and the goal would be nearly empty.
What is needed and reusable. McDiarmid's two-sided bounded-differences inequality under product measures; integrability of bounded measurable losses; existence and properties of minimizers of strongly convex objectives on ; the comparison argument behind Theorem 5. Theorem 6 is stated for an arbitrary data space and hypothesis space and is reusable for any uniformly stable algorithm. Contributions to the Theorem 5 reference and to McDiarmid's inequality benefit other missions as well.
Prove that -SAT is NP-complete for every fixed , with at most literal occurrences per clause.
Construct the reductions and certificate verifier using the existing WordRAM definitions. We reuse proved polynomial backend and Cook–Levin SAT completeness.
Many systems consist of units that form themselves into clusters: individuals at a gathering forming conversational groups, monomers forming polymers, particles coagulating and fragmenting. Chapter 8 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) treats such clustering processes as Markov processes whose state counts the clusters of each type, and shows that when the process is reversible its equilibrium distribution has an explicit product form. The chapter opens with a model of social grouping (§8.1), develops a general basic model (§8.2) and later applies it to polymerization (§8.4).
The basic model sits in the same family as the migration processes and queueing networks of the earlier chapters: the method is to guess reversibility, solve the detailed balance equations, and normalize. Its specific feature is that the transitions are unions and break-ups of clusters, with rates quadratic in the cluster counts, rather than movements of single individuals.
There is a countable collection of cluster types . A state is a vector of non-negative integers, being the number of -clusters present, with only finitely many non-zero. For cluster types let be the -th unit vector and
the union of an -cluster with an -cluster into a -cluster, and the break-up of a -cluster into an -cluster and an -cluster. Given non-negative parameters and , the clustering process has transition rates
A closed clustering process lives on a finite irreducible state space . The open clustering process additionally lets one-clusters enter at rate and leave at rate ,
and its state space is the countable set of all with finite, every state being reachable from every other.
An equilibrium distribution is a collection of positive numbers summing to one that satisfies the equilibrium equations ; the process is reversible in equilibrium exactly when satisfies the detailed balance conditions .
If there are positive numbers with
then the open clustering process has equilibrium distribution
it is reversible, and the counts are independent, being Poisson with mean .
Theorem 8.2 gives the equilibrium of a whole class of coagulation–fragmentation dynamics in closed form: the cluster counts are independent Poisson variables, and the equation system (8.8) is the only thing to solve. Quantities such as the expected number of clusters of each type, or the proportion of units in clusters of a given size, are then read off directly. Theorem 8.1 gives the corresponding result for a closed system, where the normalizing constant couples the types; opening the system removes that coupling. The results are the base of the polymerization models of §8.4 and of the later literature on reversible coagulation–fragmentation processes.
The results are proved in the book, with short proofs that state the detailed balance computation is "readily verified". To our knowledge they have no machine-checked proof. The work this mission asks for is the formal verification of that computation for the aggregated rate function, including unions in which two clusters of the same type meet, and the normalization of an infinite product over a countable set of types, which the book takes for granted.
The book calls the detailed balance computation readily verified; the bookkeeping is where a formal check can fail. Two different unions, or a break-up and the entry of a one-cluster, can lead from the same state to the same state when a cluster type is reproduced by the transition, so the rate between two states is a sum over transitions, and the identity has to be checked for the sums, not for single transitions. The same-type case carries the falling factorial rather than .
The normalization is the second difficulty. The state space of the open process is countably infinite, the product (8.10) runs over infinitely many types, and the interchange that makes it sum to one requires (8.9). Without (8.9) the weights are not summable; this is the content of the book's remark that (8.9) is necessary.
Cluster types are an arbitrary countable type R carrying a linear order, used only to count each unordered pair of types once. States are finitely supported vectors R →₀ ℕ. The rate is the sum of the rates (8.3) of all unions and break-ups taking to , plus, for the open process, the rates (8.7); a transition is present only when the clusters it consumes exist, and holds because every transition changes the number of clusters. The one-cluster type is a distinguished element one. The closed state space is a finite non-empty set closed under positive-rate transitions and irreducible. The open process carries the book's assumptions that every state is reachable from every other and that the total rate out of each state is finite.
The statements are at the level of rates: reversibility is detailed balance for a positive, normalized , the equivalence with reversibility of the stationary process being Kelly's Theorem 1.3. That is the law of a stationary Markov process with these rates is not formalized. Independence and the Poisson laws are stated as the joint law of every finite set of counts. A formalization in which may vanish, in which detailed balance is imposed only for a degenerate choice of rates, or in which (8.10) is not normalized does not meet the goal: the are positive, the rates are arbitrary non-negative symmetric parameters, and both detailed balance and total mass one are required.
The development uses the published definitions KellyStochasticNetworks_Balance (detailed balance and the equilibrium equations) and the proved implication from detailed balance to the equilibrium equations. Lemmas on summing products over finitely supported vectors, and on infinite products of exponentials, are reusable beyond this mission. Lemma 8.3, a partial converse to Theorem 8.1, is not part of this mission; a faithful statement of it, with the units structure of the clusters, is a welcome addition.