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?
The proximal map of a convex function is the basic building block of proximal-point, forward–backward, Douglas–Rachford and ADMM methods, which are used throughout large-scale convex optimization, signal processing and operator splitting. All of these methods treat as a nonexpansive operator and use the fact that it is a gradient. The questions this mission formalizes go back to the paper that introduced the map: J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), 273–299 (DOI 10.24033/bsmf.1625). Which maps are proximal maps, and how can a function be recognized as the "potential" of one?
Moreau's answer (Corollaire 10.c) is intrinsic. A map is a proximal map exactly when it is nonexpansive and selects, at every point, a subgradient of some convex function. This characterization is the Hilbert-space origin of later results on firmly nonexpansive operators and on resolvents of maximal monotone operators (Minty 1962; Rockafellar 1970). It is still how one checks that a given nonexpansive operator is a proximal map.
Throughout, is a real Hilbert space with inner product and norm .
The Lean names are GammaZero, conj, subgrad, IsProx, prox, IsProxMap, ContractsDistances, primitive, LessConvexThanQ, MoreConvexThanQ and IsProxPrimitive, all in the namespace MoreauProx.Characterization.
For every map ,
Nothing is assumed of beyond convexity.
Three further results of the paper are included as unmilestoned companions: Proposition 8.a ( implies ), Proposition 9.a ( is the only function equal to its dual) and Proposition 9.d (nonnegative combinations of prox maps with are prox maps).
The result. Corollary 10.c turns "is a prox map" into two checkable properties of , one metric and one variational, with no need to exhibit . Proposition 9.d is one consequence: closure of prox maps under subconvex combinations. Proposition 10.b gives the dual picture, which recognizes primitives of prox maps among the functions of by a Lipschitz condition on their subdifferential. The intermediate results are the standard toolkit of proximal analysis. They include the Moreau decomposition, the nonexpansiveness of , and the smoothness of the Moreau envelope (Remark 7.c) with gradient .
Formalizing it. All statements were proved in 1965 and are textbook material (Bauschke–Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., 2017, Ch. 12–14 and 24). None of them has a machine-checked proof in Mathlib, which has no class, no extended-valued Fenchel conjugate and no proximal map on a Hilbert space. A complete development here would give reusable infrastructure: the conjugate of extended-valued functions with the Fenchel–Moreau theorem, the proximal map and its nonexpansiveness, and the differentiability of the Moreau envelope. Downstream convergence proofs of proximal algorithms need this layer.
The necessity half of 10.c follows quickly from 5.b and 7.d once those are available. The sufficiency half is the hard one. Given only a nonexpansive and a convex with , one must produce with . The obvious move is to take to be something built from directly. This fails because the candidate is only defined through a duality that needs and a precise convexity comparison with . Neither is given, and neither follows from a pointwise argument. The intermediate milestones involve biconjugation of extended-valued functions, upper envelopes of affine functions in infinite dimension, and lower semicontinuity of functions taking . These are the places where finite-dimensional or finite-valued shortcuts do not apply.
Conventions committed to in Lean:
[NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]. Functions with values in are H → EReal.⨆ x, (⟪x, y⟫ : EReal) - f x, computed in EReal (a complete lattice).IsProx f z x says that minimizes . The function prox f picks such a minimizer by choice (junk value if none exists). Every theorem using prox assumes . A prox map is ∃ g, GammaZero g ∧ ∀ z, IsProx g z (p z).ConvexOn ℝ Set.univ). This is equivalent to the paper's -valued , because a subgradient at every point forces finite everywhere. The contraction condition is §10.a applied to .Trivializing formalizations are ruled out. The goal's is required to be convex and to have as a genuine subgradient at every point, with finite. excludes the constant , under which every point would minimize the proximal objective. No theorem applies prox outside , where its junk value would make statements vacuous.
Needed infrastructure: Fenchel–Moreau biconjugation for EReal-valued functions on a Hilbert space, existence of minimizers of coercive lsc convex functions (weak compactness of balls), and a Fréchet-derivative argument for the envelope. Contributions are welcome at every milestone. Also welcome are helper lemmas on EReal arithmetic for convex functions, and alternative proofs of 10.c via Minty's theorem on firmly nonexpansive maps.
Theorem 2.1 (the previous mission in this series) shows that the closed convex hull of a union of polyhedra has a compact description after lifting to a higher-dimensional space. That description comes in two dual flavors: a primal one, as the projection of an explicit lifted polyhedron, and a polar one, characterizing the hull's facets directly via a cone built from the disjuncts' own data. Both flavors matter in practice: a cutting-plane algorithm needs to know exactly which inequalities are facet-defining (so as not to waste effort generating redundant cuts), and the two routes — projection and polarity — offer complementary tools for deciding this. This mission formalizes both routes and the machinery connecting them, closing out Chapter 2 of Balas, Disjunctive Programming (Springer, 2018).
The projection route (§2.2–2.3) develops general facts about projecting an arbitrary polyhedron that predate and underlie the disjunctive-programming application: the classical projection formula via extreme rays of a projection cone, how dimension and facet structure behave under projection, and a refinement (via a coordinate transformation) that eliminates the redundant inequalities the plain projection formula can produce. The polarity route (§2.4) develops the reverse polar, an object introduced by Balas specifically for this purpose, whose iterated application recovers the closed convex hull of a disjunctive set directly, culminating in an exact characterization of when an inequality is facet-defining purely in terms of extreme rays of an explicit cone .
For a matrix system with rows, let , and let be its projection onto the -space. The projection cone is . A vector is an extreme ray of a cone if , , and the ray it generates is an extreme subset of . The dimension of a polyhedron is the dimension of its affine hull, and a set is a facet of if it is a proper face of of dimension . Partitioning 's rows into those tight throughout (the equality subsystem) and the rest, and denote the rank of the tight rows' combined and -only submatrices, respectively.
For , the polar is and the reverse polar is ; more generally the scaled polar at level is . For a disjunctive set with and , the cone .
For a full-dimensional disjunctive set () and :
Proposition 2.13 ( bounded), Theorem 2.14 ( when ), Corollary 2.15 (), Theorem 2.16 (the scaled polar stabilizes: ), and Corollary 2.17 () — each the weakest statement needed for the next.
Theorem 2.5 (), Proposition 2.6 (projection preserves integrality), Theorem 2.7 (), Corollaries 2.8–2.10 (facet/face behavior under projection), and Proposition 2.11 / Corollary 2.12 (sharper facet characterizations via a coordinate-transformed projection cone).
The results themselves. Theorem 2.18 is the practical payoff of the entire polarity apparatus: it turns "is this inequality facet-defining for the convex hull of a union of polyhedra" from a geometric question into an algebraic one about extreme rays of an explicit, finitely-generated cone built directly from the disjuncts' own constraint data — exactly the kind of question a cutting-plane algorithm needs answered to avoid generating redundant cuts. The projection track is foundational general polyhedral theory in its own right (Theorem 2.5's formula underlies Benders decomposition and classical Fourier-Motzkin elimination as special cases, per the book's own remarks), independently useful beyond the disjunctive setting.
Formalizing it. No object in this mission — polars, reverse polars, projection cones, extreme
rays of a cone, or the dimension/facet apparatus of a polyhedron — exists on the platform prior to
this mission or in Mathlib (a q=polar search returns only an unrelated cyclic-polytope
construction from the Hirsch-conjecture series, with different conventions and object). This
mission restates the disjunctive-set vocabulary of the companion ConvexHull mission locally
(per the series convention that a draft mission cannot import another draft mission's
definitions) and builds the polarity apparatus from scratch on top of it.
The natural first attempt at Theorem 2.18 tries to characterize facets of directly from the lifted-polyhedron representation of Theorem 2.1, projecting facet by facet. This misses the point of the polarity route entirely: Theorem 2.18's proof instead goes through , showing a vertex of corresponds to a nonhomogeneous subset of rank of 's own defining system being tight — algebra entirely in the dual space of multipliers, never touching the lifted polyhedron's facets directly. The two obstacles Theorem 2.14 and Proposition 2.13 exist to clear are, respectively: reverse polars do not satisfy the ordinary polar's clean involution property (an extra summand appears, capturing recession directions the reverse-polar construction alone cannot see), and reverse polars are either empty or automatically unbounded (never merely "small"), which is why the apparatus needs the normalization throughout.
All results are stated over finite index sets and matrices Matrix (Fin (m h)) (Fin n) ℝ
(disjunctive-set data, m : Q → ℕ dependent) or Matrix (Fin m) (Fin p) ℝ /
Matrix (Fin m) (Fin q) ℝ (projection-track data). PolyDim and IsFacet are stated generically
over any real vector space (via Module.finrank of vectorSpan and Mathlib's IsExtreme), so the
same definitions serve both Poly2-shaped pairs and cl conv F ⊆ Fin n → ℝ directly in Theorem
2.18. IsExtremeRay is likewise stated generically, reused for cones in plain vector space,
(v,v0)-space, and the triple (v,w,v0)-space Proposition 2.11 needs.
Two results (Proposition 2.11, Corollary 2.12) build on a coordinate-transformed polyhedron
Q̃/cone W̃ that the book itself only cites from [14] rather than constructing; consistent with
the book's own treatment, this mission takes W̃ (or its (v,v0)-projection) as given data
together with its defining relationship to Proj_x(Q), rather than re-deriving the transformation
— a choice recorded in MODERATION_NOTES.md, not a weakening of either statement's content.
Proposition 2.11's complexity remark ("O(max{m,q}³)") is a proof aside about the transformation's
cost, not part of either result's mathematical claim, and is out of scope per the book-wide
disposition (triage.json).
A trivializing formalization is ruled out explicitly: the projection-track results are stated for
generic m, p, q, never fixed at small values, and Theorem 2.18 is stated for a generic finite
disjunctive index set Q, not specialized to |Q| = 1 (which would collapse W_0 to ordinary
LP polarity and prove nothing about unions).
Classifiers trained to high standard accuracy on image benchmarks can be made to fail by perturbations of the input that are small in the norm (Szegedy et al., 2014; Goodfellow et al., 2015). Adversarial training reaches high robust accuracy on the training set, but on CIFAR10 the robust accuracy on held-out data is much lower than on the training set (Madry et al., 2018). That is, robust generalization fails.
Schmidt, Santurkar, Tsipras, Talwar and Mądry (arXiv:1804.11285) ask whether this is a statistical phenomenon: does learning a robust classifier need more samples than learning an accurate one, even in the simplest distributional model? This mission formalizes their answer for a mixture of two Gaussians. In that model, with and , a single sample suffices for standard generalization (their Theorem 4). Robust generalization, by contrast, needs a number of samples that grows polynomially with the dimension, for every learning algorithm.
Write for the feature space and for the labels.
For every learning algorithm , every and every ,
For every learning algorithm , every and every ,
Corollary 23 is the goal because it is the statement the paper advertises: its main-text Theorem 6 is Corollary 23 with .
In the same model with and of order , a single sample suffices to reach standard error below 1% (Theorem 4 of the paper), and on the order of samples suffice for robust error below 1% when is below a small constant (Theorem 5; Corollary 22, formalized in mission 3 of this series). Corollary 23 shows that, up to the logarithmic factor, no learner can do better. Robust generalization then needs times as many samples as standard generalization. The gap is information-theoretic: it concerns every algorithm, not a particular training procedure or model class. The authors present this as a candidate explanation for the robust-generalization gap observed on CIFAR10. The ½ is tight: a constant classifier attains it.
The paper's proof is complete and short. As far as a search of the platform shows, none of its statements has been formalized. A machine-checked version requires multivariate Gaussian conjugacy, Gaussian convolution identities, the outer-measure robust event, and a union bound for the maximum of Gaussians. The Gaussian conjugacy and convolution facts are standard and appear throughout Bayesian statistics. As of this Mathlib version they are not available for stdGaussian on EuclideanSpace.
The obvious attempt fixes and bounds the robust error for each . That fails: a learner may ignore the data and output the Bayes-optimal robust classifier for one fixed , so for each some learner does well. The lower bound holds only on average over the prior on . The classifier depends on the samples, and the samples depend on , so the classifier and the test distribution are correlated through . A second obstacle is measure-theoretic. The robust error of a classifier is the probability of an -thickening of an arbitrary set . Such a set need not be Borel, and it must be bounded below with no structure on the classifier beyond what the learner provides. The same statement with the ball is a different theorem.
EuclideanSpace ℝ (Fin d) with its Borel σ-algebra; is Mathlib's stdGaussian; is its image under , so every Gaussian parameter in the development is a standard deviation.Bool, with true for . A classifier is ℝ^d → Bool, and a learning algorithm is (Fin n → ℝ^d × Bool) → ℝ^d → Bool.Bool; samples form the product measure Measure.pi.A formalization that fixes instead of averaging over the prior, that restricts the learner (to linear classifiers, or to classifiers that do not depend on the data), that uses the ball, or that assumes the posterior formula as a hypothesis states a different theorem. These are ruled out by the definitions file.
Needed infrastructure: the multivariate Gaussian conjugacy and convolution identities for stdGaussian pushforwards, translation invariance of outer measure under Gaussian shifts, and a sub-Gaussian tail bound for one coordinate. The Gaussian identities are reusable well beyond this mission. Contributions of general Gaussian lemmas, stated for stdGaussian on any finite-dimensional inner product space, are welcome. Related platform work: missions 2–4 of this series formalize the Bernoulli-model lower bound and the two upper bounds of the same paper.
Proximal maps are the basic building block of first-order methods for nonsmooth convex optimization: the proximal point algorithm, forward–backward splitting (ISTA/FISTA), Douglas–Rachford splitting and ADMM all proceed by evaluating maps of the form . The notion and its name come from J.-J. Moreau, who introduced proximal points in two 1962 notes in the Comptes rendus and gave the systematic theory in Proximité et dualité dans un espace hilbertien (Bull. Soc. Math. France 93 (1965), 273–299).
The central result of that paper, which Moreau calls the key proposition, links proximal maps to conjugate duality: every point of a Hilbert space splits uniquely into the proximal point of relative to a convex function plus the proximal point relative to its dual function. The identity is used throughout modern optimization, for example to compute the proximal map of a norm from the projection onto the dual-norm ball, and in the analysis of primal–dual splitting methods.
Timeline. Moreau (1962) announces proximal points and the decomposition along mutually polar cones. Moreau (1965) proves the general decomposition theorem for and derives from it the characterization of proximal maps and the maximal monotonicity of subdifferentials in Hilbert space. Rockafellar (Pacific J. Math. 33 (1970)) extends maximal monotonicity of subdifferentials to Banach spaces.
Let be a real Hilbert space with inner product and norm . Functions take values in the extended real line .
The class consists of the functions that are convex (their epigraph is convex in ), lower semicontinuous, and not identically .
The dual function of is
Two points and are conjugate with respect to and when ; the set of such is the subdifferential .
For and , the proximal point is the unique minimizer of
When is the indicator function of a nonempty closed convex set (zero on , outside), is the nearest-point projection .
Let and . For all ,
The decomposition theorem gives, for every , a unique splitting into a pair of conjugate points, and conversely identifies every conjugate pair summing to with the two proximal points. Special cases are the orthogonal decomposition along a closed subspace and its complement, and the decomposition along a pair of mutually polar cones (Corollaire 4.b). In the rest of Moreau's paper it yields that proximal maps are nonexpansive, that the Moreau envelopes of and add up to , and that the subdifferential of a function in is maximal monotone (Proposition 12.b). In algorithms it lets one evaluate from at no extra cost, which is the basis of dual and primal–dual proximal methods.
All results in this mission are classical and proved (Moreau 1965; see also Bauschke–Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., 2017, Thm. 14.3). What the mission adds is a machine-checked development. Mathlib contains convex functions, lower semicontinuity and Hilbert-space projections onto closed convex sets, but as of this mission's environment it has no Legendre–Fenchel conjugate for extended-valued functions on a Hilbert space, no proximal map and no maximal monotone operators. The Hilbert projection theorem is on the platform as FamousTheorems.hilbert_projection_theorem; it is the special case of Proposition 3.a for indicator functions.
The two directions of the goal are unequal. That conjugate points summing to are the two proximal points needs only the definition of the dual function. The converse must produce the conjugacy identity from the bare fact that minimizes , and a pointwise first-order argument is unavailable because need be neither finite nor differentiable anywhere.
The milestones carry the analytic weight. Proposition 3.a needs existence of a minimizer of a function that is neither continuous nor coercive by itself on an infinite-dimensional space, so compactness arguments in the norm topology fail. Biconjugation (§2.b) is the Fenchel–Moreau theorem, which requires a separation theorem in applied to a closed convex epigraph whose values may be .
Everything lives in the namespace MoreauProx.Decomposition, over {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]; the paper's is ⟪x, y⟫_ℝ. The following conventions are committed to:
H → EReal. (GammaZero) is the structure: never ⊥, not everywhere ⊤, convex epigraph in H × ℝ, and LowerSemicontinuous in the norm topology. The paper defines as suprema of nonempty families of continuous affine functions, other than , and states the equivalence with this description (§2.a); the second description is the one formalized. Weak and strong lower semicontinuity agree for convex functions, as the paper remarks, so no weak topology appears.conj f y = ⨆ x, ⟪x, y⟫_ℝ - f x in EReal; since a - ⊤ = ⊥, this matches both lines of (2.2).IsProx f z x: minimizes proxObjective f z u = ‖u - z‖ ^ 2 / 2 + f u. With Proposition 3.a it is equivalent to the paper's notation; no choice function is used.GammaZero f and g = conj f; the paper's " dual to each other" follows from this by §2.b, so the goal is not weaker than the paper's.innerDual), and is the predicate IsProj C z x (nearest point).A formalization that drops the requirement that be not identically , drops the factor , replaces the duality hypothesis by unrelated , or reads values through EReal.toReal would make the statement false or vacuous; the definitions above rule these out.
Contributions welcome: proofs of the three milestones and of the goal; reusable infrastructure for extended-valued convex analysis on Hilbert spaces (conjugates, subdifferentials, proximal maps), which the companion mission Proximité et dualité dans un espace hilbertien II builds on.
The generalized assignment problem (GAP) asks for the cheapest way to give each of tasks to exactly one of agents when every agent has a limited amount of a resource and different agents consume different amounts of it for the same task. It models assigning jobs to machines or computers, software tasks to programmers, commercials to time slots, and customers to single-source plants in capacitated facility location. The problem is NP-hard, so exact methods rely on lower bounds that are cheap to compute and strong enough to prune a branch and bound tree.
G. Terry Ross and Richard M. Soland (Mathematical Programming 8, 1975) gave such a bound. The relaxation that ignores the resource limits is solved by giving every task to its cheapest agent; the overloaded agents are then repaired by one small binary knapsack problem each, whose optimal values are added as penalties. Their paper then shows that this repaired bound is not an ad hoc heuristic: it is exactly the value of a Lagrangean relaxation of the GAP at an explicit choice of multipliers. This identity made the Ross–Soland bound the reference point for the later Lagrangean and column-generation methods for the GAP (for example Fisher, Jaikumar and Van Wassenhove, Management Science 1986 and Savelsbergh, Operations Research 1997).
Agents are and tasks . Giving task to agent costs and uses units of agent 's resource; agent has units. The problem is
Dropping the resource constraints gives the relaxation (PR). It is solved by choosing, for each task , a cheapest agent with and setting ; its value is . Let be the tasks this solution gives to agent , the overloaded agents, and the excess of agent . The penalty of moving task away from is . For the binary knapsack problem
chooses the cheapest set of tasks to move off agent ; call its optimal value . The knapsack bound is
Dualizing the assignment constraints with multipliers gives the Lagrangean relaxation
Finally and are the smallest and second smallest of , counted with multiplicity.
For every cheapest-agent choice and every choice of optimal knapsack solutions,
the minimum being attained, and consequently for every feasible for (P). This is the paper's "principal result of this Lagrangean analysis" (§2, p. 96). It has no constants to improve; it is an identity between two optimization problems.
In the paper's order of use: (PR) is solved by the cheapest agents (pp. 93–94); every lower bound on (PR) is a lower bound on (P) (p. 95); (PR) separates into one binary knapsack per agent (p. 95); at the variables that are zero in the (PR) solution can be fixed at zero, the substitution turns agent 's part into (PK), , and agent 's part has value (p. 96). Two side results close the section: the solution obtained by moving the tasks the knapsacks select has cost exactly LB, so it is optimal whenever it is feasible (pp. 94–95); and the optimal dual multipliers of the bounded-variable linear program (PR) are exactly the vectors with (pp. 95–96).
The identity says that a bound computed from one sorting pass and a handful of small knapsacks equals a Lagrangean dual bound at a closed-form multiplier. Validity of LB for (P) then follows from weak Lagrangean duality alone, and the multiplier is the upper end of the range of optimal dual multipliers of the linear program (PR), which the paper singles out as a suitable choice of multipliers. The rebuilt solution gives the algorithm a feasible incumbent at no extra cost whenever the knapsack repairs happen to respect all budgets.
The result is proved in the paper, in one sentence. The mission turns that sentence into checked statements: the separation of (PR), the reduction of each agent's subproblem to (PK), the handling of ties among cheapest agents, and the role of nonnegative resources. As far as a search of the platform shows, nothing about the generalized assignment problem or its Lagrangean bounds has been formalized; the definitions here (assignment relaxations, per-agent knapsacks, bounded-variable duals) are reusable for other GAP and facility-location missions.
The Lagrangean relaxation at is a larger problem than the knapsack bound suggests: a feasible may give a task to several agents or to none, and may use any agent, not only the cheapest one. The knapsack bound, by contrast, only looks at the tasks each agent receives in the (PR) solution. The paper bridges the two in one sentence of three observations, and each observation depends on a condition the sentence does not state: the sign of the resource coefficients, the treatment of agents that are not overloaded (for which no knapsack is solved), and ties among cheapest agents, which make some penalties zero and require the statement to hold for every tie-break. An inequality in one direction only (LB is a valid bound) is not the claim; the equality needs a feasible point of (PR) whose value is exactly LB.
Agents are Fin m and tasks Fin n, indexed from 0. Costs, resources, budgets, multipliers and variables are real numbers; a 0-1 variable is a real equal to 0 or 1, so the paper's sums are literal. The cheapest-agent selection is an arbitrary function a : Fin n → Fin m with IsCheapest c a, so every statement holds for every tie-break. and are minima over the other agents, which requires (hm : 1 < m); is proved to be the second smallest cost with multiplicity. Optimal values are never encoded as sInf: is the objective of a given optimal knapsack solution, and "the bound provided by (PR)" is stated as a lower bound over all feasible points that is attained.
Standing hypotheses: (printed on p. 92), (implicit in "the resource required", and necessary: with a negative both (PR) and (P) can fall below LB), and . All costs are finite; the "not permissible" pairs of the paper's numerical example are outside the model.
A formalization that states only every (PR) value, or that restricts the (PR) competitors to the (PR) support or to at most one agent per task, would be a weaker theorem and does not meet the goal. The (PR) dual is written out explicitly with multipliers for the bounds ; "each optimal dual multiplier lies anywhere in the range " is read as "the optimal multipliers are exactly this box".
Needed infrastructure is only finite sums over Fin and Finset.inf'. Proofs of the milestones, and lemmas on separable binary programs that could serve other Lagrangean-relaxation missions, are welcome.
The random walk Metropolis algorithm is one of the most widely used Markov chain Monte Carlo methods for sampling from a density known up to a constant. Its one tuning parameter is the variance of the Gaussian proposal. If the variance is too small, the chain accepts almost every move but barely moves. If it is too large, it proposes long jumps that are almost always rejected. Practitioners need a rule for choosing it, and the rule has to work in high dimension, where both failure modes are severe.
Roberts, Gelman and Gilks (Ann. Appl. Probab. 7(1), 1997) gave the first rigorous answer for product targets. As the dimension grows, one coordinate of the suitably speeded-up chain converges to a Langevin diffusion. The speed of that diffusion is an explicit function of the proposal scale, and maximising it gives the rule "tune the proposal so that about 23% of proposals are accepted". This rule, and the 2.38/√I scaling behind it, is now standard advice in applied Bayesian statistics.
Let be a target density: positive, , integrating to one, with Lipschitz, and satisfying the moment conditions (A1) and (A2) . Here . In dimension the target is the product density on .
Fix a scale and set . The random walk Metropolis chain moves as follows. From it proposes . It sets with probability , and otherwise. The chain starts from , which is stationary for it. The speeded-up first coordinate is for .
Let be the standard normal distribution function, and define the roughness . The speed and the limiting acceptance rate are
The Langevin generator is . It generates the Langevin diffusion .
As ,
where denotes weak convergence in the Skorokhod topology, has density , and is the Langevin diffusion with speed . The limit is asserted to exist. No constants appear in the statement beyond those the model defines.
Theorem 1.1 shows that, run for times as many steps, the chain in dimension looks like a fixed one-dimensional diffusion. The algorithm's cost therefore grows linearly in dimension, and its efficiency is measured by the single number . Corollary 1.2 turns this into the 0.234 acceptance-rate heuristic and the scaling. The same diffusion-limit method has since been applied to the Metropolis-adjusted Langevin algorithm, to Hamiltonian Monte Carlo and to non-product targets.
The theorem is proved on paper; it has no machine-checked proof. A formal development would give the first verified diffusion limit of an MCMC algorithm. It would also yield reusable components: the Metropolis chain on as a measurable random mapping, a martingale-problem characterisation of one-dimensional diffusions, and a Gaussian computation (Proposition 2.4) that recurs throughout the optimal-scaling literature.
The obvious approach, a Taylor expansion of the log acceptance ratio, gives a sum of terms of size . That sum does not concentrate uniformly over the state space, since the coordinates are arbitrary. The expansion is controlled only on the sets , where the empirical averages and are close to . The limit therefore holds only after showing that the chain rarely leaves over a time horizon of steps. A pointwise law of large numbers is not enough for that, because the bound has to survive a union over steps. Passing from generator convergence on a set of high probability to weak convergence of processes requires the Ethier–Kurtz convergence theory: a core for the limit generator, and convergence of processes that are not themselves Markov. None of this theory is in Mathlib.
All declarations live in the namespace Roberts1997.RWM. The following conventions are fixed.
Fin n → ℝ, and the paper's first coordinate is index 0. Its coordinates are the indices i ≠ 0.EthierKurtz_IsContinuousDiffusionLaw.The goal cannot be satisfied trivially. The limit law must exist, and it must be a probability measure whose initial marginal is , so the zero measure is excluded. The coupled copies must carry exactly the laws of the paths , not an arbitrary process with the same one-time marginals.
The statements carry the paper's hypotheses, with one exception. The printed proof of Lemma 2.6 bounds , which Theorem 1.1 does not assume, and under alone the uniform convergence over claimed by Lemma 2.6 fails (narrow spikes of far out let a positive fraction of the coordinates shift the log acceptance ratio by a constant while and stay close to ). Lemma 2.6 is therefore stated with the proof's own assumption, with bounded, named as an addition. Theorem 1.1 and the other results keep the paper's hypotheses.
A complete development needs several pieces not yet available: path spaces and the Skorokhod topology (or the coupling reading), the martingale problem and its well-posedness for Lipschitz drift, and the Ethier–Kurtz theorem on convergence of generators on sets of high probability. Proofs of the Gaussian milestones (Propositions 2.2 and 2.4, Lemma 2.5) and of Corollary 1.2 (ii) are independent of this infrastructure and are welcome contributions.
The stable set problem (vertex packing) asks for a largest set of pairwise non-adjacent nodes of a graph. It is NP-hard, and its polyhedral study, the description of the stable set polytope by linear inequalities, is one of the most studied topics of polyhedral combinatorics. Classes of valid inequalities (clique, odd hole, odd antihole, wheel constraints) and the graph classes they describe exactly (perfect, -perfect, -perfect graphs) organize much of that literature; see Grötschel, Lovász and Schrijver, Geometric Algorithms and Combinatorial Optimization (Springer, 1988).
Lovász and Schrijver (SIAM J. Optim. 1(2), 1991) introduced a general lift-and-project procedure for 0–1 programs: lift a relaxation into a space of matrices, impose linear conditions that every 0–1 point satisfies, and project back. One round of their operator gives a tighter relaxation that still contains every 0–1 point of ; rounds give the 0–1 hull. The procedure is an ancestor of the Sherali–Adams and Lasserre hierarchies, and the stable set problem is its first test case. This mission formalizes the paper's exact description of what one round of does to the fractional stable set polytope: it adds precisely the odd hole constraints.
Let be a finite graph with no isolated nodes, . Vectors of have a distinguished coordinate ; sits inside as the hyperplane , via .
For every finite graph without isolated nodes,
Theorem 2.3 gives a complete description of one round of on the stable set problem: the only new constraints are the odd hole constraints. Consequences:
The result has been proved since 1991. At the time of drafting, Prove2Me holds no formalization of it or of any part of the Lovász–Schrijver construction, and Mathlib has none. The mission produces a formal account of the operator on the stable set polytope and a formal proof of the walk criterion for two-variable systems.
The inclusion of in the odd hole system is a short argument once Lemma 1.3 is available. The reverse inclusion is the substance: given satisfying all odd hole constraints, one must exhibit a lifted matrix . A direct appeal to Farkas' lemma yields a certificate with no visible relation to odd cycles; the difficulty is to show that every obstruction to solvability of the matrix system forces a violated odd hole constraint, which is what Lemma 2.4 and the analysis of its four walk types accomplish. Case (d) of that analysis needs the odd hole constraints; the other cases need only the edge constraints. Lemma 2.4 itself is called folklore on the page and is stated without proof there.
A further point: Lemma 2.4 is stated for lower bounds , while the lower bounds that arise from the matrix system, , can be negative.
Option V, with none the coordinate . Graphs are Mathlib SimpleGraphs on a finite type with decidable adjacency. Every statement about a graph carries the paper's standing assumption that has no isolated nodes (∀ v, ∃ w, G.Adj v w).A trivializing formalization is ruled out: the goal is the set equality for every graph without isolated nodes, not the existence of a lifted matrix and not a single graph.
Not formalized here: the semidefinite operator , the operator , algorithmic statements (Theorems 1.6, 2.1, Corollary 2.5), and the set-function results of Section 3.
Reusable beyond this mission: the matrix cone layer (, , ), the stable-set cones, and the two-variable feasibility criterion of Lemma 2.4. Contributions of any of the milestones, and of general facts about polar cones of polyhedral cones in this setting, are welcome.
Retailers of seasonal goods sell at a full price first and mark down later. Customers who know this can wait for the markdown, and a firm that always has stock left for the markdown teaches them to wait. One remedy is to stock less than the low-price market would absorb, so that a customer who waits risks not getting the good at all. Liu and van Ryzin (Management Science 54(6), 2008) model this capacity rationing as a two-period game between a monopolist who chooses a stocking quantity and risk-averse customers who choose when to buy, and they characterize exactly when rationing is worth its cost in lost sales. The paper belongs to the revenue-management literature on strategic customers, where the firm's decision must anticipate the customers' best response to it.
A firm announces a price for period 1 and a lower price for period 2 and buys units at unit cost before sales start; there is no replenishment. A market of customers, each wanting one unit, has valuations drawn independently from a distribution ; from §3 on, is uniform on .
Period-2 requests are filled at random with probability , the fill rate, which customers anticipate correctly. Every customer has the same utility : strictly increasing, concave, twice differentiable, with ; from §3 on, with (smaller means more risk aversion). A customer with valuation buys in period 1 exactly when
The threshold separates early buyers from waiters.
Under the §3 assumptions, a cutoff is induced by the fill rate and the stocking quantity . The firm's profit from a segmented market is
and the profit from serving everybody at the low price is . The firm's optimal profit is the larger of and . The first-order condition of (6) is
with root , and the critical valuation bound is
In Lean these objects are IsCustomerUtility, buysEarly, cutoff (module LiuVanRyzin.Model) and fillRate, capacity, segProfit, lowPriceProfit, focLHS, criticalU (module LiuVanRyzin.PowerModel).
If , rationing is optimal: , maximizes on , and . If , serving the whole market at the low price is optimal:
The goal fixes no constants; it is the paper's dichotomy, stated with its own (7) and (8).
Proposition 3 answers the paper's central question: whether a firm facing strategic, risk-averse customers should deliberately under-stock. The answer depends on a single number, , which depends on prices, cost and risk aversion but not on the market size, and it is compared with the top of the valuation range. Corollary 1, the limits of Proposition 4, and the comparative statics of Propositions 6–8 on how the optimal fill rate moves with , and are all read off from it. The bounds of milestone 6 turn it into sufficient conditions stated in the primitives alone.
The results are proved in the paper's e-companion (Online Appendix C). No machine-checked proof of any of them is known. Formalizing them gives a verified instance of a pattern that recurs throughout revenue management: a customer best response (a threshold), a reduction of the firm's problem to one scalar decision, a concavity argument, and a comparison of two regimes.
Most of the work is analysis of real powers with a moving base. contains , whose derivative blows up at , so its concavity on the closed half-line is not a routine second-derivative computation at the endpoint. The regime comparison in Proposition 3 is not implied by Lemma 1: Lemma 1 locates the segmented optimum, but whether it beats depends on , which enters both through the prefactor and through . The equivalence of that comparison with requires eliminating with (7).
For Propositions 1–2 the utility is general: the threshold is defined by an inequality between and , and neither its monotonicity in nor its convexity under follows from a closed form. Only for is there one.
All quantities are real numbers. The utility of Propositions 1–2 is a function that is strictly increasing, concave and continuous on , twice differentiable on , with . The threshold is defined as the infimum of the set of early buyers, not assumed. Powers are Real.rpow; every power-model statement stays on , or on where appears. is written in the closed form (6). The root is a binder constrained by and (7), and milestone 4 shows such a root exists. "Increases" in Propositions 2 and 5 is read as strictly increasing.
Hypotheses the paper uses without stating them, added here:
The goal cannot be trivialized: is pinned to the root of (7), part 2 quantifies over every , and the optimum is compared with exactly as the paper defines optimality.
Contributions are welcome at every level. Useful ones include the real-power calculus lemmas behind milestones 3–6, a proof of Propositions 1–2 for general concave utilities, and reusable facts about thresholds defined by single-crossing inequalities.
Firms that sell new products (consoles, books, films) often take preorders before release. A preorder serves two purposes at once. It lets the firm charge early adopters a different price from later buyers, a form of price discrimination, and the number of preorders is advance demand information: an early signal of how large regular-season demand will be. Li and Zhang (MSOM 15(1), 2013) ask whether better advance information always helps a seller who runs a preorder, when consumers are strategic and anticipate the seller's stocking decision. Their answer is no. The second-period stocking decision improves, but the preorder price can fall. Whether the net effect is positive depends on the low-type margin and the size of the early-adopter segment.
This mission formalizes that answer, §4 of the paper: the preorder profit as a function of the demand correlation .
A seller sells a perishable product over two periods. High-type consumers, with valuation , arrive in the first period and may preorder at price . Low-type consumers, with valuation , arrive in the second period, when the price is . A high type who waits values the product at , where and . The unit cost is , with . Unsold units have no salvage value and unmet demand carries no penalty. Write .
The demands are jointly normal with correlation . The high-type demand has mean , and denotes its standardization, a standard normal variable. The low-type demand has mean , standard deviation and . Given , the updated low-type demand is normal with mean and standard deviation . and are the standard normal distribution function and density, and solves .
In the second period the seller charges and solves a newsvendor problem. It orders
and earns (2). A waiting high type believes half of the remaining consumers will be served before her, so her belief of product availability is
In the rational-expectations equilibrium every high type preorders at . The preorder profit is
The threshold is
The proposition splits the value of advance demand information into two effects with opposite signs. Better information always raises the second-period profit (milestone 5). Its effect on the preorder price depends on the margin. When , the seller stocks below the conditional mean. A more precise forecast then raises the stock and the availability , and waiting becomes more attractive, which lowers the preorder price. The threshold says which effect wins, and LEMMA 2 describes its shape. This is the basis for the paper's later comparisons of preorder, price-guarantee and no-preorder strategies.
The paper states these results and leaves the proofs to an online appendix. None of them has a machine-checked proof. A complete development would also give reusable facts about normal laws: the expectation for standard normal , the normal newsvendor solution with its closed-form optimal profit, and derivatives of Gaussian integrals with respect to a correlation parameter.
The model is explicit, so the difficulty is not in modelling. It is in turning the two expectations into closed forms and differentiating them. The availability is an integral over of a normal probability whose mean and variance both move with . The expected newsvendor profit involves for a normal . Neither closed form is in Mathlib, and neither is a derivative in of a Gaussian integral. The obvious route, differentiating under the integral sign in (3), needs domination estimates that are uniform in near each point, and these degenerate as .
Signs are the second difficulty. changes sign at , carries a leading minus and divides by , and the derivative of vanishes at and wherever . Strict monotonicity on an interval has to be recovered from a derivative that is positive except at finitely many points.
Everything lives in the namespace PreorderADI.Correlation. A structure Params holds . The predicate Params.Standing records the model's assumptions: , , and , together with . is omitted because nothing in §4 uses it after standardization. is ProbabilityTheory.cdf (gaussianReal 0 1) and is gaussianPDFReal 0 1. The normal law with mean and standard deviation is gaussianReal m (s^2).
The formalization commits to the following conventions and additions:
QuasiconvexOn.A statement about the closed form in place of would make LEMMA 1 a one-line monotonicity fact. So would a definition of that bypasses (3). The definitions rule both out.
Welcome contributions include proofs of the milestones, general Mathlib-style lemmas on Gaussian expectations of and of , and a formalization of PROPOSITION 1 from conditions (i)–(v).
Value-at-Risk (VaR) is the loss level that a portfolio exceeds with probability at most . It is the standard risk measure of banking regulation, and its classical computation assumes Gaussian returns: for a Gaussian return vector with mean and covariance it equals , where is the standard normal distribution function. Real returns are not exactly Gaussian, and a VaR computed from a misspecified distribution can badly understate risk.
El Ghaoui, Oks and Oustry (Oper. Res. 51(4), 2003) replace the single distribution by a class of distributions and define the worst-case VaR as the smallest loss level whose probability is at most under every distribution of the class. Their first class, distributions with a given mean and covariance, leads to the Chebyshev-type bound of their Theorem 1, whose worst case is attained by discrete distributions. §4.2 of the paper asks instead for distributions that stay close to a Gaussian, measured by relative entropy (Kullback–Leibler divergence). Such balls are the basic uncertainty sets of distributionally robust optimization and of robust control in economics (Hansen and Sargent's multiplier and constraint preferences), and they give a smooth worst case. Theorem 9 computes the resulting worst-case VaR in closed form.
Returns are random vectors and a portfolio is a vector with ; its return is . For a level the loss set is (Eq. 13 of the paper).
Given a class of probability distributions on and , the worst-case Value-at-Risk (Eq. 4) is
Fix a mean and a positive definite covariance , and let be the reference Gaussian. For the relative-entropy class (Eq. 43) is
with unless is absolutely continuous with respect to .
The risk factor (Eq. 45) is
and the Gaussian tail of the loss set is .
For , , and , the minimum in (4) over exists and
The milestones follow the proof of Theorem 9 on pp. 553–554, in attack order.
Theorem 9 says that an entropy ball around a Gaussian leaves the form of the Gaussian VaR unchanged: only the risk factor moves, from to , a scalar computed by a one-dimensional maximisation. The worst-case VaR therefore stays a convex function of whenever , and minimising it over a polytope of portfolios is a second-order cone program (problem (3) of the paper). The number is the largest with , which ties the result to the binary-divergence bounds used throughout information theory.
The theorem was proved in 2003. The worst-case-probability step (milestone 5) is an instance of the Donsker–Varadhan / Gibbs variational duality for relative-entropy balls, which the paper imports from the literature (Smith 1995). No machine-checked proof of Theorem 9 or of this duality on is known. A formalization would give a verified closed form for a relative-entropy distributionally robust chance constraint, and the duality and tilting lemmas would serve any mission on KL-ball robust optimization.
The obvious argument is Lagrangian duality for the infinite-dimensional problem . Weak duality and the pointwise maximisation that produces the tilted density are elementary. The difficulty is the step the paper cites rather than proves: that the duality gap is zero, and that the supremum over distributions equals the infimum of the dual over . The feasible set is a set of measures, the objective is an indicator, and the constraint is a divergence that is off a set of absolutely continuous measures, so a finite-dimensional Slater argument does not apply as stated.
The second difficulty is at the boundary of the parameters. At the supremum defining is approached only as , so the final inversion step behaves differently from . At the theorem is false, since every level is feasible and (4) has no minimum.
Returns live in EuclideanSpace ℝ (Fin n). is Mathlib's multivariateGaussian xhat Γ with Γ.PosDef, and is InformationTheory.klDiv, which is unless with integrable log-likelihood ratio and equals otherwise for probability measures. The class requires IsProbabilityMeasure P. is cdf (gaussianReal 0 1), and is defined as , which inverts on . The quadratic form is a double sum, and is written .
Conventions the Lean statements commit to:
IsLeast of the feasible set . "" is written "for every ", with probabilities compared in .sSup of a set that is nonempty and bounded above by for , .sSup and sInf.IsLeast), which the calculus gives.Restricting to , dropping IsProbabilityMeasure, or taking an arbitrary reference measure would trivialize or change the theorem. The class is the full KL ball around the nondegenerate Gaussian.
Infrastructure a complete development needs: the pushforward of a multivariate Gaussian under a linear functional (a one-dimensional Gaussian), the Gibbs variational principle for relative entropy, the strong duality for KL balls, and properties of and its quantile (continuity, strict monotonicity, symmetry ). The Gaussian-quantile and KL-ball duality lemmas are reusable beyond this mission. Contributions of any of these as separate lemmas are welcome.
Many problems in optimization and variational analysis reduce to finding a zero of a maximal monotone operator : minimizers of a proper convex lower semicontinuous function are the zeros of its subdifferential, and saddle points and solutions of variational inequalities are zeros of associated monotone operators. The classical tool is Rockafellar's proximal point algorithm (Rockafellar 1976), which in a Hilbert space converges weakly but, as Güler showed (Güler 1991), not strongly in general.
Solodov and Svaiter (Math. Program. 87, 2000) modified the method in a Hilbert space : after each proximal step they project the starting point onto the intersection of two half-spaces, and they proved that the resulting sequence converges strongly to the metric projection of onto . Kamimura and Takahashi (SIAM J. Optim. 13, 2003) extended this result to Banach spaces such as , , replacing the identity by the duality mapping and the metric projection by a generalized projection defined through the duality mapping. This mission formalizes that extension.
Let be a real Banach space with dual , and write for the value of at .
In Lean, is J : E → StrongDual ℝ E with ∀ x, J x ∈ dualityMap x, is phi J, "" is IsGenProj J C x z, and a run of (3.1) is IsHybridRun T J r x y v with starting point x 0.
If is uniformly convex and uniformly smooth, is maximal monotone, , and , then every sequence generated by (3.1) satisfies
In the order of the paper: the single-valuedness of on smooth spaces and its uniform continuity on bounded sets for uniformly smooth spaces (§2, properties 2 and 4); Xu's characterization of uniform convexity (Proposition 1); with one bounded sequence implies (Proposition 2); existence and uniqueness of (Proposition 3); its variational characterization (Proposition 4); the inequality (Proposition 5); Rockafellar's surjectivity theorem (Theorem 6); well-definedness of (3.1) (Proposition 7); (Remark 1); and the monotonicity step
The theorem gives a strongly convergent method for finding zeros of maximal monotone operators in a class of Banach spaces that includes and for , and it identifies the limit: it is not an arbitrary zero but the generalized projection of the starting point. Applied to it yields a strongly convergent minimization method for proper convex lower semicontinuous functions (§4 of the paper). The generalized projection , the function and the hybrid (CQ-type) projection scheme became standard tools in the later Banach-space fixed-point and splitting literature.
The result is proved in the paper; the mission's contribution is a machine-checked proof. As far as the platform catalog and Mathlib show, none of its ingredients is formalized: Mathlib has uniformly convex and strictly convex spaces and the double dual, but no duality mapping, no notion of smoothness, no monotone operators and no generalized projection.
The obvious route, copying the Hilbert-space proof of Solodov and Svaiter, fails at every place where that proof uses the inner product: the projection onto is no longer characterized by orthogonality, is not a Bregman-type distance, and weak convergence of together with no longer yields strong convergence for free. The paper replaces these steps with properties of and of , which in turn rest on the geometry of : uniform convexity (through Proposition 1) and uniform smoothness (through the uniform continuity of ). In Lean, these geometric facts, reflexivity of uniformly convex spaces (Milman–Pettis) and Rockafellar's surjectivity theorem are all absent and have to be built.
NormedAddCommGroup, NormedSpace ℝ, CompleteSpace). The dual is StrongDual ℝ E with the operator norm; is f x. Sequences are indexed by from .UniformConvexSpace (ε–δ form, equivalent to the sequential definition); strict convexity is StrictConvexSpace ℝ E; reflexivity is surjectivity of NormedSpace.inclusionInDoubleDual. Smoothness and uniform smoothness are defined from the limit (2.1) over real ; uniform smoothness uses one for all unit .∀ x, J x ∈ dualityMap x in every statement that uses it; on a smooth space this determines (a milestone).Reusable infrastructure: the duality mapping and its properties, smooth and uniformly smooth spaces, Milman–Pettis, monotone operators and Rockafellar's surjectivity theorem, and the generalized projection. Contributions to any of these are welcome independently of the goal.
A semidefinite program (SDP) minimizes a linear objective subject to a linear matrix inequality . When the data are uncertain, El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) proposed to optimize against the worst case over a norm-bounded family of perturbations: the robust SDP. Their Theorem 3.1 shows that, for unstructured ("full") perturbations, the robust SDP is itself an SDP in the enlarged variable . Section 4 of the paper then asks what robustification does to the solution. Nominal SDPs are often ill-posed: the optimal set can be a whole face, and optimal points can jump under small data changes. Section 4 shows that, under explicit hypotheses, the robust problem has a unique solution with quadratic growth, which is the sense in which the paper describes robustness as a regularization of SDPs. This mission formalizes that result, Theorem 4.2.
Fix natural numbers , matrices (symmetric), , , and an objective vector , . Write and .
With full perturbations, uncertainty level and (the standing choices of §4), the robust SDP is the SDP
in the variables . A point is feasible if (symmetric positive semidefinite) and optimal if it is feasible and minimizes over all feasible . The solution is the pair .
The paper's hypotheses (§4.1):
For put , the Schur complement of the block in .
The quadratic growth condition (QGC) holds at an optimal point if there are with
Under , symmetry of the , H1, H2, H3(a) and H3(b):
Both halves are stated; uniqueness is of the pair , and existence is part of the claim.
The result. Theorem 4.2 turns the robust SDP into a well-posed problem: a unique solution with quadratic growth. Quadratic growth is the property from which the paper's Hölder-stability results (Theorem 4.3, Corollaries 4.1–4.2) follow through the perturbation theory of Bonnans, Cominetti and Shapiro, and it is what justifies using the robust SDP as a regularization of ill-conditioned SDPs (§5.4). The remark after the theorem notes a geometric reading: the growth holds for every objective, so the boundary of the robust feasible set contains no facets.
Formalizing it. The theorem has a published proof (Appendix A), which relies on a second-order sufficient condition for nonlinear SDPs cited from Bonnans, Cominetti and Shapiro. There is no machine-checked proof of it or of any second-order optimality result for SDPs that we know of. A formalization provides a complete account of the dual attainment, complementarity and second-order steps for this concrete problem class, and it checks the paper's computations; one of them, the intermediate display for the second derivative in Appendix A, has a factor error in its cross term that does not affect the conclusion.
The feasible set of (15) is a spectrahedron, and linear objectives over spectrahedra do not in general have unique minimizers, since optimal faces can be flat. Uniqueness therefore cannot come from convexity alone. It has to come from curvature of the boundary at the optimum, and that curvature is carried only by the nonlinear term of the Schur complement, which is degenerate along some directions. Positive definiteness of the Hessian must be recovered from the structural hypotheses H3(a) and H3(b), which interact with a dual matrix that is known only to exist. The natural first attempt is to use and the positive semidefiniteness of directly. That attempt fails: the second derivative is for a direction-dependent matrix , which vanishes on the kernel of , so it is not positive without H3(a) relating the kernels of all members of the pencil. Dual attainment and complementarity for (15) also have to be established, and the local second-order bound then has to be converted into a statement about every nearby feasible point.
RobustSDP.Uniqueness.SDPData m n p q; decision points are pairs y : (Fin m → ℝ) × ℝ; the coefficient Fs i, i : Fin m, is the paper's . and are Mathlib's Matrix.PosSemidef and Matrix.PosDef, which include symmetry, as the paper's notation does.τ⁻¹, which is at , so every statement about assumes or .ConvexOptimization.sdp_strong_duality on the platform, in another Mathlib environment), existence of minimizers on closed bounded sets, second derivatives of matrix-valued maps, and a local second-order argument for convex problems. The duality and second-order parts can be reused beyond this mission. Contributions to any milestone, or alternative proofs that avoid the general Bonnans–Cominetti–Shapiro theory, are welcome.Large combinatorial structures are often best understood through their limits. For dense graphs, Lovász and Szegedy (2006) showed that every sequence of graphs whose subgraph densities converge has a limit object, a graphon, and that every graphon arises this way. Borgs, Chayes, Lovász, Sós and Vesztergombi (2008) related this convergence to the cut distance. These results turned questions of extremal combinatorics and property testing into analysis on a compact space.
Hoppen, Kohayakawa, Moreira, Ráth and Sampaio (arXiv:1103.5844; J. Combin. Theory Ser. B, 2013) carried this programme over to permutations. Their limit objects, called limit permutations here and now usually called permutons (as a probability measure on the square), underlie later work on quasirandom permutations, pattern densities, and property testing of permutations (Hoppen et al., 2011). This mission formalizes the paper's main result, Theorem 1.6: convergent permutation sequences have limits, and every limit is attained.
Timeline:
For , is the set of permutations of , and for . For and , the number of occurrences counts the increasing -tuples in with . The subpermutation density is for and for . A permutation sequence is convergent if converges for every fixed .
A function is a cdf if it is non-decreasing and right-continuous with and . A limit permutation is a Lebesgue measurable such that is a cdf for every , and for every . The set of limit permutations is .
With one associates a random point : , and given , has cdf . Draw independent copies . The -random permutation records the relative order of the read in increasing order of the . The density of in is . A sequence with converges to , written , if for every .
For , the step limit permutation spreads the permutation matrix of uniformly over its grid cells. The rectangular distance is the largest difference, over axis-parallel rectangles, between the probabilities the two associated random points assign to the rectangle.
The two parts together identify with the set of limits of permutation sequences.
In the order the proof uses them:
Theorem 1.6 makes , modulo null sets, the completion of the set of finite permutations under density convergence. Asymptotic statements about pattern densities, such as quasirandomness criteria, extremal pattern-density problems and the testability of permutation properties, can then be stated and proved on a compact space of measures rather than along sequences. Lemma 4.2 is the quantitative sampling statement behind testability, and Theorem 1.7 says that a limit, viewed as a measure on the square, is unique.
The results are proved in the paper and have been used for over a decade. To the best of current knowledge they are not formalized in any proof assistant. The mission produces a machine-checked account of the permuton correspondence: the definitions of subpermutation density, limit permutation and -random permutation, and the equivalences between the three natural convergences on . Alternative proofs are welcome, for instance of (ii) through Lemma 4.2 and the Borel–Cantelli lemma rather than the paper's strong law for U-statistics.
The obvious route to (i) is compactness: the laws of the random points attached to have a weakly convergent subsequence. The weak limit is only a measure, however. Turning it into a function that is a cdf in for every , with exact uniform integrals for every , requires a regular conditional distribution (Lemma 2.2). One then has to show that weak convergence carries the pattern densities along. That fails for general measures on the square, because the events defining have boundaries on which ties occur. Uniform marginals are what rule the ties out. The limit must also be independent of the subsequence, which needs the uniqueness statement Lemma 5.1. For (ii), the natural random sequence converges only almost surely, so an almost-sure limit theorem or a quantitative concentration bound is unavoidable.
unitInterval with Lebesgue measure. A limit permutation is a curried real function Z : I → I → ℝ. Measurability is almost-everywhere measurability for the product measure, which is Lebesgue measurability. The cdf and integral conditions hold for every and every .Equiv.Perm (Fin n) (0-based), and a permutation sequence is ℕ → Σ n, Equiv.Perm (Fin n). Patterns of every length, including the trivial length , are quantified over; the length- clause always holds.Needed infrastructure includes Prokhorov compactness of probability measures on a compact space, the Portmanteau theorem, conditional cdfs (ProbabilityTheory.condCDF), Hoeffding's inequality and Borel–Cantelli, all largely in Mathlib. The permutation-density and permuton layer is reusable for quasirandomness and testing results. Mission II of this series, on the rectangular-distance characterization, uses the same model.
Many firms learn part of future demand before it has to be served: customers place orders days or weeks ahead of the date they need the goods, or commit to delivery dates in contracts. Advance demand information of this kind reduces the uncertainty the inventory manager has to protect against, and the question is how replenishment decisions should use it. Gallego and Özer (Management Science 47(10), 2001) model orders placed up to periods ahead and a supply lead time . They show that, with a fixed ordering cost, the classical structure survives with parameters that depend on the observed future demand, and they identify when that dependence disappears.
The classical theory this builds on is the finite-horizon inventory model with a set-up cost. Scarf (1960) introduced -convexity to prove that policies are optimal there. Veinott (1966) and Iglehart (1963) bounded the optimal policy parameters by myopic quantities. Gallego and Özer extend both results to a state that carries a vector of observed demands.
Periods are . In period customers place orders for periods ; is a random vector with law and nonnegative components. The lead time and the information horizon satisfy ; write . The state at the start of period is a pair : the modified inventory position , and the vector
of demands already observed for the periods beyond the protection period .
The manager raises to an order-up-to level , paying a set-up cost if . After is observed, the state moves to
with . With a convex single-period cost , discount factors and , the optimal cost satisfies and
Let . The order-up-to level is the least minimizer of , and the reorder point is .
A function is -convex, , if for all and ; is Scarf's -convexity. In the stationary problem , , and , and the myopic levels are
For the stationary problem, every and every observed-demand vector ,
Only the observed demand for the first period beyond the protection period is compared with the threshold; the other components of are free.
Theorem 1 says that advance demand information does not destroy the structure: the optimal policy is still a reorder point and an order-up-to level, now functions of . Theorem 2 is a horizon result. Once enough demand is already booked for period , the order-up-to level is the myopic one, computed from alone, and the rest of the information vector can be ignored. The threshold grows with the set-up cost. In practice the manager then orders only to cover demand up to period , knowing another order will be placed in period , and the search for state-dependent policies is confined to states with little booked demand.
The results are proved in the paper, with some steps argued informally (the unit forward difference in Lemma 3, a minimum over an open set in the definition of ). As far as the platform's catalog shows, no optimality theorem of this form has a machine-checked proof: the platform has -convexity lemmas for a single constant, not for -convexity or a dynamic program with a vector state. A formal proof would check the infinite-state induction and the conditions under which the expectation in (9) is finite. The -convexity layer and the one-period results (Lemma 2, Corollary 1) are reusable for any set-up cost model.
The obvious induction proves -convexity of and then applies Scarf's argument. The vector state makes each step conditional on facts the scalar case gets for free. The expectation in (9) mixes a random shift of with a random update of , so preserving -convexity needs Lemma 1, Part 4 rather than the scalar version. Coercivity and continuity of , and measurability and integrability of , must be carried through the induction jointly in . They cannot be assumed.
For Theorem 2, is not a function of alone, and a comparison of with has to control . That requires the lower bound at the next period, which holds only on the nonnegative state space.
Everything is stated about the functional equation (8)–(9). The paper derives it in Appendix A from a control problem over history-dependent policies, citing Özer (2000); that reduction is out of scope. The demand vector is Fin (L + M + 2) → ℝ and is Fin M → ℝ, with component equal to . is defined by backward recursion, minima over are infima over , and expectations are Bochner integrals. is an abstract primitive, not built from holding and penalty costs.
The paper's hypotheses are convex with as (stated for , used for ), (Section 4), and . The formalization adds hypotheses the paper uses without stating:
All hypotheses are placed on the primitives; nothing is assumed about the derived or . A Solutions/verification instance (, , , zero demand) shows these hypotheses can be met together.
The definition of is read as an infimum: the paper prints a minimum over an open set. and appear through IsLeast and IsGreatest, never as sInf/sSup values. A default value therefore cannot satisfy a conclusion, and vacuous readings (an empty minimizer set, an unbounded reorder set) are excluded. The infinite-horizon results (Lemma 4, Theorem 3, Corollary 2) and the zero set-up cost case are not part of this mission. Contributions are welcome at every level, and most of all a reusable library for -convex functions.
A forecaster who announces "70% chance of rain" is calibrated if, among the days on which that number was announced, it rained on about 70% of them. Dawid (The well-calibrated Bayesian, JASA 1982) proposed calibration as the minimal requirement of an honest probability forecaster. Oakes (Self-calibrating priors do not exist, JASA 1985) showed that no deterministic forecasting rule can be calibrated against every sequence of outcomes: an adversary who knows the rule can always choose the outcome that contradicts the forecast.
Foster and Vohra (Calibrated learning and correlated equilibrium, Games Econ. Behav. 21 (1997) 40–55) use calibration as the bridge between learning and equilibrium in repeated games. Their Theorem 1 says that if each player best-responds to calibrated forecasts of the opponent, the empirical distribution of play converges to the set of correlated equilibria. That theorem is only useful if calibrated forecasts can actually be produced whatever the opponent does. Theorem 3 of the paper, credited to an unpublished 1991 manuscript of the same authors and proved in the paper's Appendix, says they can, provided the forecaster randomizes.
Timeline. Dawid (1982) defines calibration. Oakes (1985) rules out deterministic calibrated forecasting against arbitrary sequences. Foster and Vohra (1991 manuscript; 1997 paper, Theorem 3 and Appendix) give a randomized forecaster calibrated against any opponent, through a pairwise ("internal") no-regret property. The full argument appeared in Foster and Vohra, Asymptotic calibration, Biometrika 85 (1998). Hart and Mas-Colell (A simple adaptive procedure leading to correlated equilibrium, Econometrica 2000) later made internal regret the standard route to correlated equilibrium.
Player 2 has pure strategies . In every round, player 1 announces a forecast , a probability vector (, ), and player 2 plays a strategy . The two moves are simultaneous: player 2 does not see the current forecast.
A history of length is the list of the pairs (forecast, play), oldest first. For a forecast vector and a strategy :
A randomized forecaster maps each history to a probability distribution on forecasts. A learning rule of player 2 maps each history to a probability distribution on strategies. In round the forecast is drawn from and the play from , independently given the history of the first rounds. This defines the law of the first rounds (histLaw F A t).
For the Appendix: with forecasts, losses and mixing weights , the pairwise regret of replacing forecast by forecast is
There is a forecaster , with probability-vector forecasts, such that for every learning rule of player 2 and every ,
The forecaster is fixed before the opponent; no rate is claimed, and the rate may depend on .
with the fractional L-2 calibration score. 4. L-1 versus L-2 (p. 54). For each , .
The result. Theorem 3 makes the hypothesis of Theorem 1 attainable: combined, they show that there are learning procedures under which play converges in probability to the set of correlated equilibria of any finite game (the paper's Corollary, p. 49). The intermediate Lemma 1 is an early internal-regret bound; internal (swap) regret minimization later became the standard algorithmic route to correlated equilibria and to calibrated prediction in online learning.
Formalizing it. The result is proved, in the 1997 Appendix in telegraphic form and in full in Foster and Vohra (1998). The Appendix leaves several steps informal (see Formalization scope), so a machine-checked proof must supply them. No formalization of calibration or of internal regret was found on Prove2Me as of 2026-09-26. The mission produces a formal model of randomized forecasters against adaptive opponents, a checked internal-regret bound with an explicit constant, and the passage from regret to calibration.
The obvious approach is to pick, at each round, a forecast that corrects the current miscalibration. This is a deterministic rule, and by Oakes' theorem an opponent can defeat it. Randomization alone does not help either: the forecaster must randomize in a way that controls every pairwise regret at once, not only the regret against the best fixed forecast. External no-regret does not imply calibration.
Two further gaps separate Lemma 1 from Theorem 3. First, the Appendix controls a fractional score in which the event "forecast was issued" is replaced by its probability . The realized calibration score involves the random choices, so a concentration argument is needed against an adaptive opponent. Second, a fixed grid gives calibration only up to its mesh . Exact convergence requires letting the grid size grow and shrink over time, and the scores of the different phases must be combined.
Fin n; forecasts are vectors Fin n → ℝ that are probability vectors (IsDist). Histories are Lean lists of (forecast, play) pairs, oldest first. Forecaster and opponent are maps from histories to Mathlib PMFs. The history law is built with PMF.bind/PMF.map, with the two draws independent given the past. is the toOuterMeasure of the law, in ℝ≥0∞; no σ-algebra on histories is used.∃ F, ∀ A). The reverse order is trivial, since one can forecast 's next play.MarkovChain.exists_isStationary for row-stochastic matrices. Also useful: martingale concentration for PMF-built processes, and Cauchy–Schwarz with weights. The history-law construction is reusable for any repeated forecasting game.A correlated equilibrium (Aumann 1974) is a joint distribution over the players' strategy profiles such that no player gains by deviating from the strategy the distribution recommends to them. It is the equilibrium notion that learning dynamics in repeated games most naturally reach, and a basic question in learning in games is which simple rules, played repeatedly, drive the empirical distribution of play to the set of correlated equilibria.
Foster and Vohra (1997) answer this with a hypothesis on forecasts instead of a particular algorithm. Each player forecasts the other's next move and best-responds to the forecast. They only require the forecasts to be calibrated in the sense of Dawid (1982): among the rounds in which a player forecast a given probability vector, the empirical frequencies of the opponent's moves must approach that vector. Their Theorem 1 says that this already forces the empirical joint distribution of play to approach the set of correlated equilibria. The paper uses this to argue that Bayesian players under a common prior, whose forecasts are calibrated by Dawid's theorem, end up playing a correlated equilibrium. That is an alternative to Aumann's (1987) derivation of correlated equilibrium from common priors and rationality.
Timeline:
A finite two-player game has strategy sets and and payoff matrices , which the players maximize. A joint distribution is a nonnegative matrix with entries summing to . It is a correlated equilibrium if
and symmetrically for player 2. The set of correlated equilibria is .
The game is played in rounds . In round player 1 issues a forecast , a probability vector over , and player 2 issues a forecast over . Each player then plays a best response to its forecast, and . Here and are best-reply functions: maximizes for every probability vector , and is a fixed function of the forecast alone. This is the paper's standing assumption of a stationary, deterministic tie-breaking rule.
For a forecast sequence and the opponent's plays , counts the rounds among the first in which forecast . is the fraction of those rounds in which the opponent played , and if there are none. The forecast is calibrated with respect to if for every
The empirical joint distribution is the fraction of the first rounds in which player 1 played and player 2 played .
If is calibrated with respect to and is calibrated with respect to , then
The goal fixes no rate and no particular forecasting method: it asserts only convergence of to the set , for every calibrated forecast.
With the constant forecast and the non-stationary tie-break "heads on even rounds, tails on odd rounds", both forecasts are calibrated and every play is a best reply, yet does not approach . The stationarity assumption cannot be dropped.
The result. Theorem 1 separates what learning needs from how it is achieved. Any forecasting procedure that is calibrated, combined with myopic best responses, yields correlated equilibrium behaviour in the long run. The paper's Theorem 3 constructs a randomized calibrated forecaster, so the theorem gives an uncoupled learning procedure for correlated equilibrium, one that needs no knowledge of the opponent's payoffs. The converse direction, that every correlated equilibrium arises this way for almost every game, is the paper's Theorem 2 (a separate mission of this series).
Formalizing it. The theorem is proved in the paper and has no machine-checked proof on Prove2Me or, to the knowledge of this mission, elsewhere. The platform's existing correlated-equilibrium results (the Algorithmic Game Theory swap-regret development, AGT.swap_regret_correlated_equilibrium) reach correlated equilibrium through swap regret of mixed strategies, a different hypothesis and a different object. This mission adds a formal notion of calibration and the convergence argument, both reusable for the paper's Theorems 2 and 3 and for later work on calibration and learning.
The obvious reading of calibration is that each player's forecast converges to the opponent's empirical distribution; if that held, best responses to it would give convergence. It does not hold. Calibration constrains the opponent's frequencies only conditionally on the forecast issued, and the forecasts need not converge at all. What must be shown is a statement about the conditional distributions of the joint play given each strategy of player 1, while the set of forecasts issued keeps growing. Rows of the limit with zero mass carry no conditional distribution. The "min → 0" form also asks for more than a property of limit points: it is a uniform statement about all large .
Fin m and Fin n; payoffs are real matrices; forecasts are real vectors required to be probability vectors in every round.AGT.IsCorrelatedEquilibrium, restated rather than imported.Proofs of any milestone, and reusable lemmas about calibration scores and compactness of the simplex of joint distributions, are welcome.
Paging is the problem of managing a two-level memory: a fast cache holds pages out of an address space of pages, requests to pages arrive one at a time, and a request to a page outside the cache (a page fault) forces the algorithm to bring that page in and, when the cache is full, to evict another. The cost is the number of faults. An on-line algorithm decides which page to evict without knowing future requests. The comparison of paging policies with the optimal off-line policy is where competitive analysis began.
Sleator and Tarjan showed that LRU and FIFO are within a factor of the off-line optimum and that no deterministic on-line algorithm does better than (Sleator–Tarjan 1985). Randomization changes the picture: Fiat, Karp, Luby, McGeoch, Sleator and Young introduced the marking algorithm and proved that its expected cost is within a factor of the optimum, where (arXiv:cs/0205038).
Timeline.
The paper works in the uniform -server problem, which is isomorphic to paging. There is a set of vertices, enumerated , and moving a server between two distinct vertices costs . There are servers, . A request is a vertex, and after each request some server must be on it. Cached pages are covered vertices; a fault is a server move.
The marking algorithm starts with its servers on and keeps a set of marked vertices, initially the covered ones. On a request to :
The marks are updated before the server is chosen. For a finite request sequence , is the algorithm's expected number of server moves. is the least number of moves with which servers, starting from the same configuration and knowing in advance, can serve .
A randomized algorithm is -competitive if there is a constant such that for every request sequence and every algorithm .
The marks divide into phases. A new phase begins at the request that would make vertices marked. A vertex is clean in a phase if it was not requested in the previous phase and not yet in this one, and stale if it was requested in the previous phase but not yet in this one.
The constant may depend on , and the enumeration, never on .
The result. Theorem 1 was the first proof that randomization beats the deterministic barrier for paging, bringing the ratio down to . Together with the paper's lower bound for every randomized algorithm, it determines the randomized competitive ratio of paging up to a factor . Its phase and clean/stale accounting is reused throughout the analysis of randomized caching.
Formalizing it. The theorem is proved (1991). As far as is known it has no machine-checked proof. Formalizing it requires a probabilistic model of a randomized on-line algorithm, an off-line optimum, and a phase decomposition with an exchangeability argument, and these are the first such objects in this library. Theorem 2 and the , example use the same definitions and also check that the formal algorithm is the paper's. The sharp ratio is a natural follow-up.
The comparison is between a random process and a deterministic adversary, and each side has its own obstacle.
On the algorithm's side, the configuration inside a phase is random, and the fault probability of a stale request depends on the whole history of the phase. The claim that the uncovered stale vertices form a uniformly random subset of the stale ones is an exchangeability property of the process, and must be established from the step-by-step uniform choice. The worst-case ordering of the requests within a phase then has to be justified as a bound, not assumed.
On the adversary's side, the per-phase bound does not sum directly. The and terms telescope across phases only because the configuration of the marking algorithm at each phase boundary is deterministic. The first phase, which begins after an initial run of requests to , and the last, incomplete phase have to be absorbed into the additive constant.
The vertex set is an abstract metric space with and for . The natural metric on is deliberately not used. The configurations and the off-line optimum are the published KServer definitions (KServer.Config, KServer.offlineCost), with taken from the marking algorithm's initial configuration. An off-line algorithm starting elsewhere changes the cost by at most , which is absorbed into .
The marking algorithm is a Markov chain on pairs (covered set, marked set). Each step is a PMF, with the eviction drawn by PMF.uniformOfFinset from the covered unmarked vertices. The expected cost is the sum over requests of the probability that the request is not covered, which is exact because the algorithm moves exactly one server per fault. Harmonic numbers are Mathlib's harmonic, cast to . Phases, clean counts and lazy off-line schedules are defined once, in the mission's definition file, and all milestones use them.
A trivializing formalization is ruled out as follows. The additive constant is quantified before , so a per-sequence constant cannot be used. The comparison is with the optimum over all off-line schedules, not a particular one. The random choice is among the covered unmarked vertices, with marks updated first. The hypothesis excludes the degenerate case , where .
Proofs of individual milestones are welcome. The laziness reduction for off-line schedules, the exchangeability lemma for the uniform eviction process, and the harmonic-sum identity are reusable beyond this mission.
A buyer and a seller negotiate over a single indivisible good. Each knows how much the good is worth to them, but not how much it is worth to the other side. Whether the two will trade, and at what price, then depends on how each party shades its offer to exploit the other's uncertainty. Chatterjee and Samuelson (Bargaining under Incomplete Information, Operations Research 31(5), 1983) modelled this situation as a one-shot game in which both parties submit sealed offers simultaneously, and characterised its Bayesian equilibria.
The model became the standard reference point for bilateral trade with two-sided private information. Myerson and Satterthwaite (J. Econ. Theory 29, 1983) showed that no mechanism can guarantee efficient trade in this setting, and that the equilibrium of the Chatterjee–Samuelson game with and uniform values attains the second-best efficiency bound. Later work on the -double auction (Satterthwaite and Williams, J. Econ. Theory 48, 1989; Leininger, Linhart and Radner, J. Econ. Theory 48, 1989) studies the continuum of equilibria of exactly this game. The object of the present mission, a pair of linked differential equations, is the tool these papers use to construct and classify equilibria.
A seller has reservation price and a buyer has reservation price . Each knows their own value. The buyer's belief about is a probability measure with distribution function ; the seller's belief about is with distribution function . The subscript names the player who holds the belief, not the variable. Each belief is regular: , , and is strictly increasing and differentiable on the value interval, with density (respectively ).
Under the Bargaining Rule, the seller asks and the buyer offers simultaneously. If the good is sold at for a fixed ; otherwise nothing happens. Profits are for the seller and for the buyer on trade, and zero otherwise.
An offer strategy is a function (for the seller) or (for the buyer) from values to offers. Against , a buyer with value offering earns in expectation
and symmetrically . The pair is an equilibrium if maximises over all real offers for every buyer value , and maximises for every seller value .
A strategy is of class if its offers are bounded, it is nondecreasing, it is strictly increasing except where it sits at its lowest offer or its highest offer , and it is differentiable wherever its offer lies strictly between and . A class equilibrium is an equilibrium in which both strategies are of class .
In a class equilibrium, wherever the seller's strategy is strictly increasing around and the buyer value offers ,
and wherever the buyer's strategy is strictly increasing around and the seller value asks ,
The paper writes in (3a) and in (3b).
The milestones assume (respectively ), which the paper's formula for the offer density needs. The goal does not assume it.
Theorem 2 reduces the search for equilibria to the analysis of a pair of ordinary differential equations. Every explicit equilibrium in the paper and in the later -double-auction literature is found as a solution of (3a)–(3b) with suitable boundary conditions: the linear equilibrium for uniform beliefs (the paper's Example 1), the one-parameter families of Satterthwaite–Williams, and the non-linear equilibria of Leininger–Linhart–Radner. The equations also expose how the split parameter distributes bargaining power: at equation (3b) forces the seller to ask their own value, and at equation (3a) forces the buyer to bid theirs.
The result is proved in the paper. To the best of a search of the platform, no formalization of it or of the bargaining model exists. This mission produces a machine-checked version of the necessary conditions. Its definitions of beliefs, expected profits, equilibrium and class are also the basis for companion missions on the uniform linear equilibrium and its trade probability.
The paper's proof is four lines: differentiate the expected profit, set the derivative to zero, substitute. Three steps of that argument do not survive a careful reading.
First, the paper differentiates under an offer density that exists only if is strictly increasing and has a positive derivative. Class allows to be flat at its bounds, to jump between them, and to have zero derivative. The formal goal assumes none of this. It must handle the case , where the offer distribution has an infinite density at and the first-order condition becomes a one-sided argument.
Second, identifying with requires that no seller value outside a neighbourhood of makes the same offer. That is a global statement about , and it is where monotonicity on the whole interval and the "flat only at the bounds" clause of class enter.
Third, the first-order condition needs the equilibrium offer to be an interior maximiser of a function of that is differentiable there. The profit is an integral over the belief, and its differentiability at must be derived from the differentiability of at the single point and of . Neither nor is assumed continuous elsewhere.
Values, offers and are real numbers. Beliefs are probability measures on , with distribution function Mathlib's ProbabilityTheory.cdf. Expected profits are Bochner integrals over the opponent's value, not over an offer density. The two agree whenever the density exists, and the integral form needs none. Integrability is not assumed: for a class strategy and a regular belief supported on the value interval, the integrand is bounded and almost everywhere measurable. Ties () trade. Deviations range over all real offers. Strategies are arbitrary functions whose values outside the value interval play no role.
The derivative is deriv S y. The paper's inverses and are not introduced as functions. The matching value is a universally quantified variable with , so no junk value of an inverse can make an equation true or false. The equations are asserted only at values interior to an open subinterval on which is strictly increasing. A formalization that assumed the first-order condition, or restricted to strategies with everywhere, would be a different and weaker theorem.
A complete development needs: differentiation of parametric integrals of indicator type (the derivative of ), the change of variables from values to offers under a strictly increasing strategy, and Fermat's rule (IsLocalMax.hasDerivAt_eq_zero). The first two are reusable for auctions and other Bayesian games with monotone strategies. Proofs of the milestones, alternative proofs of the goal, and general lemmas about monotone strategies are welcome.
A variational inequality asks for a point of a set at which a vector field makes a non-obtuse angle with every feasible direction: for all . It is the common form of the first-order optimality condition of a constrained optimization problem, of complementarity problems in mathematical programming, and of equilibrium conditions in traffic networks and economics. Two generalizations are standard in operations research. In a quasi-variational inequality the constraint set depends on the unknown, , as in generalized Nash games where each player's feasible set depends on the other players' choices. In a generalized variational inequality the vector field is set-valued, , as when is the subdifferential of a nonsmooth convex function.
D. Chan and J. S. Pang (Math. Oper. Res. 7 (1982) 211–222) introduced the problem that combines both, the generalized quasi-variational inequality (GQVI), and proved existence theorems for it. Their §5 gives a second route to existence, independent of the set-valued fixed point theory of their §3: a solution is a fixed point of a map built from Euclidean projections, and for single-valued continuous the Brouwer fixed point theorem produces one. The characterization of solutions as projection fixed points, for the generalized variational inequality, is due to Fang and Peterson (reference [11] of the paper, a 1979 University of Maryland Baltimore County research report). This mission formalizes that projection route.
Work in with the Euclidean inner product and norm . A point-to-set mapping assigns to each a subset ; a point-to-point mapping assigns a vector .
The GQVI. Given point-to-set mappings and , asks for vectors and with
Such a pair is a solution. For a point-to-point one takes : find with for all .
Projection. For a set and a point , the projection is the nearest point of to . For nonempty closed convex it exists and is unique.
Semicontinuity of point-to-set mappings (Berge). is upper semicontinuous at if for every open there is a neighbourhood of with for ; lower semicontinuous at if for every open meeting there is a neighbourhood of with for ; continuous if both. "On a set " means at every point of , with neighbourhoods relative to .
Let be continuous on a nonempty compact convex set , and let be a continuous mapping on whose values , , are nonempty, closed, convex and contained in . Then there is with
If is continuous at and every is nonempty, closed and convex, then for every the map
is continuous at .
If every is closed and convex, then for every pair
The Brouwer fixed point theorem is already on the platform (AGT.brouwer_fixed_point) and is included as a reference item, as is the Hilbert-space nearest-point theorem VectorSpaceOpt.min_distance_convex_set.
Theorem 5.2 is the existence theorem for quasi-variational inequalities with a moving convex constraint set and a continuous single-valued field, under compactness. With constant it is the Hartman–Stampacchia theorem (Acta Math. 115 (1966) 271–310), the basic existence result for finite-dimensional variational inequalities, and so it also covers existence of equilibria of generalized Nash games whose shared constraints satisfy the continuity hypotheses. The paper notes that Theorem 5.2 also follows from its Corollary 3.1, which rests on the Eilenberg–Montgomery fixed point theorem; the projection route needs only Brouwer.
Theorem 5.1 matters beyond this existence result: it turns the GQVI into a fixed-point equation, which is the basis of projection algorithms for variational inequalities and of the contraction argument of the paper's Theorem 5.3. Lemma 5.1, continuity of the projection onto a continuously moving closed convex set, is a stability result used throughout parametric optimization.
All three statements were proved in 1982. None has a machine-checked proof on the platform or in Mathlib, which has neither a projection onto a general closed convex set as a function of the set nor any variational inequality. The work of this mission is to formalize the known proofs.
Theorem 5.1 is a direct consequence of the variational characterization of the nearest point of a convex set. The substance lies in Lemma 5.1 and in adapting it to the goal. The projection depends on the set , not only on the point, and continuity of is a statement about sets, given by two separate semicontinuity conditions that each control only one side of the convergence. Neither alone suffices: upper semicontinuity without lower lets shrink abruptly and the nearest point jump; lower without upper lets limits of nearest points fall outside . The limit points of the projections must also be kept bounded, which needs the nonemptiness near .
A second difficulty is that the goal assumes continuity of only on , with neighbourhoods relative to , while Lemma 5.1 is stated for continuity at a point of . Applying the lemma to the composite map on therefore requires either a relative version of the lemma or a reduction; the lemma cannot be quoted verbatim.
The space is EuclideanSpace ℝ (Fin n) with its Euclidean norm, never the sup-norm space Fin n → ℝ. Point-to-set mappings are functions into Set. The solution predicate is IsGQVISolution K f x y; a point-to-point enters as fun z => {f z}. Upper and lower semicontinuity are Mathlib's UpperHemicontinuousAt/On and LowerHemicontinuousAt/On; "continuous on " is both, relative to .
The projection is IsProj S z p (nearest-point predicate) and proj S z, which returns a nearest point when one exists and the junk value otherwise. Theorem 5.1 uses the relational form, so no junk value enters when . Lemma 5.1 assumes every nonempty, closed and convex, so proj is always the true projection there.
Two hypotheses implicit in the paper are explicit:
A formalization in which the projection is merely "some point of ", or ignores the distance, would make the reverse direction of Theorem 5.1 false and Lemma 5.1 meaningless; a GQVI whose test points range over instead of would turn Theorem 5.2 into a plain variational inequality on . Both are excluded by the definitions above.
A complete development needs the nearest-point characterization on closed convex sets (available in Mathlib and on the platform), sequential characterizations of upper and lower hemicontinuity for closed-valued mappings in , continuity of the projection onto a moving convex set, and Brouwer's theorem (a platform reference). The hemicontinuity lemmas and the projection-continuity lemma are reusable for the other missions of this series and for parametric optimization in general. Proofs of Lemma 5.1 and Theorem 5.1, a relative-to- version of Lemma 5.1, and a proof of Brouwer's theorem are all welcome.
Infinite-horizon optimal control problems with nonnegative costs (Strauch's negative dynamic programming, the positive-cost counterpart of Blackwell's positive model) are among the settings where the standard tools of discounted dynamic programming fail: there is no contraction, costs may be infinite, and the value-iteration algorithm started from zero may converge to the wrong limit. Strauch showed in 1966 that under these assumptions the limit of value iteration can lie strictly below the optimal cost (Strauch 1966). Bertsekas (1977) recast the deterministic, stochastic and minimax versions of these problems as one abstract problem about a monotone mapping , and proved Bellman's equation, optimality criteria for stationary policies, and conditions for convergence of the dynamic programming algorithm at that level of generality (Bertsekas 1977). This framework became the basis of the "abstract dynamic programming" theory developed later in Bertsekas and Shreve (1978) and Bertsekas (2013, 2022).
This mission formalizes the part of the paper that works under the uniform increase assumption, culminating in the paper's compactness condition for convergence of value iteration.
A model consists of a nonempty state space , a control space , for each a nonempty constraint set , a mapping , where is the set of functions ordered pointwise, and a terminal function with . is monotone: implies for .
A selector is with ; a policy is a sequence of selectors, and is stationary. Define
is the optimal value function and the limit of the dynamic programming algorithm. A policy is optimal if .
Assumption I is for all and . Assumption I.1 says that commutes with limits of nondecreasing sequences above . Assumption I.2 says there is with for and , where . For the convergence analysis the paper introduces, for , the sets with real, their projections on through admissible , and the closure obtained by adding limits of real sequences at fixed .
Let I, I.1, I.2 hold, let be a Hausdorff topological space, and suppose there is such that is compact for every , real and . Then
and there exists an optimal stationary policy.
In attack order: Proposition 2 ( for the -stage problem); Proposition 4 (-optimal policies, stationary when ); Proposition 5 (Bellman's equation and minimality of among -excessive functions above ); Corollary 5.1 (the same for ); Proposition 7 ( is optimal iff ); Proposition 10 (, with equality throughout iff ); Lemma 2 (, the epigraph); Proposition 11 (convergence of value iteration is equivalent to interchanging projection and intersection); Lemma 3 (a function with compact real sublevel sets attains its minimum).
The result. Proposition 12 gives a checkable condition, compactness of sublevel sets of the one-stage costs, under which value iteration started at converges to the optimal cost and an optimal stationary policy exists, in any model covered by the abstract framework: deterministic and stochastic control with nonnegative costs, minimax control, and problems with state constraints encoded by infinite costs. Without such a condition the algorithm can stall below even in one-dimensional deterministic problems. Propositions 5 and 7 are the abstract form of the classical Bellman equation and optimality criterion for positive-cost problems.
Formalizing it. The results are proved in the paper. The platform's existing dynamic programming results are finite-state, real-valued and contraction-based; none covers extended-real costs, general state spaces, or the uniform increase regime. This mission would produce a machine-checked abstract DP layer over EReal in which the Bellman equation, the stationary-policy criterion and the convergence conditions are proved once for every model satisfying the assumptions. No machine-checked proof of these results is known.
The obvious argument for interchanges a limit in with an infimum over policies. Under Assumption I the iterates increase, and a limit of infima of an increasing family can be strictly smaller than the infimum of the limits; the paper's own example in Section 1 shows it. Monotone convergence arguments therefore do not apply. The paper converts the interchange into a statement about projections of the sets and closes the gap with a compactness argument, which requires handling infinite values carefully: epigraphs are taken over real only, and states where the value is are treated separately. Proposition 4, on which Bellman's equation rests, needs a selection of nearly optimal policies state by state and a geometric control of the errors through I.2.
Functions in are S → EReal. Policies are sequences ℕ → Selector, where a selector is a function with for all . The composition applies first. and are limUnder atTop of their defining sequences. Every statement assumes Assumption I, under which these sequences are nondecreasing and the limits exist. takes the infimum over only and over admissible policies only. Both and each are nonempty. ranges over , and the closure is the sequential closure in at fixed , not a topological closure on . The sets are used only for . I.2 is parameterized by its scalar . Proposition 4's second part refers to the for which I.2 is assumed.
Repairs of the page. Lemma 3 is false as printed. On with the cofinite topology every subset is compact, yet has no minimum. It also fails for . The mission states Lemma 3 for a Hausdorff space and nonempty , and Proposition 12 for a Hausdorff control space. Proposition 12 is also false as printed: with , cofinite, and , all hypotheses hold but no stationary policy is optimal and (70) fails. Proposition 11(b)'s parenthetical "(equivalently there exists an optimal stationary policy)" holds only together with (the paper cites an example with an optimal stationary policy and ). It is stated in that joint form, never as an equivalence between condition (68) and the bare existence of an optimal stationary policy.
Trivializing readings ruled out. An empty constraint set would make and the policy set empty, so every Bellman identity would hold trivially. The model therefore requires . The goal's three conclusions, (70), the chain of equalities and the optimal stationary policy, are all required, so a formalization that states only one of them is not the goal.
Needed infrastructure: monotone limits in EReal, infima over sets, and compactness in Hausdorff spaces (Mathlib's Cantor intersection theorem). The definitions (model, assumptions, epigraph sets) can be reused for the companion mission under Assumption D and for later abstract DP developments. Proofs of any milestone are welcome, as are reusable lemmas on monotone EReal sequences.
Conic quadratic programs (second-order cone programs) minimize a linear objective subject to linear constraints and constraints of the form . They model robust linear programs with ellipsoidal uncertainty, truss topology design, contact problems with Coulomb friction, and convex quadratically constrained quadratic programs. In theory they are no harder than linear programs of the same size; in practice, linear programming software handles far larger instances than conic quadratic solvers did at the time of writing (Ben-Tal & Nemirovski 2001, pp. 193–195). This raises a question about geometry rather than algorithms: can a second-order cone be replaced by a polyhedral cone of moderate size without losing much accuracy?
The obvious answer — circumscribe the cone by a polyhedral cone with many facets — fails: the number of facets must grow exponentially in the dimension, even for constant accuracy. Ben-Tal and Nemirovski showed that auxiliary variables change the picture completely: a projection of a polyhedral cone can approximate the Lorentz cone with size only . The construction is now standard; it underlies, for instance, the lifted linear-programming branch-and-bound algorithm for mixed-integer conic quadratic programs of Vielma, Ahmed & Nemhauser 2008.
For let . The -dimensional Lorentz cone is
Fix . A polyhedral -approximation of is a linear map
such that
Equivalently, the polyhedral cone projects onto a cone lying between and its -extension. The size of the approximation is : the number of auxiliary variables plus the number of linear inequalities (an equation counts as two).
The construction in the paper uses a tower of variables: for , the coordinates form generation , each consecutive pair of generation has a successor in generation ( has parents ), and the single variable of generation is . It also uses an explicit linear system (8) in variables , , with trigonometric coefficients , , , whose accuracy is .
There is an absolute constant such that for every positive integer and every , admits a polyhedral -approximation with
The constant is not fixed; the goal asserts only the order of growth, which is what the paper claims.
The theorem shows that conic quadratic constraints are, up to a factor logarithmic in the accuracy, no more expensive to express as linear constraints than they are in their native form. Consequences listed in the paper include approximating convex quadratically constrained quadratic programs, robust counterparts of linear programs with ellipsoidal uncertainty, and problems with low-dimensional cones (Coulomb friction, ; truss design, ) by linear programs of comparable size. Together with the matching lower bound of §3 of the same paper (a separate mission of this series), it pins down the size of the best polyhedral approximation up to constants. The recursive halving of dimensions through the tower of 3-dimensional cones is a reusable device for other rotation-invariant cones.
The result is proved in the paper; as far as is known it has not been machine-checked. This mission produces a formal proof of the construction, including the trigonometric estimate and the explicit linear encoding with its size count. Explicit values of the absolute constants are welcome as additional results.
The planar estimate is the core. Part (ii) of Proposition 2.1 must hold for every solution of the inequality system (8), not only for the solution one would write down for a given point of ; an argument that tracks only the intended solution proves part (i) and nothing about part (ii). The accuracy must also come out as , geometric in ; a bound that decays only polynomially in would give size instead of . The naive idea of approximating directly by tangent hyperplanes is ruled out by the exponential facet count mentioned above; the auxiliary variables are indispensable. The second difficulty is bookkeeping: packaging copies of system (8) on a tower of depth into a single linear map, counting its variables and inequalities exactly, handling that is not a power of two, and summing the accuracies so that the total size is rather than .
Fin k → ℝ. The norm is written out as eucNorm y = Real.sqrt (∑ i, y i ^ 2); the norm Mathlib attaches to Fin k → ℝ is the sup norm, under which the cone would be polyhedral and the theorem trivial.(Fin k → ℝ) × ℝ × (Fin p → ℝ) →ₗ[ℝ] (Fin q → ℝ) and is the componentwise order. Linearity is essential: with an arbitrary map, would be an exact approximation with , . Affine maps are not allowed either; the paper's approximations are homogeneous.Real.log.Y ℓ i with 0-based i, so the parents of Y ℓ i are Y (ℓ-1) (2i) and Y (ℓ-1) (2i+1); the milestones on (6)–(7) and (10) are stated on solution sets rather than on an explicit linear map. The size counts of (10) (properties 1–2) are not separate milestones; the arithmetic milestone on records the bound on to which they reduce.A complete development needs: elementary trigonometry of (available in Mathlib), rotations in the plane, finite products and sums over , and a way to assemble many small linear systems into one linear map with an exact count of rows and columns. The last piece, and the tower of variables with the reduction from arbitrary to a power of two, are reusable for other lifted polyhedral approximations. Contributions of any milestone, of explicit linear encodings of (8) and (10), and of the extension from to all are welcome.
Quadratic programming, the minimization of a convex quadratic function subject to linear constraints, is the simplest nonlinear extension of linear programming. It arises in least-squares estimation with sign constraints, in portfolio selection, and as the subproblem solved at each iteration of Newton-type methods for general smooth convex programs. E. M. L. Beale's 1955 paper (DOI 10.1111/j.2517-6161.1955.tb00191.x) gave one of the first finite algorithms for it by extending Dantzig's simplex method: the method keeps the simplex tableau and adds free variables, linear functions of the original variables with no sign restriction, along which the quadratic stops decreasing.
Timeline:
There are restricted variables satisfying linearly independent linear equations, and a convex quadratic objective . The iteration keeps nonbasic variables , each either a restricted variable or a free variable, and writes every restricted variable as an affine function of them:
A restricted variable that is not nonbasic is basic. The associated solution sets every , so . The objective is written as
with symmetric. Thus is the value of at the associated solution and is its linear coefficient in . The number of nonbasic free variables is .
One step chooses a nonbasic that can profitably be altered: a free one with if there is one, otherwise a restricted one with . It orients so that it is to be increased, and increases it from . It stops at the first of two events. Either a basic variable reaches (the ratio test (2.4)), and then becomes nonbasic in place of . Or stops decreasing where the free variable vanishes (3.2), and then becomes nonbasic in place of . The coefficients are then transformed by substituting for (eqs. (3.4)–(3.6)). is in standard form when it has no linear term in any free variable.
From a tableau with symmetric , positive semidefinite quadratic block and consistent labels, there is no infinite run
of steps along which every basic variable stays strictly positive in the associated solution. No bound on the number of steps is claimed, as in the paper.
The theorem makes Beale's method an algorithm: a finite procedure that ends either at an optimal tableau (milestone 4) or with a ray along which decreases without bound. This finiteness is what later active-set methods for quadratic programming inherit.
The result was proved in 1955. What remains is to formalize it: a machine-checked account of a simplex-type method whose state includes variables that are created during the run and later discarded. Mathlib has no simplex-type algorithm for quadratic programming, and no machine-checked proof of this theorem is known. The pivot algebra (3.4)–(3.7) and the tableau model are reusable for other pivoting methods for quadratic programs.
The argument for linear programming does not carry over. There, the objective strictly decreases and a basis is a subset of a finite set of columns, so no basis repeats. Here each step may create a new free variable, and nothing bounds the number of distinct free variables that can occur. Tableaux are therefore not drawn from a finite set, and a strictly decreasing objective alone does not give termination. The paper states this itself: "there is no obvious limit to the number of free variables that may be involved". The difficulty is to bound the number of steps between returns to a well-behaved tableau, and this depends both on the rule that free variables are chosen first and on how the coefficient matrix evolves under repeated pivots.
Fin (N+1). Slot 0 is ; the nonbasic slot k : Fin N is index k.succ. A pivot stores the new nonbasic variable in the slot of the variable it replaces, so the paper's index in (3.4)–(3.7) is that slot. The tableau holds the labels (restricted or free), the rows of all restricted variables (a nonbasic one has the unit row), and . Free variables carry no row, as in the paper.pivotC is computed literally from (3.5) and then (3.6). Rows are transformed by the same substitution, as the paper states.Contributions are welcome on every milestone. The algebraic milestones 1–3 are self-contained.
In a linear regression with many more candidate variables than observations, least squares is not defined uniquely and does not estimate anything useful. The Lasso (Tibshirani, 1996) replaces it by an -penalised least-squares problem, which is convex, can be solved at scale, and returns sparse coefficient vectors. The question that a statistician, a signal-processing engineer or an operations researcher fitting a sparse model must answer before trusting it is quantitative: how far is the Lasso estimate from the true coefficient vector, how well does it predict, and how many variables does it select, as functions of the sample size , the number of variables and the sparsity of the truth?
Bickel, Ritov and Tsybakov (arXiv:0801.1095, Ann. Statist. 37(4), 2009) answered this under the restricted eigenvalue (RE) condition, which they introduced, with explicit constants and an explicit failure probability. Their Theorem 7.2, the goal of this mission, is a standard reference result of high-dimensional statistics and a model for the Lasso analyses in the textbooks of Bühlmann and van de Geer (2011) and Wainwright (2019).
Timeline, restricted to what each work proved:
A deterministic design matrix with columns is observed together with
where is unknown and has independent entries with . Throughout, , , and every diagonal entry of the Gram matrix equals .
For write , for the support, for the sparsity, and for the vector that agrees with on and vanishes off . The largest eigenvalue of is .
The Lasso estimator with tuning parameter is any minimiser
Minimisers exist but need not be unique.
Assumption RE (, ) asks that
Assumption RE (, , ) is the same with in the denominator, where and collects the largest in absolute value coordinates of outside .
Let , let RE hold, and let with . With probability at least , every Lasso solution satisfies
and, if RE holds, on the same event and for all ,
In the order in which the paper's proof uses them:
The result. Theorem 7.2 gives, for fixed and rather than asymptotically, the rate for the prediction loss and for the loss of the Lasso, under a condition on the design only (RE), with no assumption on how compares with . The dependence on is only logarithmic, which is what makes the Lasso usable when . Bound (7.9) shows that the Lasso selects at most a constant multiple of variables, and (7.10) covers every loss between and . Together with Theorem 7.1 for the Dantzig selector, the result shows that the two estimators have the same rates.
Formalizing it. The theorem is proved on paper. As far as a search of the platform shows, there is no machine-checked proof of a probabilistic Lasso rate. The closest platform statement, HighDimStat.SparseLinear.lasso_l2_error_bound (Wainwright, Theorem 7.13(a)), is deterministic, assumes a lower bound on the regularisation parameter in place of Gaussian noise, uses a restricted eigenvalue condition over the cone of one fixed support, and concludes an bound with a different constant. A formal proof of Theorem 7.2 would supply the Gaussian maximal inequality, the Lasso optimality conditions, and the cone and interpolation inequalities as reusable lemmas.
Each step is short on paper, and none of the steps is deep. The main work is in three places. First, the probability: the event on which the deterministic argument runs involves all correlations at once, and its probability must be bounded by exactly , which requires the law of a linear combination of independent Gaussians and a sharp Gaussian tail estimate, not a generic concentration bound with unspecified constants. Second, the Lasso is defined only through its minimising property, while the sparsity bound (7.9) is a statement about the number of non-zero coordinates of a minimiser of a non-differentiable objective; the characterisation (B.6) of minimisers is not in Mathlib. Third, (7.10) involves two restricted eigenvalue constants, a ranking of coordinates with possible ties, and real exponents, and every constant has to come out exactly.
The obvious idea of proving (7.7)–(7.10) for one fixed minimiser does not suffice: the statement quantifies over every minimiser on a single event.
The design is a Matrix (Fin n) (Fin M) ℝ; vectors are functions Fin M → ℝ. The noise is a family W : Fin n → Ω → ℝ of independent, measurable random variables with law gaussianReal 0 σ² on a probability space, and . The probabilistic conclusion is one measurable event with on which every minimiser of (7.2) satisfies all bounds; the event does not depend on the minimiser, on or on . is the natural logarithm.
RE and RE are stated through witnesses: a predicate " for every admissible and ", and the theorem holds for every witness . Because the paper's is an attained minimum, every witness is at most it and the bounds decrease in , so this is equivalent to the printed statement. The assumption quantifies over every with , as on page 7, not only over the support of . is the supremum of over unit vectors . Lemma B.1 is stated in its Section-7 specialisation (unit column norms, ), the form used in the proof of Theorem 7.2; (B.28) is stated for every and (B.27) likewise, since the paper writes them with and invokes them with . The printed Theorem 7.2 needs no correction; all four constants were checked against the proof.
A formalization in which the noise is not Gaussian, the Lasso predicate can be vacuous, the RE condition is imposed only on the support of , or the probability is that of a non-measurable set, is not this theorem and is ruled out by the statement.
Needed infrastructure: Gaussian tail bounds and the law of a linear combination of independent Gaussians (largely in Mathlib), subdifferential calculus for -penalised least squares, and elementary finite-sum inequalities. The cone inequalities (B.27)–(B.28), the interpolation inequality and the optimality conditions (B.6) are reusable in other sparse-estimation missions; contributions to any milestone are welcome.
In high-dimensional linear regression the number of unknown coefficients may be much larger than the number of observations , and the coefficient vector can only be recovered because it is assumed to be sparse: few of its entries are non-zero. Two convex estimators dominate this setting: the Lasso of Tibshirani (1996), an -penalized least-squares estimator, and the Dantzig selector of Candès and Tao (2007), which minimizes the norm subject to a bound on the correlation between the residual and the columns of the design. Both are used routinely in statistics, signal processing and machine learning, and their rates of convergence determine how many observations suffice to estimate a sparse vector.
Bickel, Ritov and Tsybakov (arXiv:0801.1095; Ann. Statist. 37(4), 2009) analysed the two estimators side by side under a single, weak condition on the design, the restricted eigenvalue (RE) assumption. This mission formalizes their rates for the Dantzig selector, Theorem 7.1 of the paper.
Timeline. Candès and Tao (Ann. Statist. 35, 2007) introduced the Dantzig selector and bounded its error under a uniform uncertainty principle on the design. Bickel, Ritov and Tsybakov (2009) replaced that condition by the RE assumptions, which are implied by it (their Lemma 4.1), and obtained bounds for every and a prediction bound, with explicit constants. Later work (van de Geer and Bühlmann, EJS 2009) compared RE with the compatibility condition and other design conditions.
Observations follow the linear model
where is a deterministic design matrix, , , is unknown, and has independent coordinates with . The columns are normalized: every diagonal element of the Gram matrix equals 1.
For , is its support and its sparsity; satisfies for an integer . Norms are and ; for an index set , keeps the coordinates of in and sets the others to 0, and is the complement of .
With a tuning level , , the Dantzig selector is any minimizer
The cone condition at an index set with constant is . Assumption RE asks that
Assumption RE is the same with in the denominator, where and collects the largest outside ; it is used for , .
With probability at least , every Dantzig selector satisfies
and, on the same event, if RE holds, simultaneously for all ,
In the order the proof of the paper uses them:
The result. Theorem 7.1 shows that, up to the factor , the Dantzig selector estimates an -sparse vector as well as least squares would if the support were known: the prediction error is of order , and the errors are of order . The bounds hold for any , including , provided only that RE holds, and every constant is explicit. The paper's Theorem 7.2 gives the same rates for the Lasso; comparing the two is the paper's main message.
Formalizing it. The theorem is proved in the paper; to the best of current knowledge it has not been machine-checked. A complete formal proof would provide: a verified Gaussian maximal inequality for the noise event, the deterministic cone and RE arithmetic that underlies essentially all -regularized estimation theory, and a reusable – interpolation lemma. Most milestones are deterministic and independent of the probability layer.
The obvious argument — compare with in Euclidean norm using the smallest eigenvalue of — fails because that eigenvalue is 0 whenever . The proof must instead show that the error vector lies in a cone on which is injective in a quantitative sense, and this uses the optimality of (not just feasibility) together with the event on which itself is feasible. The bound needs a second, stronger condition RE and a control of the tail of the error outside the largest coordinates. On the formal side, handling the non-uniqueness of the minimizer, real powers with exponent or , and the union over Gaussian tails with the exact constant all need care.
Vectors are functions Fin M → ℝ, the design is Matrix (Fin n) (Fin M) ℝ; the paper's dictionary of functions enters only through . The unit diagonal of is a hypothesis, not a normalization performed in the proof. The noise is W : Fin n → Ω → ℝ on a probability space, measurable, mutually independent, each of law ; is the natural logarithm. The Dantzig selector is a predicate (feasible and of minimal norm among feasible vectors), and every result is stated for every minimizer. RE and RE are stated through a witness (a number with the defining lower-bound property); is the largest witness and the bounds decrease in , so the statements are equivalent to the paper's while avoiding the value of a real infimum over an empty set. Two witnesses are kept apart: for RE in (7.4)–(7.5), for RE in (7.6). Ties in the choice of the largest coordinates are handled by quantifying over every admissible . The probability statement asserts one measurable event with on which all three bounds hold for every minimizer, every admissible , every witness and every .
The event is fixed before the minimizer is quantified, so a formalization in which the event depends on , or in which RE is a hypothesis about the random error vector rather than the design, would be a different (weaker) statement and is not accepted. The deterministic milestones (B.26)–(B.29) take the conclusion of (B.25) as a hypothesis; they are true for every vector satisfying their hypotheses and are not restricted to the event.
A complete development needs Gaussian tail bounds and a union bound (Mathlib's gaussianReal), finite Hölder-type inequalities for real exponents, and elementary sorting arguments for the tail outside . The cone, RE and interpolation lemmas are reusable for the Lasso (Theorem 7.2, a sister mission) and beyond. Proofs of any milestone are welcome independently.
Two estimators dominate sparse high-dimensional regression, where the number of candidate regressors can far exceed the sample size . The Lasso (Tibshirani, 1996) minimises a least-squares criterion plus an penalty. The Dantzig selector (Candès and Tao, 2007) minimises the norm of the coefficients subject to a bound on the correlation between the residual and the regressors, and is computed by a linear program. They were proposed independently and first analysed under different assumptions: sparsity oracle inequalities for the Lasso (Bunea, Tsybakov and Wegkamp, 2007) and bounds for the Dantzig selector under a uniform uncertainty principle (Candès and Tao, 2007). A practitioner choosing between them needs to know whether guarantees for one say anything about the other.
Bickel, Ritov and Tsybakov (arXiv:0801.1095; Ann. Statist. 37(4), 2009, doi:10.1214/08-AOS620) analyse both estimators in parallel under one assumption on the design, the restricted eigenvalue condition. Their main message is that, under sparsity, the two estimators "exhibit similar behavior" (p. 2). Section 5 makes this precise: the prediction losses of the two estimators are close. The result holds in a nonparametric model: the regression function need not be a combination of the regressors. This mission formalizes that comparison, Theorem 5.1 of the paper.
Let be real functions (the dictionary) on a set , and fixed design points, with and . The design matrix is . Observations are , where is an unknown function and are independent with . Write , and , so .
The empirical norm of is . Every column has , and . For , has value vector . The support is and the sparsity is . For , agrees with on and vanishes elsewhere.
Fix . The Lasso is any minimiser of
With , the Dantzig constraint is . The Dantzig selector is any vector of smallest that satisfies it. The estimators are and .
Assumption RE with , asks that
Throughout, , where is the natural logarithm.
Assume RE with , and let . With probability at least , every Lasso solution with and every Dantzig selector satisfy
The proof uses one probabilistic event and two one-sided deterministic inequalities.
Assume for all and RE. With probability at least , whenever ,
The result. Theorem 5.1 bounds the gap between the two prediction losses by the rate of a sparse regression with parameters. The bound carries a factor that measures how ill-conditioned the Gram matrix is on sparse vectors. A prediction bound for one estimator therefore transfers to the other at this cost. The paper uses this transfer in Proposition 6.3, which combines Theorem 5.1 with the Lasso oracle inequality of Section 6 to derive an oracle inequality for the Dantzig selector. The theorem requires no assumption relating to the dictionary.
Formalizing it. The result has been proved since 2009, and this mission formalizes that proof. None of the objects involved exists on Prove2Me yet: the weighted Lasso, the Dantzig selector and the Gaussian noise events. The Wainwright series on the platform defines a differently normalised Lasso with an unweighted penalty, a single fixed support and a different restricted eigenvalue condition, so it cannot be reused here. A machine-checked proof would also confirm the paper's constants, and the thresholds and , which appear in all later analyses.
Each estimator is defined only implicitly, as the solution of an optimisation problem, and neither need be unique. Comparing their losses directly gives plus with . A crude bound on the cross term, , yields an error proportional to . This does not produce the sparse rate unless is controlled by . That control needs to lie in the restricted eigenvalue cone at the support of the random, data-dependent vector . The restricted eigenvalue condition must therefore hold uniformly over supports of size at most ; a condition for one fixed support does not suffice. The probabilistic part is a union bound over Gaussian coordinates, and it must be arranged so that a single event serves every minimiser of both programs.
The dictionary and the design points enter every statement only through and , so the Lean statements take X : Matrix (Fin n) (Fin M) ℝ and f : Fin n → ℝ directly, and is arbitrary. The noise is a family W : Fin n → Ω → ℝ of measurable, mutually independent random variables with law gaussianReal 0 σ², and . The Lasso and the Dantzig selector are predicates (IsLasso, IsDantzig), and every theorem is stated for every solution. The Dantzig constraint is written coordinatewise as . The Lasso penalty and the Dantzig constraint are weighted by , and the Dantzig objective is unweighted, exactly as in the paper. Theorem 5.1 does not normalise the columns.
RE is stated through a witness: a real with on the cone, for all . The paper's is attained, so it is the largest witness. Every bound decreases in , so this reading is equivalent to the paper's and avoids a real infimum over an empty set. "With probability at least " becomes the existence of a measurable event with on which the conclusion holds for every Lasso solution and every Dantzig selector. The condition is imposed inside the event, per realisation. The milestones (B.2), (B.10), (B.15) and (B.17) are stated deterministically, on the noise events and as predicates on the noise vector; this is how the proof uses them. (B.4) is stated for every , which is stronger than the paper's and still true.
The goal cannot be made vacuous. For the probability bound is positive. Lasso solutions exist because and every , and Dantzig selectors exist because the Lasso is feasible. RE with holds for .
A complete development needs:
The noise-event lemmas and the Lasso optimality condition can be reused by the companion missions on this paper. Proofs of any milestone are welcome, including proofs that route (B.4) through Mathlib's sub-Gaussian API.