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?
Markov decision processes are the standard model of sequential decision making under uncertainty in operations research, control and artificial intelligence. Their finite-horizon, discounted and average-cost versions are all solvable in polynomial time, by dynamic programming or linear programming. Papadimitriou and Tsitsiklis (The Complexity of Markov Decision Processes, Math. Oper. Res. 12(3), 1987) asked the next question: can these problems be solved fast in parallel, in polylogarithmic time on polynomially many processors (the class NC)? Their Theorem 1 answers no, unless every polynomial-time problem parallelizes: all three versions are P-complete. The proof is a short reduction from the circuit value problem (CVP), the canonical P-complete problem (Ladner, 1975). This mission formalizes the mathematical heart of that reduction: the constructed process has optimal expected cost zero exactly when the circuit evaluates to true.
The result is the first of a series of five missions on the same paper; the others treat the deterministic special cases (which are in NC) and the partially observed case (which is PSPACE-hard).
A circuit is a finite sequence of triples with . Each is one of the operations false, true, and, or. A triple with is an input; a triple with is a gate, and a gate reads two earlier triples, . The value of an input is its constant; the value of a gate is the Boolean operation applied to the values of triples and . The value of is the value of triple .
A finite Markov decision process has a finite state set , an initial state , and at each state a nonempty finite set of decisions. Taking decision at state at time costs and moves to with probability . A policy chooses a decision for every state and time. For a horizon the expected cost of is
and the optimal expected cost is over all policies.
From a circuit the proof of Theorem 1 builds a stationary process : one state per triple plus an absorbing state . An input state has one decision, moving to , at cost if the input is false and if it is true. An or gate has two free decisions, moving to and moving to . An and gate has one decision, moving to or with probability each. All other costs are zero. The initial state is triple and the horizon is .
In the Lean development these are MDPComplexity.CircuitValue.MDP (with Policy, trajProb, expCost, optCost), Circuit (with val, value, lastIdx) and Circuit.toMDP.
for every circuit with triples (theorem1_reduction). This is the claim "the optimum expected cost is 0 or less iff the value of was true" on p. 445.
The discounted analogue, which the paper asserts in one sentence: for , the optimal expected discounted cost of is at most iff is true (discounted_reduction).
Combined with the log-space computability of from , the goal shows that the finite-horizon Markov decision problem is P-hard, hence not in NC unless P = NC. This is the reason dynamic programming for general Markov decision processes is believed to be inherently sequential, and it frames the contrast drawn in the rest of the paper: deterministic processes are in NC, and partially observed ones are PSPACE-hard. The construction is also stationary, so it shows that even the stationary finite-horizon problem is P-hard, as the paper remarks.
The theorem is proved in the paper, in one paragraph; it is not open. To our knowledge no machine-checked proof of it exists. Formalizing it produces a precise statement of what the reduction proves, a reusable finite-trajectory model of finite-horizon Markov decision processes with time-dependent policies, and a reusable encoding of Boolean circuits and their value.
The informal argument is short, but two points need care. First, the optimum ranges over all time-dependent policies, which form an infinite type; the infimum is attained only because the expected cost depends on finitely many decisions, and this must be established rather than assumed. Second, the passage from "the expected cost is zero" to "the circuit is true" turns a statement about trajectory probabilities into a statement about the recursive value of the circuit, and the and gates (where both successors are reached with positive probability) behave differently from the or gates (where only the chosen successor is reached). Reasoning only along a single path, as for a deterministic process, does not suffice at and gates.
Theorem 1 is a complexity statement: "The Markov Decision Process problem is P-complete in all three cases." Membership in P, the log-space computability of the construction, the notion of P-completeness, and the average-cost case are not part of this mission; Mathlib has no log-space reductions or class P. The mission states the correctness of the reduction, for the exact process of the proof.
Conventions committed to:
Fin k (paper index is Lean index ); via [NeZero k]. The fields of an input are unused (the paper sets them to , not a triple index). Triple need not be a gate.Option (Fin k), with none the state ; decisions are Fin 2 at or gates and Fin 1 elsewhere.A formalization that defines the optimal cost directly as "the cost of the best choice at the or gates", or optimizes only over stationary policies, would make the goal a restatement of the circuit's value; the mission's optimum is over all time-dependent policies of the general model.
Contributions welcome: proofs of the milestones and the goal; lemmas on the trajectory model (marginalization of trajProb, attainment of the infimum for policies that matter only up to time ) that are reusable for any finite-horizon process.
A Markov decision process with finitely many states and decisions, a discount factor and the objective of minimizing expected discounted cost is the basic model of sequential decision making in operations research and reinforcement learning. It is solvable in polynomial time by linear programming. Papadimitriou and Tsitsiklis (Math. Oper. Res. 12(3), 1987) asked the finer question of whether it can be solved fast in parallel, and showed a sharp split: the general (stochastic) problem is P-complete (their Theorem 1), so it is unlikely to admit a polylogarithmic parallel algorithm, while the deterministic special case, where every transition probability is 0 or 1, is in NC (their Theorem 4).
The deterministic case is a shortest-path problem with a twist. Every policy traces a walk in a graph, and the cost of the walk counts its -th arc with weight . The paper's argument identifies the optimal discounted cost with the cost of a finite combinatorial object, a sigma, and computes it from discounted min-plus matrix products. This mission formalizes that identity.
A deterministic stationary Markov decision process consists of a finite set of states, an initial state , and for each state a finite nonempty set of decisions. Decision costs and leads with certainty to the state . Equivalently, it is a directed graph on with an arc of weight for each decision; parallel arcs and loops are allowed.
A policy chooses a decision for every state and time ; it is stationary if does not depend on . From it produces the states and the discounted cost
The optimal discounted cost is , the infimum over all policies .
A sigma is a walk along decisions whose nodes are distinct and whose last node repeats an earlier one, with : the walk from up to the first repetition of a node. It is a prefix of arcs followed by a cycle of arcs. Its discounted cost is the discounted cost of the infinite walk that follows it and repeats its cycle forever.
In the min-plus semiring (addition is , multiplication is , zero is ), let be the least cost of a decision from to ( if none), let multiply every finite entry by , and let
with the min-plus identity. The entry is the least discounted cost of a -arc walk from to .
For ,
with both minima attained. This is the claim on pp. 446–447 on which Theorem 4 rests. The algebraic expression is the corrected form of the paper's (see Formalization scope).
BertsekasDP.discounted_main_theorem (Proved), and the deterministic case is stated in this mission's model.The identity reduces an optimization over infinite objects, the time-dependent policies, to a minimum over finitely many closed-form expressions in matrix entries. Each is a product of min-plus matrices, and matrix products parallelize well; that is the source of the NC algorithm. The same reduction, with the discounting removed, underlies the minimum-mean-cycle characterization of the average-cost problem (mission II of this series), and the sigma structure reappears in the stationary finite-horizon analysis (mission IV).
On the formalization side, the result has been proved in the paper only as a short paragraph, which cites the existence of stationary optimal policies and leaves the algebra to the reader. Its printed formulas contain index slips (below). A machine-checked version fixes the exact constants. To our knowledge none of these statements has a formal proof. The existence of stationary optimal policies for finite discounted problems is formalized on the platform in Bertsekas's general stochastic setting.
The obvious argument says: an optimal policy may be taken stationary, a stationary deterministic policy produces an eventually periodic path, and an eventually periodic path is a sigma. The first step is the substantial one: the optimum is an infimum over all time-dependent policies , and a non-stationary policy can follow any walk at all, so this step is a statement about the whole dynamic program, not a combinatorial fact about a single walk. The second part of the goal adds a matching argument in the other direction: the expression ranges over arbitrary -arc walks and closed -walks, which need not be simple, so one must check that none of them beats the best sigma, and that the best sigma has and . Finally, the discount factors must be tracked exactly; the printed formulas are off by one power of in two places.
The Lean development lives in the namespace MDPComplexity.Discounted, with one definition file and five theorems. Conventions committed to:
DetMDP S has a finite state type, a nonempty finite decision type at each state (the paper says "a finite set "; nonemptiness is implicit since a policy must choose a decision), a successor map and real costs.optDisc is the infimum over all such policies. Defining it over stationary policies or over sigmas would make the goal true by definition. That shortcut is ruled out, and the stationarity step is part of the content.tsums, which are junk () for non-summable series; every statement that sums costs assumes , under which the series converge absolutely.Tropical (WithTop ℝ), so is ⊤ and the product is Mathlib's matrix product over the tropical semiring.Not formalized: membership in NC, the processor count , the parallel time, and the P-completeness of the general problem. Mathlib has no parallel complexity classes. Only the identity that makes the algorithm correct is a target.
Contributions welcome: proofs of any milestone. A bridge from DetMDP to BertsekasSSPModel (taking decisions as controls and 0/1 transition rows) would let milestone 2 be derived from the platform's proved Proposition 7.3.1. A direct proof of the deterministic case is also welcome. The lasso and walk lemmas are reusable for the other missions of the series.
Online matching describes allocation when requests must be answered as they arrive. A matching decision uses only the edges revealed so far and cannot be revised when later requests appear. In the bipartite setting studied by Karp, U. Vazirani, and V. Vazirani, the arriving vertices are girls and the possible partners are boys. Even when the full graph has a perfect matching, a fixed greedy priority can leave many girls unmatched. The paper introduced RANKING, which randomly chooses the boys' priority order once and then uses that order for every arrival.
The question is quantitative: how many pairs does RANKING guarantee in expectation against a graph and an arrival order chosen before its random ranking? The paper's target is a fraction approaching of the pairs in a perfect matching. Its printed Theorem 1 concerns an auxiliary algorithm called EARLY; the RANKING statement follows the intended chain through Lemmas 3 and 5. The original EARLY analysis has a gap for general upper-triangular matrices, so this mission states the RANKING target and the earlier, unaffected lemmas separately. This distinction matters because an assertion about EARLY would be a different formalization target.
A bipartite graph has a boy side and a girl side , each with vertices. An edge means that boy may be paired with girl . A matching is a collection of edges in which no boy or girl occurs twice. The standing hypothesis for the performance guarantee is that the graph has a perfect matching: some bijection from boys to girls selects an edge for every boy. The graph is otherwise arbitrary.
Girls arrive in a predetermined order. When girl arrives, only her incident edges are revealed. RANKING first chooses a uniformly random permutation of the boys. For each arriving girl, it selects the highest-ranked adjacent boy who is still unmatched, if one exists. Write for the final matching. The expected size is the finite average over all rankings. The guarantee must hold for every graph and every predetermined arrival order; relabeling girls lets the formal statement fix their order to .
The paper also uses a dual rows-arrive view. Boys arrive in an order and choose among eligible girls, whose priority order is fixed. This is the same greedy rule with the sides exchanged. For its triangular reduction, the columns are numbered and column has highest priority. An upper-triangular matrix with unit diagonal is a graph with every edge and with an edge only when . On such a graph, the auxiliary algorithm EARLY declines to match row if column is already covered by EARLY's own matching. For any matching , denotes the indices for which both row and column are covered.
For every , one threshold must work for every size and every graph with a perfect matching:
This is the uniform lower-bound reading of the paper's target. It does not prescribe a finite- additive constant. The mission goal is the RANKING assertion drawn from the paper's Theorem 1 and Lemmas 3 and 5. The six milestones formalize the paper's Lemmas 1–5 and the corollary to Lemma 4, in their source order. They cover the side-exchange identity, arbitrary refusal algorithms, the triangular reduction, the matching-count identity, its expected form, and the pointwise comparison with EARLY.
The guarantee gives a concrete worst-case floor for a simple randomized allocation rule: as the graph size grows, RANKING matches at least an asymptotic fraction of the pairs available in a perfect matching, in expectation. The order is selected before the random permutation, matching the paper's performance measure. The lower bound remains meaningful on sparse graphs and does not rely on a density assumption. The original paper also studies the limit on what any randomized online algorithm can guarantee; that upper-bound result is treated in a separate mission.
A formal development here would provide reusable finite definitions for online greedy matching, arbitrary state-dependent refusal, fixed-order duality, and uniform expectation over permutations. The goal is a theorem statement awaiting a machine-checked proof; compiling the draft declarations verifies their Lean syntax and types, not their truth. The local mission separates the valid early structural statements from later statements whose published EARLY argument does not justify them on general upper-triangular graphs.
The random permutation does not make the fate of different vertices independent. Matching one girl removes a boy who might be essential to a later girl, so a per-arrival probability estimate cannot simply be added across all arrivals. The dual and triangular views capture useful structure, but turning that structure into a uniform bound for every graph is the main obstacle. In particular, reasoning about EARLY as if its matched-column set had the same monotonicity as unrestricted RANKING fails on some upper-triangular matrices. A proof of the goal must establish the RANKING guarantee without treating those later EARLY statements as available facts.
Boys and girls are both Fin n; an adjacency matrix is a relation between them. A published predicate represents a perfect matching as an edge-preserving bijection. The generic greedy run processes arrival times in increasing order and interprets a smaller priority index as higher rank. It makes a new matching decision only from the current matching and the arriving vertex. RANKING's returned edges are consistently ordered as (boy, girl), even though girls arrive. The dual run has rows arriving in an arbitrary permutation and takes column as highest priority in Lean's zero-based numbering. EARLY's refusal test consults the matching constructed by EARLY itself.
All expectations are finite averages over Equiv.Perm (Fin n), scaled by . The formal claim is with a perfect matching, the displayed lower bound. Placing before preserves the worst-case meaning. The perfect-matching condition is essential: the empty graph cannot satisfy a positive linear guarantee. The triangular matrix in Lemma 3 retains every diagonal edge, so a zero matrix cannot witness the reduction. These conventions rule out vacuous versions of the goal and reduction.
The definitions of partial matching, covered vertices, greedy run, RANKING, EARLY, and uniform average are part of the mission. A complete proof may build further finite counting and permutation machinery; such lemmas can be shared beyond this paper. Contributions toward the six milestone statements, the goal, and faithful supporting results are in scope. Lemmas 6–12 and the printed EARLY Theorem 1 are outside this mission because their analysis depends on claims that fail for some matrices allowed by their surrounding assumptions.
A supplier who sells through a single newsvendor retailer faces double marginalization: the retailer bears the whole cost of leftover stock but earns only the retail margin, so under a plain wholesale-price contract he orders less than the integrated supply chain would. The literature reviewed in G. P. Cachon's chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, vol. 11, 2003) shows that buy-back, revenue-sharing and related contracts correct this distortion. Section 6.5 asks what happens when the supplier sells through several retailers who compete for the same customers.
Competition can push in the opposite direction. When customers buy wherever stock is available, a retailer who stocks more also takes demand from his rivals, and he does not count that loss as a cost. This demand-stealing effect pushes the retailers towards over-ordering, which offsets double marginalization. §6.5.1 makes this precise in the proportional allocation model, in which total demand is split among the retailers in proportion to their inventories. The model goes back to the deterministic version of Wang and Gerchak (2001); related allocation models are those of Lippman and McCardle (1997) and Anupindi and Bassok (1999), and Mahajan and van Ryzin (2001) observe the same mitigation of the need for coordinating contracts.
This mission formalizes §6.5.1 of the chapter's January 2003 third draft, pp. 48–53.
There are retailers and one supplier. Total retail demand is random, with distribution function that is differentiable on with density , strictly increasing on , and satisfies . The retail price is and the supplier's unit production cost is , with . Goodwill costs, the salvage value and the retailers' handling cost are zero.
Retailer orders . Write and . Retailer receives the demand . Under a buy-back contract he pays per unit ordered and is refunded per unit left over; is the wholesale-price contract. His expected profit is
Because total sales depend only on the total stock, the integrated chain earns with , and its optimal stock solves the newsvendor equation , Eq. (20). A Nash equilibrium is a profile of orders in which each maximizes over all orders . A contract coordinates the chain when its equilibrium total order is .
Two contract prices appear on p. 52: the wholesale price that induces total stock , and the buy-back wholesale price
For , and solving (20), with : maximizes ; ; the profile in which every retailer orders is the unique Nash equilibrium; and at that equilibrium
The milestones are the section's own claims, in attack order: the newsvendor characterization (20); the inequality ; the closed form of and its strict concavity in the retailer's own order (p. 50); the first-order condition and Eq. (21); the monotonicity and limits of the left side of Eq. (22), giving a unique root for ; the unique, symmetric Nash equilibrium for every ; the increase of the equilibrium total in ; that induces , that , and that the supplier's profit under wholesale pricing has negative slope at ; the coordinating price with for ; and the ratio (p. 53). A companion item states the endpoint , at which the supplier takes all of .
The section answers two questions. First, with competing retailers a plain wholesale-price contract can coordinate the chain and still leave the supplier a positive margin, which a single retailer never allows. Second, that contract is not the supplier's best wholesale price, and it fixes a single division of profit. Buy-back contracts remove both limitations: the family coordinates for every and moves the supplier's share continuously from to all of . The ratio also measures how little a coordinating contract adds when many retailers compete (80% of the optimal profit at ).
The results are proved in the chapter, mostly by short computations, and none of them has been machine-checked. The formalization makes explicit what the page leaves implicit: that no equilibrium has a retailer ordering zero, the limits behind "from 0 to 1", and the density condition behind the strict sign on p. 52. It also produces a reusable proportional-allocation game and a Nash-equilibrium predicate for nonnegative real strategies.
The algebraic identities (the profits at the coordinating contract, the ratio , the derivative at ) are routine once has its closed form. The closed form itself requires computing the expectation with proportional shares and identifying with .
The real obstacle is the uniqueness of the equilibrium. The page argues from first-order conditions, which describe only interior best responses. A complete proof must show that each retailer's profit is strictly concave in his own order, that no retailer orders zero in equilibrium, and that the all-zero profile (where has in a denominator) is not an equilibrium. Strict concavity is the delicate step. The second derivative mixes the density with the term , and concavity has to be established on the closed half-line, including the boundary .
Retailers are indexed by Fin n with (the page's ). The comparison in also allows a single retailer, as the page does. Orders are real numbers , and best responses range over all . The demand law is a probability measure on carried by with finite mean, is its cdf, and is a field with HasDerivAt F (f y) y for . These are the chapter's standing assumptions (p. 7). The condition is needed for (20) to have a solution. The integrated optimum enters each theorem through the hypothesis , which determines it uniquely. Transfers run from the retailers to the supplier.
Added or made explicit relative to the page: in the concavity claim (at the profit is linear); for the strict sign of the supplier's marginal profit; positivity of the total order wherever appears. The page's printed slips (the first-order condition rescaled by , "", "") are corrected in the statements and kept in the milestone quotes.
Ruled out as trivializing: and are the printed formulas, not "the price at which is an equilibrium"; the supplier's profit is computed from the transfers, not as minus the retailers' profits; the equilibrium statement quantifies over all nonnegative deviations, so restricting attention to interior or symmetric profiles is not an option.
A complete development needs interval integrals of a cdf, the fundamental theorem of calculus for , and strict concavity from a strictly decreasing derivative. The proportional-allocation game and the Nash predicate are reusable for the other allocation models of §6.5. No platform item is referenced: the competing-retailer game of Cachon and Lariviere (2005), RevShareCoord.Competing.*, uses deterministic revenue functions and is a different model.
Online convex optimization is the standard model for learning from a stream of data: in round a learner commits to a point in a convex set , a convex loss is revealed, and the learner pays , where is a fixed regularizer. Subgradient methods for this model use one fixed geometry (usually the Euclidean one) for every coordinate and every direction, regardless of the data. Duchi, Hazan and Singer (JMLR 12 (2011) 2121–2159) introduced ADAGRAD, which adapts the geometry to the observed subgradients. The diagonal version is one of the most widely used optimizers in machine learning and the ancestor of RMSProp and Adam. This mission formalizes the paper's full-matrix version: the proximal term is built from the matrix square root of the accumulated outer products of the subgradients, so the method adapts to correlated directions, not only to individual coordinates.
The analysis extends the regret bounds of primal-dual subgradient methods and regularized dual averaging (Nesterov 2009; Xiao 2010) and of composite mirror descent to proximal functions that change over time, and combines them with trace inequalities for the matrix square root. Concurrent work by McMahan and Streeter (COLT 2010) studied closely related adaptive proximal methods.
Vectors live in with the Euclidean inner product and norm . In round the learner plays and observes a subgradient , that is, for all . The regret against a comparator is
The outer product matrix is , a symmetric positive semidefinite matrix, and is its positive semidefinite square root. With parameters and , ADAGRAD with full matrices (Figure 2 of the paper) sets
starts at , and computes by one of two updates:
The dual (semi)norm of is , where is the pseudo-inverse.
Assume closed and convex, and convex, and minimized over at . For the primal-dual update with , every satisfies
and for the composite mirror descent update with any ,
In the order the proof uses them:
The quantity can be much smaller than the factor in the regret of non-adaptive online gradient descent with a tuned step size: it is small when the subgradients concentrate in a few directions, possibly not aligned with the coordinate axes. The paper's Corollary 11 rewrites it as times the square root of , the gradient term of the best fixed full-matrix proximal function chosen in hindsight. The supporting results have their own uses. Propositions 2 and 3 are the generic regret bounds for adaptive proximal methods. Lemmas 8–10 are trace inequalities for the matrix square root that appear throughout the analysis of second-order online methods.
The results are proved in the paper. To our knowledge none of them has a machine-checked proof. Formalizing them requires the matrix functional calculus (square roots, pseudo-inverses, real powers) in a form usable for inequalities, which Mathlib has only partly: for instance, monotonicity of the square root is in Mathlib for C*-algebras, which covers complex but not real matrices. A complete development gives a verified regret bound for an adaptive full-matrix method together with these matrix inequalities.
The online-learning half (Lemma 16, Propositions 2 and 3) is a convex-analysis argument once the proximal functions are quadratic. The obstacle is the matrix half. The natural approach to Lemma 10 is induction with a scalar inequality applied eigenvalue by eigenvalue. This fails because and do not commute, so their eigenvectors differ. One needs the concavity of on positive semidefinite matrices and its gradient, at points where may be singular. That is where Lemma 8 and the pseudo-inverse enter: the inverse root does not exist, and a limit is needed. The same issue arises in Lemma 9 and in the dual norm when .
Vectors are EuclideanSpace ℝ (Fin d), so ‖·‖ is the Euclidean norm. Matrices are Matrix (Fin d) (Fin d) ℝ, acting on vectors through Matrix.toEuclideanLin. The square root is Mathlib's CFC.sqrt under the Loewner order (MatrixOrder). The pseudo-inverse is the functional calculus of with , and is written as . Mathlib's matrix inverse is used only where the matrix is invertible or the vector is zero. Rounds are 1-based and . The losses and are real-valued convex functions, and the constraint is carried by . Each update's argmin is a predicate (the next iterate lies in and minimizes the objective there), which does not assert existence or uniqueness. A run consists of the rounds of Figure 2, with the subgradient relation imposed in every round. The subgradient relation is the platform's published ShorNonsmooth.AlmostDiff.IsSubgradient.
Restrictions and conventions, each stated in the item that needs it:
A formalization in which the next iterate need not lie in , the comparator ranges outside , is itself or its entrywise square root, or is Mathlib's matrix inverse (which vanishes on singular matrices), states a different theorem and is excluded.
Proofs need the convex-analysis optimality conditions for the two updates, the Loewner-order calculus of CFC.sqrt on real matrices (Lemma 13), concavity and differentiability of , and limits in the functional calculus. The matrix lemmas (13, 14, 8, 9, 10) are reusable outside this paper. Alternative proofs, for instance of Lemma 10 through operator concavity, are welcome.
Policy gradient methods optimize a parameterized policy directly by gradient ascent on its expected discounted return. They underlie most practical reinforcement-learning systems, yet for a long time their convergence was understood only locally: the objective is not concave, and plain gradient ascent can stall on plateaus. The natural policy gradient (NPG) of Kakade (2001) preconditions the gradient by the pseudoinverse of the Fisher information matrix of the policy, so that steps are measured in the geometry of the induced action distributions rather than in parameter space. NPG is the conceptual ancestor of trust-region methods such as TRPO and PPO.
Agarwal, Kakade, Lee and Mahajan (arXiv:1908.00261v5, JMLR 2021) prove that exact NPG with softmax policies converges to the optimal value at rate , with constants that depend on neither the number of states, nor the number of actions beyond , nor any distribution mismatch coefficient. This mission formalizes that result, Theorem 5.3 of the paper, and the lemmas its proof rests on.
Timeline. Kakade (2001) introduced NPG and observed that, for softmax policies, it moves toward the greedy policy. Kakade and Langford (2002) proved the performance difference lemma. Even-Dar, Kakade and Mansour (2009) analyzed experts algorithms in changing MDPs, whose regret argument this proof adapts; Geist, Scherrer and Pietquin (2019) studied regularized policy iteration with related rates. Agarwal et al. (preprint 2019, journal 2021) gave the dimension-free bound formalized here.
A finite discounted MDP consists of finite sets (states) and (actions, nonempty), a transition kernel , rewards and a discount factor . A policy assigns to each state a distribution over actions. Its value is the expected discounted sum of rewards started from ; for a start distribution , . The state–action value is and the advantage is . The discounted state visitation distribution is
An optimal policy has for every policy and every state ; write .
The softmax policy with parameter is . The Fisher information matrix with respect to is
and the NPG update with step size is
where is the Moore–Penrose pseudoinverse and are the quantities of . Following §5.3, every state is assumed reachable from : for each some policy has . The normalizer appears in the lemmas.
For NPG (15) from with any fixed , for all ,
If moreover and , then for every .
The result. Theorem 5.3 is a global, non-asymptotic guarantee for a non-concave policy optimization problem, with no dependence on and no distribution mismatch coefficient: the same analysis does not go through for plain softmax policy gradient, whose rates in the same paper carry such coefficients or are only asymptotic. It explains why Fisher preconditioning helps, and it is the template for the paper's later analysis of NPG with function approximation (§6) and for subsequent work on linear convergence of NPG and on entropy-regularized variants.
Formalizing it. The theorem is proved on paper; no machine-checked proof is known. A formal development needs: a policy-gradient identity for softmax policies, the computation of the Moore–Penrose pseudoinverse of a singular, block-structured Fisher matrix acting on the policy gradient, the performance difference lemma in the unnormalized convention, and a telescoping regret argument with Kullback–Leibler divergences between action distributions. Each of these is reusable: the performance difference lemma and the visitation-distribution calculus serve every result of the paper and much of the reinforcement-learning literature.
The obvious approach, treating NPG as gradient ascent on a smooth objective, fails: is non-concave and its smoothness constant grows with , which would give a rate depending on the state space and on distribution mismatch. The dimension-free rate comes only after the NPG step is rewritten exactly as a multiplicative-weights update on each state's action distribution, and this rewriting is itself delicate. The Fisher matrix is always singular (each state's block annihilates the all-ones vector), the pseudoinverse returns the minimum-norm solution, which is not but differs from it by a state-dependent offset; and the identity holds at a state only if that state carries positive visitation weight, which is why reachability from is assumed. A newcomer's first idea, replacing by "any solution of " or by an ordinary inverse, does not define the algorithm.
Lean conventions (Mathlib, namespace PolicyGradTheory.NPG):
S → A → ℝ (π s a ) satisfying the published IsPolicy; transitions P s a s' ; values, -functions and state occupation probabilities are the published FoundationsML definitions PolicyValue, QFunction, OccupationDist, and optimality is IsOptimalPolicy. is the value of a policy assumed optimal, never a supremum over arbitrary functions.EuclideanSpace ℝ (S × A), so norms are Euclidean and gradient is .VectorSpaceOpt.IsPseudoinverse (minimum-norm least-squares inverse, which on Euclidean space is the Moore–Penrose pseudoinverse); Mathlib has none.The goal does not assume the soft-policy-iteration form, the improvement bound or monotonicity; those are milestones to be proved, and a statement taking any of them as a hypothesis would not be Theorem 5.3. The parameter form "" of Lemma 5.1 is not stated, since the pseudoinverse step differs from it by a state-dependent offset (as the lemma's own proof on p. 70 shows); only the policy form, which is invariant to that offset, is a target.
Contributions welcome: the softmax policy-gradient identity and score-function formula, existence and uniqueness of the minimum-norm least-squares inverse on Euclidean space, Kullback–Leibler identities for finite distributions, and the summability facts behind the visitation distribution.
Many counting problems in probability, combinatorics and statistics ask for the law of the number of occurrences of rare, weakly dependent events: long head runs in coin tossing, matching segments between two DNA sequences, isolated vertices or small subgraphs in a random graph, clusters of points in a scan statistic. Chen's 1975 adaptation of Stein's method gives an explicit error bound for approximating such a count by a Poisson law. Arratia, Goldstein and Gordon (Ann. Probab. 17 (1989) 9–25) recast it in terms of a neighbourhood of dependence for each event. In this form the error bound needs only the first two moments of the indicators whenever each event is independent of the events outside its neighbourhood. The paper's examples (head runs, DNA sequence matching, birthday-type problems) made this form standard in applied probability.
The paper has two main results. Theorem 1 bounds the distance between the law of the total count and a Poisson law; it is essentially contained in Chen (1975). Theorem 2, which the authors describe as new, is a process version. It compares the joint law of all the indicators, that is, where the events occur, with a Poisson process. Theorem 3, a corollary, compares a dependent family of events with an independent family having the same marginal probabilities. This mission formalizes Theorem 2, the finite-dimensional bound it is derived from, the steps of its proof in §6, and Theorem 3.
Let be a probability space and an index set. For let be a Bernoulli random variable, , with
For each fix a set with , the neighbourhood of dependence of . Put and
Roughly, measures the size of the neighbourhoods, the expected number of neighbours of an occurrence, and the dependence between an event and the events outside its neighbourhood. In many applications is independent of , so .
The dependent Bernoulli process is , a random element of . The Poisson process on with intensity is with the mutually independent and Poisson with mean .
Distances are measured in the paper's total variation norm,
which is twice the usual total variation distance.
The bound has no dependence on and no assumption on beyond countability (which the setting forces).
The result. Theorem 2 says that when , , are small, the set of indices at which the dependent events occur is close in law to a Poisson process with the same intensity. The bound covers every event about the locations, not just the total count. It is in the strong total variation norm and needs only moment information when . Theorem 3 turns this into a decoupling statement: a dependent family of rare events is almost indistinguishable from an independent family with the same marginals. The process bound is the form used when the positions of rare events matter, for example in the distribution of the location of the longest match in sequence comparison and in scan statistics.
Formalizing it. The results are proved in the paper; none is machine-checked. A formal development would give a Lean statement and proof of a Chen–Stein bound with explicit constants, for countable index sets and arbitrary dependence. It would also include the coordinatewise Stein operators on and the bounds on their solutions, which are reusable for other multivariate Poisson approximations. A companion mission formalizes Theorem 1, including Lemma 1 (the bounds on the one-variable Stein solution) on which milestone 2 rests.
The total variation distance between two laws on cannot be bounded coordinate by coordinate, because the are dependent. The one-variable Stein equation controls only the law of a single integer-valued statistic. The paper passes through finite-dimensional block sums and replaces the coordinates one at a time. At each replacement the error has to be charged to the terms of indexed by the current block, so that the total over all blocks reproduces without a factor . Two further points need care. First, the bound is the only one available for differences in a coordinate other than the one being replaced; this is why the constants are larger than in Theorem 1. Second, the infinite index set requires a limiting argument from finitely many blocks to the full process.
MarkovChainCLT.tvDist (supremum over measurable sets of ). Dropping the factor would make the goal twice as strong and false in general.tsums, equal to the true sums almost surely. A partition is a surjection (Fin d), so Lean's coordinate 0 is the paper's coordinate .Needed infrastructure: product measures and independence on , Poisson laws (Mathlib's poissonMeasure), conditional expectation, and a one-variable Stein bound (Lemma 1). Contributions of proofs of any milestone, of the general step of §6, and of the one-dimensional Lemma 1 are welcome.
Counts of rare events often look Poisson even when the events are dependent. For example, a local pattern in a random graph can overlap another copy of the pattern, so the corresponding occurrence indicators are not independent. The useful question is quantitative: how far is the distribution of the total count from a Poisson distribution with the same mean? Arratia, Goldstein and Gordon give a bound in terms of three quantities that can be estimated from neighbourhoods of dependence. Their 1989 paper applies the Chen–Stein method to the count and then to the full point process. This mission concerns the count bound, Theorem 1.
The authors explain that the result is essentially contained in Chen’s earlier work, while their one-variable proof prepares the process result in Theorem 2. The bound remains useful as a precise statement of the dependence conditions under which the Poisson approximation works. The process theorem belongs to the companion mission.
Let index Bernoulli indicators , each taking values in on a probability space with law . Write , and let
For each , choose a dependence neighbourhood containing . The neighbourhoods need not be symmetric, and the theorem imposes no independence condition: dependence on indicators outside is measured directly. Define and
The remaining quantities use conditional expectation. Let , and let be the sigma algebra generated by all outside . Put
Conditioning on the count retains less information than conditioning on all far indicators, so . Let have the Poisson law with mean . The paper defines as twice the usual supremum over events: .
The goal is the complete four-clause statement of Theorem 1, including its strict final inequality:
The intermediate targets are the Stein-operator inverse identity, the bound on a telescoping term, display (11) relating the approximation error to , and the two clauses of Lemma 1. The goal keeps the coefficients and both forms of fixed, as the paper states them.
The result reduces a distributional approximation question to local sums of probabilities and conditional-dependence errors. When , and are small, the entire law of the count is close to its Poisson comparison law, and the probability of no occurrence has its own sharper bound. The latter is useful whenever a model asks whether at least one rare event occurs. The result applies without demanding exact independence outside the chosen neighbourhoods; the residual dependence appears in .
The paper proves these results. The formalization task is to give the known estimates machine-checked statements and proofs with the constants and probability conventions exposed. Mathlib supplies the Poisson measure and conditional expectation, while the mission adds the paper-specific neighbourhood sums and Stein operators. The formalized theorem can be reused for count approximations in other dependent-indicator models once those models supply bounds on the three error quantities. No machine-checked proof is claimed here: the theorem items are proposed targets with sorry bodies.
A first approximation based only on misses overlapping event pairs. Bounding pair dependence through alone also misses dependence between one indicator and the aggregate of far indicators. The authors' third term measures that remaining effect by conditional expectation. The proof must control the Stein solution uniformly while preserving its precise constants; replacing that control with a qualitative bound would not recover Theorem 1. In the countably infinite setting, the sums and conditional expectations also require careful handling of convergence and measurability. The proof of Lemma 1 is attributed in the paper to Barbour and Eagleson; it is a substantive target here rather than an assumed bound.
The Lean index type is countable. Under the paper's assumptions and , only countably many indices can exist, so this representation retains the stated probabilistic setting. Indicators are measurable natural-number-valued functions with values at most one. The parameter is a positive real equipped with the exact HasSum statement for the probabilities. The Poisson law is Mathlib's poissonMeasure at converted to a nonnegative real parameter.
The sums defining use extended nonnegative reals, so divergence becomes rather than the real tsum default zero. The random counts and use natural-number tsum; their divergent-input default can occur only on a null set under the finite-mean hypotheses and therefore does not change their laws. Measurability of these counts follows from countability and measurability of each indicator. The far-field sigma algebra is generated by the measurable indicators, and the formalization checks that it lies below the ambient sigma algebra, avoiding a default-zero conditional expectation. The paper's total variation norm is exactly 2 * MarkovChainCLT.tvDist, with the factor two retained.
The source writes a strict final inequality without discussing infinite error sums. The Lean statement conditions that single strict clause on ; otherwise both sides can be infinite and strict comparison is false. The other three clauses allow infinite bounds, as the source does. Lemma 1 fixes the Stein inverse at zero exactly as the paper chooses and uses explicit pointwise sup-norm bounds over all nonnegative integers. Display (11) allows , a strengthening of the displayed case. These choices rule out loss of the norm's factor two, disappearing divergent sums, default-zero mapped measures or conditional expectations, and an unannounced independence assumption.
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.
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.