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?
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.
Classical non-cooperative game theory randomizes with objective, independent devices: each player spins a private wheel whose odds everyone agrees on. Aumann's 1974 paper (doi:10.1016/0304-4068(74)90037-8) asks what changes when the randomizing events are ordinary events of the world, about which players may hold different subjective probabilities and may be differently informed. The paper introduced correlated equilibrium, and it also separates two effects that the classical model fuses: subjectivity (players disagree about probabilities) and correlation (players peg their choices on common or dependent events).
This mission formalizes the paper's result on subjectivity without correlation. Example 2.3 of the paper exhibits a three-person game in which strategies pegged on subjective but mutually secret events form an equilibrium that every player prefers to every classical mixed equilibrium. Proposition 5.1 shows that this cannot happen with two players.
A game has a finite set of players, a finite set of pure strategies for each player, a finite set of outcomes and an outcome function from onto . Player has a utility ; write for .
A randomizing structure consists of a set of states of the world with a -field of events, a sub--field for each player (the events is informed about), and a probability measure on for each player (the subjective probability of ). A strategy of is a map whose level sets lie in . For a profile of strategies the payoff of is
computed under player 's own beliefs. An equilibrium point is a profile with for every player and every strategy of .
An event is -secret if and every other player regards as independent of every event in the -field generated by the , : . A strategy is mixed if its level sets are -secret, and objective if each level set has the same probability under every . A measure is non-atomic on a -field if every event of of positive measure contains an event of of strictly smaller positive measure; a roulette is a sub--field of on which every is non-atomic. Throughout, Assumption II holds: every player has a -field of -secret events on which every is non-atomic.
For distributions on the classical payoff is , and is a Nash equilibrium point if no player gains by switching to another distribution.
Let and assume
Then for every equilibrium point in mixed strategies there is an equilibrium point in objective mixed strategies with
The game need not be zero-sum.
The result. Proposition 5.1 isolates correlation as the source of the new equilibrium payoffs of the subjective model in two-person games: disagreement about probabilities alone, with strategies pegged on secret events, reproduces only payoffs already achievable by classical mixed strategies (by Proposition 4.3, only Nash equilibrium payoffs). The paper uses it to explain Example 2.9, where two zero-sum players both expect more than the value, as an effect of subjectivity combined with correlation. Proposition 4.3 is the bridge that embeds classical Nash theory in the subjective model; with Nash's theorem it gives existence of equilibrium points in every game.
Formalizing it. The results are proved in the paper; to our knowledge none of them has been machine-checked. The mission produces a reusable measure-theoretic model of randomized strategies with private information and subjective beliefs (secret events, mixed and objective strategies, roulettes), a non-atomicity notion relative to a sub--field, and the Lyapunov-type construction of Lemma 7.1, none of which exists in Mathlib at the pinned revision.
The equilibrium conditions quantify over all strategies of the deviator, i.e. all -measurable maps, and the deviator may know events on which the opponent's mixed strategy is pegged. The obvious computation of as a sum of products of marginal probabilities is valid only because the opponent's strategy is pegged on secret events, which is the content of Lemma 7.3; for correlated strategies it fails, and Example 2.9 shows the proposition then fails. A second obstacle is that the replacement must reproduce player 2's beliefs about , while player 1's own equilibrium condition is stated under ; condition (5.2) is what transfers " is played with positive probability" from one player's beliefs to the other's. Constructing objective strategies with prescribed probabilities (Lemmas 7.1 and 4.1) needs the convexity of the range of a non-atomic vector measure (Lyapunov's theorem), which is not in Mathlib.
Players are a finite type (Fin 2 in the goal, players ); the and are finite types, and is surjective. The -field is an explicit parameter mΩ of the structure RandomizingStructure ι Ω mΩ, which carries the and the probability measures . Probabilities are -valued Mathlib measures. Utilities and are data (Assumption I is used only to compare lotteries by expected utility; the uniqueness of is not encoded). is a Bochner integral; for strategy profiles the integrand has finitely many values and is measurable, hence integrable. Non-atomicity on a sub--field is defined directly; Mathlib's NoAtoms (singletons are null) would trivialize Assumption II and is not used. "Mixed" means pegged on the family of all -secret events, not on the -field of Assumption II. Classical distributions, and Nash equilibrium points are AGT.IsLottery, AGT.expectedPayoff and AGT.IsMixedNash from the published definition agt_games.
A formalization that restricted deviations to mixed or objective strategies, or dropped "mixed" from the hypothesis on , would state a different theorem and is ruled out.
Useful contributions: Lyapunov's convexity theorem for finite-dimensional non-atomic vector measures (or the special case needed for Lemma 7.1), the factorization of Lemma 7.3, and the payoff identities used in the proof of Proposition 4.3. The model definitions are shared in meaning with the companion mission on two-person zero-sum games.
The continuous-review policy — order a fixed quantity whenever the inventory position falls to the reorder point — is the textbook policy for a single item with random demand and a positive replenishment leadtime (Hadley and Whitin 1963). Its optimal parameters have no closed form, so practice routinely falls back on the deterministic economic order quantity (EOQ) model with backorders, whose optimum is explicit. How much the deterministic model misjudges the stochastic system's cost is therefore a practical question, and before Zheng (1992) it had been studied only numerically (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978).
Zheng's paper answers it analytically. This mission targets its Theorem 3, which brackets the optimal cost of the stochastic model by the optimal cost of the EOQ model with the same parameters.
Demands arrive at rate and orders arrive after a fixed leadtime . Each order costs ; holding and backorder costs accrue at rates and per unit per unit time. The leadtime demand is a nonnegative random variable with . The inventory cost rate at inventory position is the newsvendor cost
assumed to attain its minimum at a unique point .
For order quantity and reorder point , the long-run average cost is
Let be a reorder point minimizing , and define for , , and . The optimal order quantity minimizes over , and . Write and
the controllable cost, so that ; . The constant is the newsboy cost.
The EOQ model is the same construction with demand constant at : , with functions , , optimal quantity and optimal cost .
All three inequalities are part of the goal. The weaker remark after the proof, , drops the factor and is not the goal.
Theorem 3 says that randomness of leadtime demand raises the total optimal cost above the EOQ's, yet the controllable part of that cost — the part the order quantity actually trades off — is smaller than the EOQ's cost, scaled by . Combined with (Theorem 2 of the paper), the gap is at most the newsboy cost , independent of , so the EOQ cost is a good proxy when is large relative to . The same machinery yields the paper's Theorem 5, that using in the stochastic model costs at most more than the optimum.
The result was proved in 1992; no machine-checked proof is known to exist. Formalizing it requires the continuous model as a whole — optimal reorder points, the one-variable reduction through , and the area function — none of which is in Mathlib. The companion missions of this series formalize Theorems 2, 4 and 5 of the same paper on the same model.
The middle inequality compares minima of two different functions: pointwise follows from Jensen's inequality, but only after the reorder point of each model is chosen optimally, so the comparison has to pass through the definition of as a minimum over . The outer inequalities depend on Lemma 8, whose proof uses convexity of and a slope comparison (Lemmas 4 and 7). The paper argues these through first and second derivatives of and , which exist only when the leadtime demand has a smooth distribution; the formal statements assume no density, so a proof must either avoid derivatives or handle one-sided ones. Existence of optimal reorder points and of is asserted in the paper without a separate argument.
Everything lives in the namespace ZhengQR.CostBounds. The machinery (qrCost, reorderPt, idealPt, Hfun, Cfun, Afun, H0fun, C0fun, IsOptQty) is defined for an arbitrary and instantiated at the stochastic and at . A structure QRModel holds the parameters, the demand distribution (a probability measure on ) and the standing assumptions.
Conventions committed to:
A formalization in which were an arbitrary number, or an arbitrary positive real, would make the goal false or empty; both are tied to the model above.
Needed infrastructure: existence of minimizers of convex coercive functions on , differentiation of parametric integrals , and properties of the newsvendor cost (convexity, coercivity, Jensen). Most of it is reusable for any continuous-review inventory model. Proofs of any milestone, and of lemmas the paper uses but this mission does not list (Lemmas 2–5, 7), are welcome.
Howard's finite Markovian decision process (MDP) models a controller who, at each instant, observes the state of a system, chooses a decision, collects a reward and moves to a random next state with known transition probabilities. Howard's policy-iteration algorithm computes an optimal policy, and the model has been applied to inventory control, equipment replacement, quality control and marketing. Its weak point is the requirement that every transition probability be known exactly: in applications these numbers are estimated and are hard to measure.
Satia and Lave (Operations Research 21(3), 1973) relax this requirement. In their game-theoretic formulation, the controller knows only a set of admissible probability rows for every state–decision pair, and nature chooses the rows adversarially. This is the model now called a robust MDP with (s,a)-rectangular uncertainty, studied later by Iyengar (Math. Oper. Res. 2005) and Nilim and El Ghaoui (Oper. Res. 2005), who reprove and extend the dynamic-programming results for it. The paper gives a policy-iteration algorithm for the max-min criterion and proves that it terminates at an optimal policy. This mission formalizes that part of the paper (pp. 728–732).
Timeline:
There are finitely many states and, in state , a finite nonempty set of decisions . A transition under decision earns reward ; rewards are discounted by with . For every pair there is a nonempty, closed, convex set of probability rows , , . Nature's choice is a matrix : one row for every pair.
A pure stationary policy selects . Under its present value is the unique solution of equations (5),
Nature's minimum is , and the max-min return of criterion (2) is . A policy is max-min optimal if in every state.
The algorithm alternates two routines. Phase 1 (nature's policy evaluation) fixes , computes from the current rows, replaces each row at by a minimizer of over (6), and stops when the minima reproduce . Phase 2 (policy improvement) chooses in each state a decision maximizing the test quantity (7),
at , keeping on ties; if the algorithm terminates.
Along every run of Phase 2 steps,
and the terminal policy attains the solution of the equations (4) and is -optimal for every .
The goal certifies a complete algorithm for the max-min problem: it computes a policy that is optimal against the worst admissible transition probabilities, in all states at once, in finitely many improvement steps. Propositions 1 and 2 show that the dynamic-programming equations (4) characterize the max-min value and that neither side gains from randomization. The known-transition case (every a single row) recovers Howard's policy iteration.
On the platform, Howard-type policy iteration for known transitions has been formalized (the Bertsekas Dynamic Programming and Optimal Control missions); nothing with uncertain transitions exists. The results of this paper are proved in the literature (Satia's thesis, and in greater generality by Iyengar and by Nilim and El Ghaoui); none has a machine-checked proof. This mission produces the first formal robust-MDP model and robust policy-iteration theorem on the platform.
The obvious argument copies Howard's improvement lemma. It fails at two points. First, the value of a policy is itself the result of an inner optimization by nature, so comparing two policies requires comparing two different worst-case transition matrices; the matrix minimizing against is not the one minimizing against . Second, the proof of Proposition 4 as printed shows only that nature's values decrease and converge; that the limit is nature's optimum, over a continuum of admissible rows, needs a separate argument. Finally, Proposition 1 involves randomized strategies and probability measures on the uncertainty sets, and reducing them to pure strategies is the content of Propositions 1 and 2, not a definitional convenience.
States are a finite type S (nonemptiness is not needed: every statement is unchanged in meaning at and trivially true at ), decisions a family D : S → Type* of finite nonempty types. The model fixes these conventions and readings:
Equation (4) must not be collapsed to in its definition: that would make Proposition 2 true by definition. Similarly, the Phase 2 relation always has a successor and algorithm runs exist from every policy, so the goal is not vacuous.
Needed infrastructure: Neumann series for with stochastic , monotonicity of policy evaluation, existence of minimizers of linear functions on compact subsets of the simplex, and the contraction argument for the robust Bellman operator. These are reusable for any robust or known-transition MDP development. Proofs of any milestone, alternative arguments for Propositions 1 and 2, and extensions to the max-max criterion are welcome.
The traveling salesman problem with the triangle inequality asks for a shortest closed tour through points whose distances form a metric. It is NP-hard, so in practice tours are built by fast construction heuristics, and the natural question is how far such a tour can be from optimal in the worst case. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case analysis of the standard heuristics. Their results are reproduced in textbooks on approximation algorithms and combinatorial optimization, and they are the reference point against which later guarantees (Christofides' algorithm, the double-tree -approximation) are compared.
The simplest heuristic studied is the nearest neighbor algorithm (Bellmore and Nemhauser, 1968; the "next best method" of Gavett, 1965): from the current node, always move to the closest node not yet visited, and return to the start at the end. The paper shows that this greedy rule is never worse than logarithmic (Theorem 1) and that the logarithm cannot be removed (Theorem 2). This mission is about Theorem 2, the lower bound.
A traveling salesman graph on nodes is a complete graph with a distance that is symmetric, , nonnegative, , and satisfies the triangle inequality . A tour lists the nodes in a visiting order and returns to ; its length is the sum of the distances along it. OPTIMAL is the least length of a tour.
The nearest neighbor algorithm starts at an arbitrary node ; having reached , it moves to a node that minimizes over the nodes not yet visited, breaking ties arbitrarily; after the last node it returns to . The length of the resulting tour is written NEARNEIBER. Because the start node and the ties are free, one instance has in general several nearest-neighbor tours. A lower bound needs only one of them; an upper bound must hold for all.
The instances of the proof are built from a recursive family of weighted graphs. With (so ), the graph is a triangle with unit weights, and consists of two copies of joined through one new node by two edges of length and two edges of length . Each has nodes and a path from its start node to its middle node through every node, of length with , . The graph adds two closing edges to , and is the complete graph on the same nodes whose distance is the shortest-path distance of .
For each there is a traveling salesman graph with nodes and a nearest-neighbor tour on it such that
The statement is existential in both the instance and the run of the algorithm, exactly as in the paper.
The instance for is .
Theorem 1 of the same paper shows for every nearest-neighbor tour on every traveling salesman graph. Theorem 2 shows that this bound has the right order: no constant-factor guarantee holds for the nearest neighbor rule, and the gap between the two constants ( against ) is all that remains. This separates the nearest neighbor rule from the insertion rules analysed later in the same paper, of which nearest and cheapest insertion are within a factor of optimal. It is the standard example of a natural greedy heuristic whose approximation ratio grows with .
The upper bound, Theorem 1, is already on Prove2Me with a machine-checked proof (SupplyChainTheory.nearest_neighbor_bound); its statement notes that the lower-bound instances are not formalized there. This mission supplies them: an explicit recursive family of metric instances, the shortest-path computations that certify it, and the arithmetic of its ratio. The result is proved in the paper; to our knowledge it has not been formalized in any proof assistant. The construction (a recursively defined weighted graph with a closed-form shortest-path table) is also a reusable pattern for other worst-case lower bounds of greedy heuristics.
The arithmetic ((2.12) and the final inequality) is routine. The content is in properties a) and b). A shortest-path distance is an infimum over all walks, and property a) asks that no detour through the recursive structure is shorter than the direct edge, at every level of the recursion. The paper handles this by an induction on (2.13)–(2.17) that tracks only seven nodes per level, and argues that distances inside a copy of are not shortened by embedding it into . Property b) then needs that at each step of the chosen node is at least as close as every unvisited node, including nodes in the other copy and nodes reached through the start or right nodes; ties occur, and the claim is only that some resolution of them follows . Checking small cases by computer does not give either property for all .
Nodes of an instance are Fin n, a tour is a permutation of Fin n, the tour length is the sum over consecutive pairs including the closing edge, and OPTIMAL is a minimum over the finite set of permutations. The model is the paper's: symmetric, nonnegative distances with the triangle inequality. The distance structure also carries , a normalization not in the paper; the diagonal never enters a tour length. A nearest-neighbor tour is a permutation in which each step goes to a node at least as close as every unvisited node, from an arbitrary start with arbitrary ties.
Ratios are multiplied out: the goal is together with , the paper's standing assumption (1.1). is Real.logb 2 of , as printed. Because of the strict inequality and the conjunct , the all-zero distance does not satisfy the goal, so the statement cannot be met by a degenerate instance.
In the construction the nodes of , , are numbered from left to right (start node , middle node , right node ); in the left copy comes first, then the new node, then the right copy. Graphs are edge lists with real weights and is defined in exactly as in (2.11). The shortest-path distance is the infimum of walk weights over an inductive walk predicate; it would be for two nodes with no connecting walk, a case that does not arise because every and is connected. is defined by its difference equation; its identification with the length of the tour along is milestone 7. All construction statements assume .
A complete development needs a small library for shortest-path distances of finite weighted edge lists (symmetry, triangle inequality, attainment, behaviour under relabelling and under gluing two graphs at a few nodes); this part is reusable beyond the mission. Contributions welcome: proofs of any milestone, and such general shortest-path lemmas as separate theorems. Theorem 1 is not part of this mission.
Semidefinite programming (SDP) optimizes a linear function over the intersection of the cone of positive semidefinite matrices with an affine subspace. It contains linear programming as the diagonal case and is the computational core of relaxations in combinatorial optimization, control theory and polynomial optimization. Its standard duality theory, however, is weaker than that of linear programming. The Lagrangian dual of an SDP can have a strictly positive duality gap, can fail to attain its optimal value, and an infeasible semidefinite system need not have a certificate of infeasibility of the naive Farkas form. All the classical strong duality theorems for SDP therefore assume a constraint qualification such as Slater's condition (a strictly feasible point).
M. V. Ramana (1997, Math. Program. 77, 129–162) constructed a dual, the Extended Lagrange–Slater Dual (ELSD), whose size is polynomial in the data and which enjoys every property of linear programming duality for every SDP, with no constraint qualification. The same construction yields an exact theorem of the alternative for semidefinite feasibility and the complexity consequence that semidefinite feasibility lies in NP if and only if it lies in co-NP in the Turing model.
Timeline:
Let be natural numbers, the space of real matrices, and the symmetric ones. On the inner product is . For symmetric , means is positive semidefinite. The data are symmetric and . The primal SDP is
with feasible region , a spectrahedron. Define by and write for " and ".
For let be the set of tuples of real matrices with and, for ,
The need not be symmetric. and are the sets of last components and ; . The ELSD is
and Weak-ELSD is the same program with . For the milestones: the polar , the algebraic polar , and .
For all data :
Propositions 7(vi) and 7(vii) (facts on PSD matrices), Lemma 9 (annihilation ), weak duality over every , Lemma 10 (nested subspaces), Lemma 13 (), Corollary 14, Claims 17 and 16, the central Theorem 12,
the translation invariance of (§2.5), and system (14) (dual attainment at value 0). Theorems 19–21 (Farkas lemma for SDP, optimality condition, primal attainment) are further items stated on the same definitions.
The Duality Theorem gives SDP a dual with the full strength of linear programming duality for every instance, at polynomial size. Consequences in the paper: an exact theorem of the alternative for semidefinite feasibility (Theorem 19); semidefinite characterizations of optimality of a given point and of primal attainment (Theorems 20, 21); and the complexity results that semidefinite feasibility is in NP iff it is in co-NP in the Turing model and in NP ∩ co-NP in the Blum–Shub–Smale model (Theorem 25, not part of this mission). Theorem 12 separately gives an exact semidefinite description of the polar of any spectrahedron containing the origin.
The results are proved on paper and are classical. No machine-checked version is known to exist; the platform's existing SDP duality theorem assumes Slater's condition. A formalization would provide the first constraint-qualification-free SDP duality in Lean, together with reusable infrastructure on PSD matrices (range inclusion, ) and on polars of convex sets.
The obvious route to SDP strong duality separates the primal's value from the image of the PSD cone under a linear map and invokes a closed-cone Farkas lemma. That step fails: the linear image of the PSD cone need not be closed, which is exactly why Lagrangian duality has gaps. In this mission the obstruction reappears as the non-closedness of the algebraic polar (Lemma 13 only gives ). The difficulty is to show that finitely many, and at most , corrections by the sets close (Claims 16, 17), and to control dimensions in doing so. A proof by assuming closedness, strict feasibility or a Slater point is a different theorem.
Everything lives in the namespace ExactSDPDuality.ELSD, in one definition file. Matrices are Matrix (Fin n) (Fin n) ℝ, vectors Fin m → ℝ; "" is Mathlib's PosSemidef (which over ℝ includes symmetry); is the entrywise sum on all of ; is the dot product. The data carry symmetry hypotheses in every statement, as the paper assumes throughout. is encoded by sequences with , so ; for the index is . Optimal values are least upper and greatest lower bounds of the value sets, never real sSup/sInf. The polar is the one-sided polar. In §2.4 statements the standing assumption is a hypothesis. In Claim 16 the index satisfies , the range where is introduced, and is the rank of the span of .
Theorems 20 and 21 are printed with ; both are false as printed (counterexamples in the items) and are stated with the corrected that the paper's derivation from Theorem 6 gives.
Trivializing formalizations are ruled out: no Slater or other constraint qualification appears; the dual is the ELSD built from the recursively defined , not the Lagrangian dual or an arbitrary subspace; the range over all of , not only symmetric matrices (the paper's Example 4 needs a nonsymmetric ).
Needed infrastructure: PSD matrix facts (Proposition 7), bipolar theorem for closed convex sets containing the origin (Proposition 11), closedness arguments for linear images of cones, and dimension counting of subspaces of . Contributions of any milestone, of these general lemmas, and of alternative proofs (for instance via facial reduction) are welcome.
Many problems in optimization and equilibrium modelling reduce to a system of equations with that is continuous and locally Lipschitz but not differentiable. Complementarity problems rewritten through the min or Fischer–Burmeister functions, Karush–Kuhn–Tucker systems of nonlinear programs, and the gradients of augmented Lagrangians all have this form. Newton's method cannot be applied verbatim, because need not exist.
Qi and Sun (Math. Programming 58 (1993) 353–367) replaced the Jacobian by an arbitrary element of Clarke's generalized Jacobian and proved that the resulting method converges under a condition they called semismoothness, extending Mifflin's notion (SIAM J. Control Optim. 15 (1977)) from functionals to maps. The paper has two convergence results. Theorem 3.2 is local: near a semismooth root with nonsingular generalized Jacobian the method converges superlinearly. Theorem 3.3, the target of this mission, is global in the Newton–Kantorovich sense: explicit constants on a ball around the starting point guarantee that the iteration never leaves , that has exactly one zero in , and that the iterates converge to it with a computable error bound. The authors describe it as "an extension of the classical Newton-Kantorovich theorem" (p. 361), which is stated for smooth maps in Ortega and Rheinboldt's monograph.
Timeline.
Work in with the Euclidean norm ; for a linear map , is the induced operator norm. Let be locally Lipschitz. Write for the set of points where is differentiable and for the derivative at .
In Lean these are NonsmoothNewton.Global.clarkeJac, dirDeriv, SemismoothAt and IsNewtonRun, over EuclideanSpace ℝ (Fin n).
Fix , , the closed ball , and constants with .
Assume is semismooth at every point of and, for all and : is nonsingular,
with and . Then every run of (3.2) from stays in , every is nonsingular, has a unique zero in , , and
The theorem certifies, from data checkable on a single ball, that a solution exists, where it is, that it is unique there, and how far the current iterate is from it; (3.4) is an a-posteriori stopping criterion. It holds for every choice of , which is what implementations need, since they compute one element of and not the whole set. The result underlies the global and semilocal analysis of semismooth Newton methods for complementarity problems, variational inequalities and nonsmooth KKT systems, a line that continued through the 1990s and 2000s.
The theorem is proved on paper; no machine-checked version is known. The platform has no Newton–Kantorovich theorem, smooth or nonsmooth, and no Clarke generalized Jacobian. A complete formalization would supply both, and the definitions layer here (generalized Jacobian, one-sided directional derivative, semismoothness, Newton runs) is shared with the two companion missions on Qi and Sun's local convergence theorem and on semismoothness of augmented Lagrangian gradients.
The Newton map is set-valued: depends on the choice of , so the Banach fixed-point theorem for a single contraction does not apply directly, and the argument must hold for every sequence of choices. The contraction estimate needs both consecutive steps to start inside , so containment in and the geometric decay of the steps must be established together. Identifying the limit as a zero requires a uniform bound on , which is not a hypothesis: it has to come from local Lipschitz continuity through the structure of the generalized Jacobian. Uniqueness uses an element , whose existence rests on Rademacher's theorem. Finally, the directional derivative in the hypotheses is only meaningful because semismoothness makes it exist.
The space is EuclideanSpace ℝ (Fin n), so the norm is Euclidean, as in the paper (p. 356), and is the operator norm. Local Lipschitzness is global (LocallyLipschitz F), the standing assumption of Section 3. Conventions:
fderiv along sequences in ; no closure is taken (the limit set is compact for locally Lipschitz ).Ring.inverse is not used.dirDeriv, a limUnder along , used only at points of , where semismoothness makes the limit exist.The goal is the full four-part conclusion: containment, existence, uniqueness, and convergence with (3.4). A formalization that proves only that the iterates converge to some zero, or that treats as possibly empty so that the hypotheses become vacuous, is not the theorem. The hypotheses are satisfiable by genuinely nonsmooth maps, e.g. on with a ball containing the kink.
A complete development needs: nonemptiness and local boundedness of the generalized Jacobian (Rademacher's theorem, available in Mathlib as LipschitzWith.ae_differentiableAt); geometric-series and Cauchy-sequence arguments in a complete space. The generalized-Jacobian facts are reusable well beyond this mission. Contributions of any of the milestones, or of these general facts as separate lemmas, are welcome.
Bin packing asks how to place a list of items with sizes in into as few unit-capacity bins as possible. It models the cutting of stock material, the packing of files onto tracks of a disc and the assignment of jobs to machines with a common deadline. Deciding the optimum is NP-hard, so in practice simple rules are used, and the question is how far they can stray from the optimum in the worst case.
Johnson, Demers, Ullman, Garey and Graham (SIAM J. Comput. 3(4), 1974) gave the first sharp worst-case bounds for the four classical rules. For First-Fit Decreasing (FFD), the rule that sorts the items into nonincreasing order and then places each into the first bin with room, they announced the bound , whose full proof in Johnson's thesis exceeds 75 pages. To show the method, Section 4 of the paper proves a simpler bound in detail: when no item exceeds , FFD uses at most bins. That result is the subject of this mission.
Timeline:
A list is a finite sequence of real numbers in ; values may repeat. A bin has capacity ; its level is the sum of the numbers in it. The optimum is the least number of bins into which the elements of can be placed with no bin level exceeding .
First-Fit places in order into bins , each initially at level : goes into the bin of least index whose level satisfies . First-Fit Decreasing first arranges into nonincreasing order and then runs First-Fit. is the number of bins it uses.
The proof uses a weight on finite sets of elements. For an integer , is a -piece if , and a -bin is a bin whose largest element is a -piece. Set . A pair obeys relation if is a -piece and ; then , and otherwise . For a partition of into one- and two-element sets, with each pair ordered (earlier, later) in the nonincreasing order,
BASIC is the set of elements of that are -pieces lying in a -bin of the FFD packing of , for some ; SURPLUS is the rest of .
The constants are those printed in the paper. The multiplicative constant is best possible.
A companion item states the Remark after Theorem 4.1: for every there is a list with all elements below , and .
Theorem 4.1 shows the weighting-function method in its simplest nontrivial form: a weight whose total is within a constant of the algorithm's bin count, and which no feasible bin can exceed by more than the target ratio. The same method, with more elaborate weights, gives the bound for FFD, and it is the model for later worst-case analyses of packing heuristics. The Remark shows that is exact for items in , and the Corollary on p. 322 extends the analysis to the asymptotic ratio when items are bounded by .
The source proof is partial. The billing argument behind Claim 4.2.2 is given only when two auxiliary conditions (G1) and (G2) hold ("The more intricate argument here omitted", p. 321), and Lemma 4.3 is checked in four of about seventy-four cases ("leaving the remaining 70-odd, more or less routine, cases to the ambitious reader", p. 321). Complete details are in Johnson's thesis. The theorem itself is established. A formalization therefore gives the first complete, checked proof in a single place. The finite case analysis of Lemma 4.3 is well suited to machine checking. No machine-checked proof of any FFD bound is known to exist.
The obvious weight alone fails. Claim 4.2.1 shows that covers the FFD bins, but many sets of elements with sum at most have , for example two -pieces, a -piece and a -piece. The pair discounts of repair Lemma 4.3, but they must then be paid for in Lemma 4.2, for every partition. That is Claim 4.2.2: a charge from each discounted pair to distinct SURPLUS elements that are no larger. The charge is straightforward only when no member of a pair obeying relation lies in a bin of type . In general a pair's larger element may already have been charged by a smaller relation, and the paper omits the argument that handles this. Lemma 4.3 is elementary but has many cases, each determined by the piece types in and the relations they obey.
A list is L : List ℝ with IsList L ( for each element) in every statement. is optBins L, the least such that some map from positions to Fin b has every bin sum at most . The First-Fit run keeps the nonempty bins as a List (List ℝ), and opens a new bin at the end exactly when no existing bin fits, which is the paper's "least ". The fit test is . FFD is First-Fit on sortDesc L, the mergeSort into nonincreasing order; ties do not affect the bin count. Indices are -based.
sorts into nonincreasing order and minimises over the involutions of its positions: fixed points are singletons, and a pair is oriented (larger, smaller). The minimum is over a finite nonempty set, so it is attained. BASIC is a set of positions of sortDesc L, and each position's bin is its bin in the final FFD packing. In , is the piece type of the first element. Sums are over Finset.Icc 2 (N - 1) with .
The goal's range is . The restriction to belongs only to the proof, through Lemma 3.3. Stating the goal for , weakening or , or making an unattained infimum would each change the theorem. Only the FFD half of Lemma 3.3 is stated. Claim 4.2.1 is stated with Lemma 4.2's standing hypothesis . The Remark's printed range is a misprint: its FFD packing needs , and the companion item states only the existence claim.
Infrastructure needed: a usable API for the First-Fit run (the invariants of the fold, bin levels, the order of bins), a lemma that FFD bins receive items in nonincreasing order, and a decision procedure for Lemma 4.3's case analysis over piece types. The model file and the weight file are reusable for the bound (mission 3 of this series) and for the bounded- corollaries. Contributions of proofs of Lemma 4.3 by computer-checked case enumeration, and of the missing general case of Claim 4.2.2, are especially welcome.