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.
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?
Linear programs solved in practice carry data that are measured, estimated or rounded. Ben-Tal and Nemirovski (Math. Program. 88, 2000) examined the NETLIB collection of real-world LPs and found that in 13 of them a relative perturbation of only 0.01% in the "ugly" coefficients of the inequality constraints can make the nominal optimal solution more than 50% infeasible (§2.3). Their remedy is the robust counterpart methodology: replace the nominal problem by a deterministic problem whose feasible solutions remain nearly feasible for every, or for all but a small probability of, data realizations.
The paper made the approach concrete for entry-wise uncertainty and gave the probabilistic guarantee that became a standard tool of robust and chance-constrained optimization. The main steps of the history are:
An uncertain linear program is
with , , , and bounds , . For each inequality row a set lists the uncertain entries , . Only these entries are uncertain; are exact.
Given an uncertainty level and a feasibility tolerance , write .
The robust counterpart (RC[ε, δ, Ω]), with a safety parameter , has variables , , and constraints , , , for all , and
The interval robust counterpart (IRC[ε, δ]) has variables and the constraint with , besides the nominal ones. Problem (∗) is the same with replaced by .
If extends to a feasible solution of (RC[ε, δ, Ω]), then is feasible for (LP) and, for every ,
Proposition 1 turns a probabilistic requirement, which is hard to handle directly, into a single convex (second-order-cone) program. The bound does not depend on the dimension, on the number of uncertain entries, or on which symmetric distributions the perturbations follow, so can be chosen from the desired reliability level alone. Together with milestones 3–6, the mission certifies the whole chain: the worst-case notion of reliability is exactly Soyster's linear program (IRC), and (RC) is never more conservative than (IRC), with an advantage that can reach the factor .
The results are proved in the paper; to our knowledge none of them is machine-checked. A formal development produces a reusable model of entry-wise uncertain LPs, the counterparts (∗), (IRC) and (RC) as Lean predicates, and a Hoeffding-type bound for weighted sums of symmetric bounded variables in the exact form (1). The platform's HighDimProb.Concentration.hoeffding_rademacher covers the Rademacher special case only.
The deterministic parts (milestones 1, 3–7) are elementary: worst cases of interval perturbations, and the Cauchy–Schwarz inequality. The obstacle lies in the probabilistic step. The printed proof passes from to with an equality that holds only in distribution, and contains index misprints, so it cannot be transcribed line by line; the reduction has to be restated pointwise. Eq. (1) is a tail bound for general symmetric variables in , not only for random signs; the step (c) of the printed proof of (1) is written as an equality that holds only for random signs, so that proof too needs repair. The degenerate case must be handled rather than assumed away.
UncertainLP n p m over Fin indices (0-based), with A : Matrix (Fin m) (Fin n) ℝ, J : Fin m → Finset (Fin n) arbitrary, and EReal bounds so that infinite bounds are expressible. The objective is omitted: no statement involves it.IsProbabilityMeasure; the name avoids a clash with the safety parameter . Symmetry is equality of the laws of and ; values lie in at every outcome; independence is required within each row only, with no identical distribution (§3.1 says only "independent", which is weaker than the "iid" of §2.2). Probabilities are P.real.A two-sided market in which each seller owns one indivisible good (a house, in the paper's example) and each buyer wants at most one is the simplest model in which prices emerge from bargaining between individuals rather than from a supply curve. Shapley and Shubik, The Assignment Game I: The Core (Int. J. Game Theory 1 (1971)), treat this market as a cooperative game with transferable utility and describe its core, the set of payoff divisions that no group of traders can improve upon by trading among themselves. The paper is the foundation of the literature on assignment markets, auctions of heterogeneous items, and two-sided matching with money.
This mission formalizes the paper's structural result on the shape of the core, Theorem 3 (p. 121): among all core outcomes there is a high-price corner in which every seller simultaneously receives the highest payoff available in the core and every buyer the lowest, and a low-price corner with the roles reversed; these two corners are the farthest-apart pair of core points. The authors note (p. 121, footnote 2) that a similar theorem for markets without money is proved by Gale and Shapley (1962), where it becomes the existence of seller-optimal and buyer-optimal stable matchings.
Let be a finite set of sellers and a finite set of buyers, with and not necessarily equal. For each seller and buyer a number is given: the gain the pair can realize by trading (Eq. (2.5), p. 114; Sec. 2.3, p. 116).
A coalition is described by its seller part and buyer part . A matching inside is a set of seller–buyer pairs in which no player occurs twice. The characteristic function (Eq. (2.6), p. 115) gives the coalition the best total gain it can realize by pairing its members:
A matching of the whole market attaining is an optimal assignment.
A payoff vector is a pair with (sellers' payoffs) and (buyers' payoffs). The core (p. 118) consists of the payoff vectors with
Singleton coalitions have worth , so core vectors are nonnegative; the paper calls them "imputations in the core".
For a seller , write and for the highest and lowest value of over the core; for a buyer , write and likewise.
The low-price corner and the high-price corner are in the core, and for all core vectors , ,
Milestone 5 is the strongest form of the distance clause of the goal: it gives the same conclusion for every distance that depends only on the absolute values of the coordinate differences, as the paper remarks on p. 122.
The result. Theorem 3 says that the core of an assignment market is elongated along the direction of market-wide price movements: "intergroup allocations are relatively indeterminate, intragroup allocations are relatively precise" (p. 121). The high-price corner is the outcome most favourable to all sellers at once, and the low-price corner the one most favourable to all buyers; that such simultaneous optima exist is a property of this game, not of cores in general. The low-price corner, the buyers' optimum, is the outcome reached by the ascending multi-item auction of Demange, Gale and Sotomayor (J. Polit. Econ. 94 (1986)), and the lattice structure underlies the incentive analysis of assignment mechanisms.
Formalizing it. The theorem is classical and fully proved in the paper; Prove2Me has no formalization of it, and nothing on the platform treats transferable-utility assignment games (the platform's stable-matching material concerns the non-transferable-utility model). The mission produces a reusable definition of the assignment game and its core, the lattice property of the core, and the extremal-corner theorem, stated with the core's extrema defined intrinsically rather than as parameters.
The proof in the paper takes a finite family of core vectors realizing all the extremal values and applies the Lemma repeatedly (p. 122). That argument presupposes that each extremum , , , is attained by some core vector, which the paper takes from the core being a nonempty polytope without stating it separately. Nonemptiness is itself the substantive result of the paper's linear-programming analysis (Theorem 2, via the duality theorem and the integrality of the assignment polytope), and it is not available here as a black box. The other nontrivial point is the Lemma's efficiency claim: that the coordinatewise min/max vectors still distribute exactly , which depends on the structure of an optimal assignment and fails for the naive combination .
Fintype); either may be empty and is allowed. The matrix is a : M → N → ℝ, and every theorem carries the paper's standing assumption as a hypothesis. No other hypothesis is added.(A, B) : Finset M × Finset N. Matchings are finsets of pairs with injective projections. The paper maximizes over exactly disjoint pairs; the formalization maximizes over matchings of every size, which gives the same value because .worth, since v denotes buyers' payoffs.Set ((M → ℝ) × (N → ℝ)) defined by (3.5) and (3.6) over all coalitions, with no separate nonnegativity clause (it follows from singleton coalitions).uHi, uLo, vHi, vLo are sSup/sInf in ℝ of the image of the core under a coordinate. On an empty or unbounded set these return ; the goal does not assume the core nonempty or bounded, so it is not vacuous and does not hide milestones 1–2 as hypotheses. The goal's membership clauses imply attainment of the extrema.dist on a product of function types is the sup-distance and is not used.sSup/sInf of compact coordinate images are reusable for any assignment-market or TU-matching development.Algorithmic stability asks how much the output of a learning algorithm changes when its training sample is perturbed. Since Devroye and Wagner (IEEE Trans. Inf. Theory 1979) it has served as a route to generalization bounds that does not go through the complexity of the hypothesis class. Bousquet and Elisseeff (JMLR 2002) popularised uniform stability, and Mukherjee, Niyogi, Poggio and Rifkin (Adv. Comput. Math. 2006) showed that for empirical risk minimisation in supervised learning, a leave-one-out type of stability is necessary and sufficient for consistency.
Shalev-Shwartz, Shamir, Srebro and Sridharan (JMLR 11, 2010) study stability in Vapnik's General Learning Setting, where uniform convergence can fail even though the problem is learnable. In Appendix A.2 they compare replace-one and leave-one-out (LOO) stability. For an empirical risk minimiser they prove that LOO stability is equivalent to consistency and to generalization, provided each property holds with one rate for all distributions (Theorem 31, p. 2667). This mission formalizes that theorem and the lemmas of Section 5.3 on which its proof rests.
Timeline:
A learning problem consists of an instance space with a -algebra, a nonempty hypothesis class , and an objective with for all . For a probability measure on :
A rate is a sequence that is non-increasing and tends to . A property holds universally if it holds under every with one and the same rate.
For an ERM :
The statement has no rates. Each side asserts that some rate exists and serves every distribution.
In the order the proof uses them:
Theorem 31 shows that for exact ERMs, LOO stability is not only sufficient but necessary for consistency. It transfers the supervised-learning characterisation of Mukherjee et al. to the General Learning Setting, where uniform convergence is no longer available as an intermediate. The hypothesis is sharp in one direction: Example 6 of the paper gives a universally consistent AERM that is not LOO stable. The equivalence therefore depends on exact minimisation, and an asymptotic minimiser does not suffice.
The lemmas are useful on their own. Lemmas 14 and 15 are the standard bridges between on-average generalization, generalization and consistency. Lemma 16 says that the minimal empirical risk estimates consistently in every learnable problem, even when no ERM learns. Lemma 16 also underlies Theorem 7, the paper's main characterisation of learnability, which is the subject of mission I of this series.
The results are proved in the paper. As far as is known they have not been formalized in any proof assistant. The platform has the textbook side of this framework (Shalev-Shwartz and Ben-David, Understanding Machine Learning, Chapter 13). Those statements are in and use a replace-one stability notion; they do not cover leave-one-out stability or the General Learning Setting.
The implications between stability and generalization change the sample size: has points, so a statement about the rule at size has to be compared with the rule at size under the marginal law of the reduced sample. The step from universal consistency to generalization needs Lemma 16. That lemma estimates from a sample on which the ERM itself may be inconsistent, and it is the only place where universality of the consistency rate is used. Per-distribution consistency of an ERM does not imply generalization (Example 1 of the paper). An argument that fixes throughout therefore cannot succeed.
Samples are tuples with law Measure.pi (the i.i.d. product), and is Fin.removeNth i S. A learning rule is a family . Its value at is never used, and LOO stability is required only for . is the infimum and no minimiser is chosen. An ERM is a rule attaining this infimum at every sample. A rate is non-increasing on and tends to . Universal properties are stated as "there exists with IsRate ε such that for every probability measure …", with the rate chosen before the distribution. The bound is any bound on ; the paper's is , and all its rates increase with .
Measurability is not discussed in the paper. The formalization assumes that each is measurable and that the rule is measurable in the sense that is jointly measurable. Lemmas 14–17 also assume that is measurable. For a measurable ERM this holds automatically, so Theorem 31 makes no such assumption. Without these assumptions Lean's integral of a non-measurable function is and every rate bound would hold trivially. For the same reason Utility Lemma 13 assumes integrable. The ERM hypothesis of the goal must not be weakened to an AERM: the statement would then be false (Example 6).
One statement corrects the printed text. In the second display of the proof of Theorem 31 (p. 2668), the chain adds and then drops it. The milestone states the bound the argument proves, . The rate-free Theorem 31 is unaffected.
The development needs product measures, independence and variance bounds, all available in Mathlib, and the marginals of Measure.pi under removal of a coordinate. The definitions of risks, rules and stability notions can be reused by other stability results. Proofs of any milestone are welcome, and so are alternative proofs of the goal.
Statistical learning theory asks when a rule that sees only an i.i.d. sample from an unknown distribution can return a hypothesis whose expected loss is close to the best possible. In supervised classification the classical answer is uniform convergence: learnability holds exactly when empirical risks converge to expected risks uniformly over the hypothesis class, and then empirical risk minimization (ERM) learns. Shalev-Shwartz, Shamir, Srebro and Sridharan (JMLR 11, 2010) showed that in Vapnik's broader General Learning Setting this picture breaks down. Their motivating example is stochastic convex optimization in a Hilbert space: minimizing an expected convex, Lipschitz objective over a bounded convex set from samples. This problem underlies regularized linear prediction, kernel methods and online-to-batch conversions, and the paper shows (§4.1) that in infinite dimension uniform convergence can fail and the plain empirical minimizer can fail to converge, while the problem is still learnable.
This mission formalizes the positive half of that example: Tikhonov-regularized ERM learns every such problem, with an explicit bound holding with probability (Theorem 3, p. 2644), through the stability of strongly convex empirical minimization (Theorem 2).
Let be a measurable space of instances and a real Hilbert space. A stochastic convex optimization problem consists of a nonempty, closed, convex, bounded set and an objective such that for every the map is convex and -Lipschitz on , each is measurable, and on . For a distribution on define the risk and optimal risk
and for a sample the empirical risk . A function is -strongly convex on if is convex there. The regularized empirical minimizer is
For the general part, a learning rule maps samples to hypotheses; it is an AERM with rate if , consistent with rate if , and uniform-RO stable with rate if replacing any one sample point changes the loss at any test point by at most on average over the replaced index (Definition 4).
If on , , , and , then with probability at least over
The constants are the paper's.
The result. Theorem 3 shows that every convex, Lipschitz, bounded stochastic optimization problem over a bounded subset of a Hilbert space is learnable at rate , with no dimension dependence and no uniform convergence. Together with the counterexamples of §4.1 it separates learnability from uniform convergence and from ERM, and it motivates the paper's general characterization: a problem is learnable if and only if it admits a uniform-RO stable asymptotic empirical risk minimizer (Theorem 7). Theorem 8 is the sufficiency half of that characterization and is reused wherever stability arguments give generalization bounds.
Formalizing it. The results are proved in the paper; to our knowledge none has a machine-checked proof. The closest platform material is the textbook treatment in Understanding Machine Learning, chapter 13 (Shalev-Shwartz and Ben-David): Corollary 13.9 (UnderstandingML.convex_lipschitz_bounded_learnable), Corollary 13.6 (rlm_lipschitz_stable) and Lemma 13.5 (strongly_convex_lemma). Those are stated in , bound the risk in expectation, use the regularizer over all of , and have different constants; the present mission works in an arbitrary Hilbert space, over a constraint set , with high-probability bounds and the paper's constants. Its definitions of learning rules, AERM, consistency and replace-one stability in the General Learning Setting are reusable by the other missions of this series.
The obvious route, bounding , is unavailable: §4.1 exhibits problems of exactly this type in which that supremum stays bounded away from zero for every sample size. Any successful argument therefore has to rely on a property of the learning rule rather than of the class , and the plain empirical minimizer does not have it: §4.1 shows it can stay a constant away from at every sample size. A second difficulty is purely formal: the regularization parameter depends on and , so the regularized minimizer changes with them, and all expectations involve a data-dependent hypothesis in a possibly non-separable Hilbert space, where measurability is not automatic.
Lean conventions, fixed for every item:
CompleteSpace E, never assumed finite-dimensional; is Hset : Set E, and all infima, suprema, strong convexity and Lipschitz conditions are taken on Hset only. is ⨅ h : Hset, F h.Fin m → Z, is Measure.pi, is Function.update S i z', and throughout.StrongConvexOn Hset λ, which is the paper's definition.No statement of the paper is corrected: all printed constants were checked against the proofs and are reproduced exactly.
A formalization in which the expected excess risk is a Bochner integral of a non-measurable or non-integrable function, or in which is an infimum over all of or over an unbounded family, would make the bounds trivially true; the measurability hypotheses, the bound and the infimum over the nonempty set rule this out.
Contributions welcome: proofs of the milestones in order, and in particular a reusable replace-one identity under Measure.pi, and Markov's inequality in the form used for high-probability bounds.
Many equivalence problems on finite structures reduce to computing the coarsest partition of a finite set that is compatible with a relation. Deciding whether two states of a finite labelled transition system are bisimilar, testing congruence of finite-state processes in Milner's calculus of communicating systems (CCS), and minimizing a deterministic finite automaton are all instances. Kanellakis and Smolka studied the relational version in connection with CCS equivalence and gave an -time algorithm, conjecturing that was possible. Paige and Tarjan's 1987 paper answers that conjecture with an algorithm that has since become the standard method for bisimulation minimization in model checkers and process-algebra tools.
Timeline:
Let be a finite set with elements and let be a binary relation on ; write for and . For the preimage of is
A partition of is a family of nonempty, pairwise disjoint subsets of , its blocks, whose union is . A partition is a refinement of a partition if every block of lies inside a block of .
A set is stable with respect to if or : either every element of has an -successor in , or none does. A partition is stable with respect to if all its blocks are, and a partition is stable if it is stable with respect to each of its own blocks.
Given and an initial partition , the coarsest stable refinement of is a stable partition refining such that every stable partition refining is a refinement of . The relational coarsest partition problem asks for it.
The algorithms refine by the operation , which replaces each block of that meets both and its complement by the two blocks and . The set is a splitter of if .
The improved algorithm is analysed under the standing assumption for all : every element has at least one successor. (The paper reduces the general case to this one by a preprocessing step.)
For every run of the improved algorithm with refining blocks :
Items 1–4 are the correctness of the improved algorithm, which the paper deduces from that of the naïve one. Item 5 is the counting fact on which the bound rests.
The coarsest stable refinement of the partition of states by their labels is the bisimilarity relation of a finite transition system, so the goal certifies, for any sequence of choices, the correctness of the refinement loop at the core of bisimulation minimization. The halving count is the combinatorial half of the bound: once the implementation charges per refining block , the count bounds the total work.
The results are proved in the paper, some by one-line arguments and the elementary properties (1)–(4) not at all ("stated without proof"). No machine-checked proof of the Paige–Tarjan algorithm's correctness or of its halving count is known to be available in Lean or Mathlib. The mission produces a checked account of the invariant, the final correctness and the counting argument for every run, not only for a particular implementation.
The correctness of the improved algorithm is not a special case of the naïve one read off directly. An improved step refines by and by , and is a union of blocks of only because refines . The invariant that is stable with respect to every block of is what makes a stopping condition, and it holds initially only under the standing assumption. The naive idea of reusing Hopcroft's argument fails: for relations, stability with respect to and does not imply stability with respect to , which is why both refinements are performed. For the halving count, the refining blocks that contain a fixed element must be shown to be nested across steps, which requires tracking how blocks of are replaced.
Fintype with decidable equality, a decidable relation U → U → Prop. Partitions are Finset (Finset U) with an explicit predicate IsPartition (nonempty, pairwise disjoint blocks covering ); blocks are required to be nonempty, which the paper leaves implicit.Fin (K + 1), with the choices recorded. Every statement holds for every run, so no choice rule is fixed.2 * B.card ≤ S.card, is K + 1 ≤ n, is Real.logb 2 of cast to . The termination bound for the improved algorithm is not printed in the paper and is derived as in the proof of Theorem 2. Running times (, ) and the data structures of the implementation are out of scope.A Markov decision process (MDP) is solved by dynamic programming once its transition probabilities are known. In practice they are estimated from data, and the optimal policy of an MDP can be sensitive to estimation error: a policy computed from point estimates may perform much worse under the true transition matrices. Nilim and El Ghaoui (Oper. Res. 53(5), 2005) study the robust version of the problem, in which the controller minimises the worst-case expected cost when the transition matrices are only known to lie in given uncertainty sets, and motivate it with aircraft routing under uncertain weather.
Earlier work on MDPs with uncertain transition probabilities includes Satia and Lave (1973) and White and Eldeib (1994), which treat interval and set-valued transition models, and Givan, Leach and Dean (1997) on bounded-parameter MDPs. The robust Bellman recursion under a rectangularity assumption was obtained independently by Iyengar (Columbia technical report 2002, published as Robust dynamic programming, Math. Oper. Res. 30(2), 2005). This mission targets the finite-horizon result of Nilim and El Ghaoui: Theorem 1, which shows that the robust problem is solved by a recursion of the same shape as the nominal one and that the associated min–max game has a value.
The states form a finite set , the decision horizon is , and the action set is finite, nonempty and the same in every state. Costs are for , and there is a terminal cost . The system starts in a given state .
Write for the probability simplex. For every action and state , a nonempty set describes the possible -th rows of the transition matrix under . No convexity or closedness is assumed. The rectangular uncertainty property says the uncertainty set of the matrix is the product .
A controller policy consists of maps , and is the set of such policies. A policy of nature picks, for every stage, action and state, a row . The admissible set is , so nature may change the matrices from stage to stage. The expected total cost is
where the state evolves as a Markov chain with transition matrix from state . The support function of a set is . The robust recursion (7) starts from and sets
and for a fixed the evaluation recursion (10) starts from and sets .
together with three further statements. First, for every . Second, every policy that chooses actions attaining the minimum in (7) (rule (8)) achieves in the worst case. Third, every nature policy whose rows attain the suprema (rule (9)) forces the value on every controller.
Theorem 1 shows that, under rectangular uncertainty, robustness costs one inner optimisation per state and action: the expected continuation cost of nominal dynamic programming is replaced by the support function . The equality of the min–max and max–min values says that it does not matter whether nature commits before or after the controller. The optimal controller policy remains deterministic and Markov. The later sections of the paper build on this recursion. They cover the discounted infinite-horizon case, the gap between stationary and time-varying uncertainty, and the computation of for likelihood and entropy models, which the other missions of this series formalize.
The result is proved in the paper, and independently by Iyengar. It has no machine-checked proof that this mission is aware of. A formal proof yields a reusable development: a finite-horizon MDP with a forward-defined expected cost, the link between that expectation and backward linear programs, and the finite-horizon robust Bellman equation for arbitrary nonempty uncertainty sets.
The nominal Bellman recursion is standard. The robust statement is harder than "apply the nominal recursion under the worst matrix", because no single worst matrix need exist. The sets are neither closed nor convex, so the suprema in need not be attained, and is not compact. Minimax theorems for convex–concave or compact games therefore do not apply. The expected cost is defined forward, as an expectation over a Markov chain, while the recursions run backward, and connecting the two is part of the work. The max–min side needs nature policies that come within any tolerance of the value simultaneously at every stage, state and action.
Fin n and stages Fin N. Values are indexed by natural numbers, and only is meaningful. Vectors are Fin n → ℝ with the componentwise order.stdSimplex ℝ (Fin n). Nonemptiness is implicit in the paper: without it is empty, and a real supremum over an empty index is .sSup of . This is the true supremum because the set is nonempty and bounded above by .⨆ τ in the goal and IsLUB in the milestones, because the row sets need not be closed. Minima over the finite nonempty and over are ⨅. The argmax rule (9) is stated only for nature policies attaining the row suprema. The argmin rule (8) is stated for every attaining policy.High-dimensional statistics studies estimation when the number of parameters is comparable to, or larger than, the number of observations . The standard estimators in this regime are regularized M-estimators: minimise an empirical loss plus a penalty that encodes structure, such as the Lasso ( penalty, sparse vectors), the group Lasso (block norms, group sparsity) and nuclear-norm regularization (low-rank matrices). Before 2009 each of these estimators came with its own consistency proof. Negahban, Ravikumar, Wainwright and Yu (arXiv:1010.2731; Statistical Science 27(4), 2012, doi:10.1214/12-STS400) isolated two properties that these proofs share, decomposability of the regularizer and restricted strong convexity of the loss, and proved one deterministic theorem from them. The Lasso rates of Bickel, Ritov and Tsybakov (arXiv:0801.1095), rates under -sparsity, and group-sparse and low-rank rates then follow as corollaries. The framework is the organising principle of Chapter 9 of Wainwright's textbook High-Dimensional Statistics (Cambridge University Press, 2019).
Let be a finite-dimensional real inner product space with inner product and induced error norm . Given a loss , a regularizer and a constant , program (1) is
For a subspace write for the orthogonal projection of onto , and for the orthogonal complement.
The conditions of the paper's main theorem are (G1): is a norm, decomposable with respect to with ; and (G2): is convex, differentiable and satisfies RSC. The Lean development lives in the namespace UnifiedMEstimator.General, with these objects named IsNormFn, IsDecomposable, dualNorm, compat, setC, taylorErr, RSC and IsOptimal.
Under (G1) and (G2), if and , then every optimal solution of program (1) satisfies
The bound holds for every pair over which decomposes, and for every optimum, not only a distinguished one.
Theorem 1 reduces a consistency proof for a new regularized estimator to two checks: that the regularizer decomposes over a pair of subspaces adapted to the model, and that the loss is curved on the set , together with a bound on that is usually a concentration inequality. The paper derives from it the Lasso rate under restricted eigenvalue conditions, rates for weakly sparse (-ball) vectors, and group-Lasso rates; companion papers use it for low-rank matrix estimation, matrix completion and generalized linear models. Because the bound holds for every pair , it gives an explicit trade-off between an estimation error and an approximation error .
The theorem is proved in the paper's supplementary appendix. No machine-checked proof of it is known. On Prove2Me, Wainwright's textbook restatement (Theorem 9.19, HighDimStat.Decomposability.thm9_19_general_bound) is a related but different statement: its RSC condition is local, on a ball, with a tolerance proportional to , and it has extra side conditions and a different bound. A formal proof of the present goal certifies the deterministic core that every corollary of the paper relies on.
The obvious argument compares the objective at and at and applies RSC to the error. RSC, however, is available only on the set , not on all of : in high dimensions the loss is flat in many directions, so strong convexity fails. The work is to show first that the error lies in (Lemma 1, which rests on decomposability and the choice of ), and then to relate the regularizer to the error norm through the projections onto and . The distinction between and matters throughout: the compatibility constant is taken on the larger space , while the approximation error projects onto the complement of the smaller one. The bound comes from a quadratic inequality in , and the constants depend on how its terms are split.
Representation. The parameter space is an arbitrary finite-dimensional real inner product space E (equivalently with any inner product, as the paper allows); matrices are covered by the same abstraction. Subspaces are Submodule ℝ E, projections are Submodule.starProjection, and the gradient is Mathlib's gradient, under the hypothesis that is differentiable. The dual norm and are real suprema (sSup). They equal the paper's quantities because is required to be a genuine norm (nonnegative, definite, absolutely homogeneous, subadditive) and is finite-dimensional; . The tolerance is a real number entering as ; RSC contains and is quantified over exactly for the same pair and point as the decomposability. Every statement is for every optimal solution of program (1). The data are fixed and absorbed into , and is an arbitrary point: the paper's requirement that minimise the population risk is never used by the theorem and is dropped.
Corrections of the printed statements.
Trivializations ruled out. A regularizer predicate weaker than a norm would let the real suprema collapse to the junk value and make the condition or the term free; RSC over all of would be classical strong convexity, and RSC over the cone without the slack would make the goal false; decomposability without or with the bars misplaced changes the theorem. None of these is used. The example and a checked one-dimensional instance show that all hypotheses of the goal can hold simultaneously.
Infrastructure and contributions. A complete development needs: Hölder's inequality for a norm and its dual norm, boundedness of the two suprema in finite dimension, the decomposability inequality , the first-order characterization of convexity, and the solution of a scalar quadratic inequality. The dual-norm and compatibility-constant lemmas are reusable for every decomposable-regularizer mission. Proofs of the milestones, of the goal, and of the instance are all welcome.
The proximal map of a convex function is the basic building block of proximal-point, forward–backward, Douglas–Rachford and ADMM methods, which are used throughout large-scale convex optimization, signal processing and operator splitting. All of these methods treat as a nonexpansive operator and use the fact that it is a gradient. The questions this mission formalizes go back to the paper that introduced the map: J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), 273–299 (DOI 10.24033/bsmf.1625). Which maps are proximal maps, and how can a function be recognized as the "potential" of one?
Moreau's answer (Corollaire 10.c) is intrinsic. A map is a proximal map exactly when it is nonexpansive and selects, at every point, a subgradient of some convex function. This characterization is the Hilbert-space origin of later results on firmly nonexpansive operators and on resolvents of maximal monotone operators (Minty 1962; Rockafellar 1970). It is still how one checks that a given nonexpansive operator is a proximal map.
Throughout, is a real Hilbert space with inner product and norm .
The Lean names are GammaZero, conj, subgrad, IsProx, prox, IsProxMap, ContractsDistances, primitive, LessConvexThanQ, MoreConvexThanQ and IsProxPrimitive, all in the namespace MoreauProx.Characterization.
For every map ,
Nothing is assumed of beyond convexity.
Three further results of the paper are included as unmilestoned companions: Proposition 8.a ( implies ), Proposition 9.a ( is the only function equal to its dual) and Proposition 9.d (nonnegative combinations of prox maps with are prox maps).
The result. Corollary 10.c turns "is a prox map" into two checkable properties of , one metric and one variational, with no need to exhibit . Proposition 9.d is one consequence: closure of prox maps under subconvex combinations. Proposition 10.b gives the dual picture, which recognizes primitives of prox maps among the functions of by a Lipschitz condition on their subdifferential. The intermediate results are the standard toolkit of proximal analysis. They include the Moreau decomposition, the nonexpansiveness of , and the smoothness of the Moreau envelope (Remark 7.c) with gradient .
Formalizing it. All statements were proved in 1965 and are textbook material (Bauschke–Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., 2017, Ch. 12–14 and 24). None of them has a machine-checked proof in Mathlib, which has no class, no extended-valued Fenchel conjugate and no proximal map on a Hilbert space. A complete development here would give reusable infrastructure: the conjugate of extended-valued functions with the Fenchel–Moreau theorem, the proximal map and its nonexpansiveness, and the differentiability of the Moreau envelope. Downstream convergence proofs of proximal algorithms need this layer.
The necessity half of 10.c follows quickly from 5.b and 7.d once those are available. The sufficiency half is the hard one. Given only a nonexpansive and a convex with , one must produce with . The obvious move is to take to be something built from directly. This fails because the candidate is only defined through a duality that needs and a precise convexity comparison with . Neither is given, and neither follows from a pointwise argument. The intermediate milestones involve biconjugation of extended-valued functions, upper envelopes of affine functions in infinite dimension, and lower semicontinuity of functions taking . These are the places where finite-dimensional or finite-valued shortcuts do not apply.
Conventions committed to in Lean:
[NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]. Functions with values in are H → EReal.⨆ x, (⟪x, y⟫ : EReal) - f x, computed in EReal (a complete lattice).IsProx f z x says that minimizes . The function prox f picks such a minimizer by choice (junk value if none exists). Every theorem using prox assumes . A prox map is ∃ g, GammaZero g ∧ ∀ z, IsProx g z (p z).ConvexOn ℝ Set.univ). This is equivalent to the paper's -valued , because a subgradient at every point forces finite everywhere. The contraction condition is §10.a applied to .Trivializing formalizations are ruled out. The goal's is required to be convex and to have as a genuine subgradient at every point, with finite. excludes the constant , under which every point would minimize the proximal objective. No theorem applies prox outside , where its junk value would make statements vacuous.
Needed infrastructure: Fenchel–Moreau biconjugation for EReal-valued functions on a Hilbert space, existence of minimizers of coercive lsc convex functions (weak compactness of balls), and a Fréchet-derivative argument for the envelope. Contributions are welcome at every milestone. Also welcome are helper lemmas on EReal arithmetic for convex functions, and alternative proofs of 10.c via Minty's theorem on firmly nonexpansive maps.
Proximal maps are the basic building block of first-order methods for nonsmooth convex optimization: the proximal point algorithm, forward–backward splitting (ISTA/FISTA), Douglas–Rachford splitting and ADMM all proceed by evaluating maps of the form . The notion and its name come from J.-J. Moreau, who introduced proximal points in two 1962 notes in the Comptes rendus and gave the systematic theory in Proximité et dualité dans un espace hilbertien (Bull. Soc. Math. France 93 (1965), 273–299).
The central result of that paper, which Moreau calls the key proposition, links proximal maps to conjugate duality: every point of a Hilbert space splits uniquely into the proximal point of relative to a convex function plus the proximal point relative to its dual function. The identity is used throughout modern optimization, for example to compute the proximal map of a norm from the projection onto the dual-norm ball, and in the analysis of primal–dual splitting methods.
Timeline. Moreau (1962) announces proximal points and the decomposition along mutually polar cones. Moreau (1965) proves the general decomposition theorem for and derives from it the characterization of proximal maps and the maximal monotonicity of subdifferentials in Hilbert space. Rockafellar (Pacific J. Math. 33 (1970)) extends maximal monotonicity of subdifferentials to Banach spaces.
Let be a real Hilbert space with inner product and norm . Functions take values in the extended real line .
The class consists of the functions that are convex (their epigraph is convex in ), lower semicontinuous, and not identically .
The dual function of is
Two points and are conjugate with respect to and when ; the set of such is the subdifferential .
For and , the proximal point is the unique minimizer of
When is the indicator function of a nonempty closed convex set (zero on , outside), is the nearest-point projection .
Let and . For all ,
The decomposition theorem gives, for every , a unique splitting into a pair of conjugate points, and conversely identifies every conjugate pair summing to with the two proximal points. Special cases are the orthogonal decomposition along a closed subspace and its complement, and the decomposition along a pair of mutually polar cones (Corollaire 4.b). In the rest of Moreau's paper it yields that proximal maps are nonexpansive, that the Moreau envelopes of and add up to , and that the subdifferential of a function in is maximal monotone (Proposition 12.b). In algorithms it lets one evaluate from at no extra cost, which is the basis of dual and primal–dual proximal methods.
All results in this mission are classical and proved (Moreau 1965; see also Bauschke–Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., 2017, Thm. 14.3). What the mission adds is a machine-checked development. Mathlib contains convex functions, lower semicontinuity and Hilbert-space projections onto closed convex sets, but as of this mission's environment it has no Legendre–Fenchel conjugate for extended-valued functions on a Hilbert space, no proximal map and no maximal monotone operators. The Hilbert projection theorem is on the platform as FamousTheorems.hilbert_projection_theorem; it is the special case of Proposition 3.a for indicator functions.
The two directions of the goal are unequal. That conjugate points summing to are the two proximal points needs only the definition of the dual function. The converse must produce the conjugacy identity from the bare fact that minimizes , and a pointwise first-order argument is unavailable because need be neither finite nor differentiable anywhere.
The milestones carry the analytic weight. Proposition 3.a needs existence of a minimizer of a function that is neither continuous nor coercive by itself on an infinite-dimensional space, so compactness arguments in the norm topology fail. Biconjugation (§2.b) is the Fenchel–Moreau theorem, which requires a separation theorem in applied to a closed convex epigraph whose values may be .
Everything lives in the namespace MoreauProx.Decomposition, over {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]; the paper's is ⟪x, y⟫_ℝ. The following conventions are committed to:
H → EReal. (GammaZero) is the structure: never ⊥, not everywhere ⊤, convex epigraph in H × ℝ, and LowerSemicontinuous in the norm topology. The paper defines as suprema of nonempty families of continuous affine functions, other than , and states the equivalence with this description (§2.a); the second description is the one formalized. Weak and strong lower semicontinuity agree for convex functions, as the paper remarks, so no weak topology appears.conj f y = ⨆ x, ⟪x, y⟫_ℝ - f x in EReal; since a - ⊤ = ⊥, this matches both lines of (2.2).IsProx f z x: minimizes proxObjective f z u = ‖u - z‖ ^ 2 / 2 + f u. With Proposition 3.a it is equivalent to the paper's notation; no choice function is used.GammaZero f and g = conj f; the paper's " dual to each other" follows from this by §2.b, so the goal is not weaker than the paper's.innerDual), and is the predicate IsProj C z x (nearest point).A formalization that drops the requirement that be not identically , drops the factor , replaces the duality hypothesis by unrelated , or reads values through EReal.toReal would make the statement false or vacuous; the definitions above rule these out.
Contributions welcome: proofs of the three milestones and of the goal; reusable infrastructure for extended-valued convex analysis on Hilbert spaces (conjugates, subdifferentials, proximal maps), which the companion mission Proximité et dualité dans un espace hilbertien II builds on.
The generalized assignment problem (GAP) asks for the cheapest way to give each of tasks to exactly one of agents when every agent has a limited amount of a resource and different agents consume different amounts of it for the same task. It models assigning jobs to machines or computers, software tasks to programmers, commercials to time slots, and customers to single-source plants in capacitated facility location. The problem is NP-hard, so exact methods rely on lower bounds that are cheap to compute and strong enough to prune a branch and bound tree.
G. Terry Ross and Richard M. Soland (Mathematical Programming 8, 1975) gave such a bound. The relaxation that ignores the resource limits is solved by giving every task to its cheapest agent; the overloaded agents are then repaired by one small binary knapsack problem each, whose optimal values are added as penalties. Their paper then shows that this repaired bound is not an ad hoc heuristic: it is exactly the value of a Lagrangean relaxation of the GAP at an explicit choice of multipliers. This identity made the Ross–Soland bound the reference point for the later Lagrangean and column-generation methods for the GAP (for example Fisher, Jaikumar and Van Wassenhove, Management Science 1986 and Savelsbergh, Operations Research 1997).
Agents are and tasks . Giving task to agent costs and uses units of agent 's resource; agent has units. The problem is
Dropping the resource constraints gives the relaxation (PR). It is solved by choosing, for each task , a cheapest agent with and setting ; its value is . Let be the tasks this solution gives to agent , the overloaded agents, and the excess of agent . The penalty of moving task away from is . For the binary knapsack problem
chooses the cheapest set of tasks to move off agent ; call its optimal value . The knapsack bound is
Dualizing the assignment constraints with multipliers gives the Lagrangean relaxation
Finally and are the smallest and second smallest of , counted with multiplicity.
For every cheapest-agent choice and every choice of optimal knapsack solutions,
the minimum being attained, and consequently for every feasible for (P). This is the paper's "principal result of this Lagrangean analysis" (§2, p. 96). It has no constants to improve; it is an identity between two optimization problems.
In the paper's order of use: (PR) is solved by the cheapest agents (pp. 93–94); every lower bound on (PR) is a lower bound on (P) (p. 95); (PR) separates into one binary knapsack per agent (p. 95); at the variables that are zero in the (PR) solution can be fixed at zero, the substitution turns agent 's part into (PK), , and agent 's part has value (p. 96). Two side results close the section: the solution obtained by moving the tasks the knapsacks select has cost exactly LB, so it is optimal whenever it is feasible (pp. 94–95); and the optimal dual multipliers of the bounded-variable linear program (PR) are exactly the vectors with (pp. 95–96).
The identity says that a bound computed from one sorting pass and a handful of small knapsacks equals a Lagrangean dual bound at a closed-form multiplier. Validity of LB for (P) then follows from weak Lagrangean duality alone, and the multiplier is the upper end of the range of optimal dual multipliers of the linear program (PR), which the paper singles out as a suitable choice of multipliers. The rebuilt solution gives the algorithm a feasible incumbent at no extra cost whenever the knapsack repairs happen to respect all budgets.
The result is proved in the paper, in one sentence. The mission turns that sentence into checked statements: the separation of (PR), the reduction of each agent's subproblem to (PK), the handling of ties among cheapest agents, and the role of nonnegative resources. As far as a search of the platform shows, nothing about the generalized assignment problem or its Lagrangean bounds has been formalized; the definitions here (assignment relaxations, per-agent knapsacks, bounded-variable duals) are reusable for other GAP and facility-location missions.
The Lagrangean relaxation at is a larger problem than the knapsack bound suggests: a feasible may give a task to several agents or to none, and may use any agent, not only the cheapest one. The knapsack bound, by contrast, only looks at the tasks each agent receives in the (PR) solution. The paper bridges the two in one sentence of three observations, and each observation depends on a condition the sentence does not state: the sign of the resource coefficients, the treatment of agents that are not overloaded (for which no knapsack is solved), and ties among cheapest agents, which make some penalties zero and require the statement to hold for every tie-break. An inequality in one direction only (LB is a valid bound) is not the claim; the equality needs a feasible point of (PR) whose value is exactly LB.
Agents are Fin m and tasks Fin n, indexed from 0. Costs, resources, budgets, multipliers and variables are real numbers; a 0-1 variable is a real equal to 0 or 1, so the paper's sums are literal. The cheapest-agent selection is an arbitrary function a : Fin n → Fin m with IsCheapest c a, so every statement holds for every tie-break. and are minima over the other agents, which requires (hm : 1 < m); is proved to be the second smallest cost with multiplicity. Optimal values are never encoded as sInf: is the objective of a given optimal knapsack solution, and "the bound provided by (PR)" is stated as a lower bound over all feasible points that is attained.
Standing hypotheses: (printed on p. 92), (implicit in "the resource required", and necessary: with a negative both (PR) and (P) can fall below LB), and . All costs are finite; the "not permissible" pairs of the paper's numerical example are outside the model.
A formalization that states only every (PR) value, or that restricts the (PR) competitors to the (PR) support or to at most one agent per task, would be a weaker theorem and does not meet the goal. The (PR) dual is written out explicitly with multipliers for the bounds ; "each optimal dual multiplier lies anywhere in the range " is read as "the optimal multipliers are exactly this box".
Needed infrastructure is only finite sums over Fin and Finset.inf'. Proofs of the milestones, and lemmas on separable binary programs that could serve other Lagrangean-relaxation missions, are welcome.
The random walk Metropolis algorithm is one of the most widely used Markov chain Monte Carlo methods for sampling from a density known up to a constant. Its one tuning parameter is the variance of the Gaussian proposal. If the variance is too small, the chain accepts almost every move but barely moves. If it is too large, it proposes long jumps that are almost always rejected. Practitioners need a rule for choosing it, and the rule has to work in high dimension, where both failure modes are severe.
Roberts, Gelman and Gilks (Ann. Appl. Probab. 7(1), 1997) gave the first rigorous answer for product targets. As the dimension grows, one coordinate of the suitably speeded-up chain converges to a Langevin diffusion. The speed of that diffusion is an explicit function of the proposal scale, and maximising it gives the rule "tune the proposal so that about 23% of proposals are accepted". This rule, and the 2.38/√I scaling behind it, is now standard advice in applied Bayesian statistics.
Let be a target density: positive, , integrating to one, with Lipschitz, and satisfying the moment conditions (A1) and (A2) . Here . In dimension the target is the product density on .
Fix a scale and set . The random walk Metropolis chain moves as follows. From it proposes . It sets with probability , and otherwise. The chain starts from , which is stationary for it. The speeded-up first coordinate is for .
Let be the standard normal distribution function, and define the roughness . The speed and the limiting acceptance rate are
The Langevin generator is . It generates the Langevin diffusion .
As ,
where denotes weak convergence in the Skorokhod topology, has density , and is the Langevin diffusion with speed . The limit is asserted to exist. No constants appear in the statement beyond those the model defines.
Theorem 1.1 shows that, run for times as many steps, the chain in dimension looks like a fixed one-dimensional diffusion. The algorithm's cost therefore grows linearly in dimension, and its efficiency is measured by the single number . Corollary 1.2 turns this into the 0.234 acceptance-rate heuristic and the scaling. The same diffusion-limit method has since been applied to the Metropolis-adjusted Langevin algorithm, to Hamiltonian Monte Carlo and to non-product targets.
The theorem is proved on paper; it has no machine-checked proof. A formal development would give the first verified diffusion limit of an MCMC algorithm. It would also yield reusable components: the Metropolis chain on as a measurable random mapping, a martingale-problem characterisation of one-dimensional diffusions, and a Gaussian computation (Proposition 2.4) that recurs throughout the optimal-scaling literature.
The obvious approach, a Taylor expansion of the log acceptance ratio, gives a sum of terms of size . That sum does not concentrate uniformly over the state space, since the coordinates are arbitrary. The expansion is controlled only on the sets , where the empirical averages and are close to . The limit therefore holds only after showing that the chain rarely leaves over a time horizon of steps. A pointwise law of large numbers is not enough for that, because the bound has to survive a union over steps. Passing from generator convergence on a set of high probability to weak convergence of processes requires the Ethier–Kurtz convergence theory: a core for the limit generator, and convergence of processes that are not themselves Markov. None of this theory is in Mathlib.
All declarations live in the namespace Roberts1997.RWM. The following conventions are fixed.
Fin n → ℝ, and the paper's first coordinate is index 0. Its coordinates are the indices i ≠ 0.EthierKurtz_IsContinuousDiffusionLaw.The goal cannot be satisfied trivially. The limit law must exist, and it must be a probability measure whose initial marginal is , so the zero measure is excluded. The coupled copies must carry exactly the laws of the paths , not an arbitrary process with the same one-time marginals.
The statements carry the paper's hypotheses, with one exception. The printed proof of Lemma 2.6 bounds , which Theorem 1.1 does not assume, and under alone the uniform convergence over claimed by Lemma 2.6 fails (narrow spikes of far out let a positive fraction of the coordinates shift the log acceptance ratio by a constant while and stay close to ). Lemma 2.6 is therefore stated with the proof's own assumption, with bounded, named as an addition. Theorem 1.1 and the other results keep the paper's hypotheses.
A complete development needs several pieces not yet available: path spaces and the Skorokhod topology (or the coupling reading), the martingale problem and its well-posedness for Lipschitz drift, and the Ethier–Kurtz theorem on convergence of generators on sets of high probability. Proofs of the Gaussian milestones (Propositions 2.2 and 2.4, Lemma 2.5) and of Corollary 1.2 (ii) are independent of this infrastructure and are welcome contributions.
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.
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.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 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.
Machine scheduling asks how to assign jobs to machines over time so that a criterion such as the makespan , the time at which the last job completes, is as small as possible. In practice jobs also compete for scarce resources beyond the machines themselves: tools, operators, memory, power. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the standard three-field classification of Graham, Lawler, Lenstra and Rinnooy Kan (1979) by a resource field . They then settled the complexity of every problem with parallel identical or uniform machines, unit-time jobs, precedence constraints and the criterion. Their Fig. 2 separates the maximal polynomially solvable problems from the minimal NP-hard ones, and it has been the reference map for resource-constrained scheduling since.
Brief timeline of the problems involved:
There are jobs and machines . Every job has processing time on every machine, each machine handles at most one job at a time, and jobs are not preempted. There are resources; resource has a positive integer size , the amount available at any time, and job has a nonnegative integer requirement , the amount it holds throughout its execution. A directed acyclic graph on the jobs gives the precedence constraints: if has a path from to (), then must complete before starts. The precedence is chain-like when every vertex of has indegree and outdegree at most one.
A schedule gives each job a machine and a real start time ; the job occupies and completes at . It is feasible if jobs on one machine do not overlap, precedence is respected, and at every time the jobs running at require at most of each resource . The makespan is .
The problem restricts this to , one resource () of size (), every requirement at most (), and chain-like precedence. The problem has , one resource of arbitrary size and requirements, and no precedence.
3-PARTITION: given , a positive integer and positive integers with and , can be split into disjoint 3-element sets with ?
A problem is NP-hard in the strong sense if it remains NP-hard when every number of the instance is written in unary.
The hypothesis is Garey and Johnson's theorem on 3-PARTITION, which the paper cites and does not prove. The conclusion concerns the decision version: given an instance and , is there a feasible schedule with ?
Theorem 7 is the sharpest hardness result of the paper's classification. Without resources, two-machine unit-time scheduling with arbitrary precedence is polynomial (Coffman and Graham, Acta Inform. 1972); without precedence, it is polynomial under arbitrary resources (Theorem 1 of the paper). The theorem shows that combining the weakest nontrivial versions of both constraints, chains and one unit resource, already crosses the borderline. The paper's §4.1 extends the same reduction to the and criteria.
On the formal side, the mission provides a machine-checked model of resource-constrained scheduling with real start times, a definition of NP-hardness in the strong sense on top of the platform's Turing-machine formalization of and , and 3-PARTITION as a reusable source problem. As far as the platform's corpus shows, none of Theorems 4 and 7, 3-PARTITION, or strong NP-hardness has been formalized before. Both theorems are proved in the literature; what remains is to formalize the reductions and their polynomial running time.
The combinatorial heart is the "only if" direction: a schedule of length must be shown to be rigid. Start times are arbitrary reals, so the first obstacle is to show that both machines are busy throughout , that the chain forces unit spacing, and that the primed jobs of the chains can only run in the intervals the chain leaves free of the resource. Only after this is established can the index sets be read off. Arguing on integer time slots from the start is not enough: the model allows fractional start times, and ruling them out is part of the proof.
The second obstacle is the complexity layer. NP-hardness is stated with respect to polynomial-time many-one reductions computed by one-tape Turing machines. The reduction from 3-PARTITION therefore has to be implemented and its running time bounded on unary codes. The constructed instance has jobs, which is polynomial in the unary length of the 3-PARTITION instance; this is exactly why the reduction proves hardness in the strong sense.
Fin n and machines Fin m, 0-based. Only identical machines with unit processing times are modelled. Start times are real, execution intervals are half-open, and the resource constraint is imposed at every real time. Precedence is the transitive closure of the arc list of . for an empty instance.Welcome contributions: proofs of the four milestones; a formalized polynomial-time implementation of the reduction on unary codes; general lemmas about composing polynomial-time reductions on the one-tape machine model.
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.
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.
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.
Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It models cutting stock, memory allocation, file placement and the loading of trucks, and it is NP-hard, so in practice lists are packed by simple rules that look at one item at a time. The two most widely used rules are First-Fit and Best-Fit, and the question that Johnson, Demers, Ullman, Garey and Graham answered in 1974 is how far from optimal they can be in the worst case.
Their headline answer is that both rules use at most about times the optimal number of bins, and that is asymptotically attained. The lists that force this ratio use items larger than . When all items are known to be small, which is typical of memory and storage applications, the guarantee is much better, and this mission is about that refinement: the paper's Theorem 2.3 and its corollary, which determine the asymptotic worst-case ratio of First-Fit and Best-Fit exactly as a function of the largest allowed item size .
Timeline. Ullman (1971) introduced the worst-case analysis of First-Fit with a bound. Garey, Graham and Ullman (1972) and Johnson's thesis (MIT, 1973) extended it to Best-Fit and to the decreasing variants. The 1974 SIAM paper collects these results; Theorem 2.3 there is the parametric bound for items of size at most . The additive constants in the unrestricted bound were sharpened over the following four decades, culminating in Dósa and Sgall's proof (2013) that .
A list is a finite sequence of real numbers in . Its optimum is the least number of bins into which the elements of can be placed so that no bin contains numbers whose sum exceeds . The level of a bin is the sum of the numbers in it. For a real , write when every element of is at most .
First-Fit () considers bins , all initially empty, and places in that order: goes into the bin of least index whose level satisfies . Best-Fit () is the same except that, among the bins with , it chooses one of largest level (least index among ties). and denote the numbers of nonempty bins at the end.
The restricted worst-case ratios are
Throughout, and , an integer with and .
The goal is stated as a limit, which is the stable form of the result: it is unaffected by any improvement of the additive constants below.
For each there is a list with and ; likewise for .
If no element of exceeds , then in the First-Fit packing every bin except possibly the last contains at least elements, and all but at most two bins have level at least .
For every list ,
The theorem gives an exact, parametric description of how the worst case of the two greedy rules improves as items shrink: the asymptotic ratio is when items are at most , when at most , and tends to as the maximum item size tends to . Combined with the bound for unrestricted lists, it shows that the bad behaviour of First-Fit is caused entirely by items larger than . Such parametric bounds are the standard way bin-packing heuristics are compared in the literature on online and semi-online packing, and the construction in part (i) is a reusable template for lower-bound lists.
The paper proves the First-Fit upper bound and the lower bound (the verification of the lower-bound construction is left to the reader). The Best-Fit upper bound is stated but not proved: the paper says only that "a similar, but slightly more complicated, argument can be used". A formal proof of the goal therefore requires supplying that argument. None of these results is known to have a machine-checked proof; Mathlib contains no bin-packing development.
For First-Fit the upper bound is a counting argument, but it rests on a property of the run, not of the final packing: an item that went into a later bin did not fit into an earlier bin at the moment it was placed. Turning that into a statement about the final levels requires an invariant maintained through the whole sequence of placements.
The Best-Fit upper bound is harder because that property fails: Best-Fit may put a small item into a fuller, later bin while an earlier, lighter bin still has room, so a light early bin and a light later bin can coexist longer than under First-Fit. The paper gives no argument for this case.
The lower bound requires computing the exact behaviour of both algorithms on a specific interleaved list with item sizes perturbed by powers of , and computing exactly for that list, which needs a matching lower bound on the optimum.
A list is L : List ℝ with the hypothesis IsList L (every element in ); is the additional hypothesis ∀ a ∈ L, a ≤ α. is optBins L, a sInf in ℕ over numbers of bins admitting a feasible assignment; the hypothesis IsList makes the set nonempty. The runs ffPack L and bfPack L are folds over the list that keep the nonempty bins in the order they were opened, each with its contents; an item that fits nowhere opens a new bin at the end, which is the paper's "least " over infinitely many empty bins. Comparisons are exact (classical decidability on ℝ), and , are the lengths of the final bin lists. is Nat.floor α⁻¹, cast before any division.
The ratios , are suprema taken in ℝ≥0∞: an unbounded family would give , never a default value, and at the only admissible list is empty and the value is . The goal is a Tendsto … atTop (𝓝 (1 + (⌊α⁻¹⌋₊)⁻¹)) statement in ℝ≥0∞. A real-valued sSup would have returned on an unbounded family and made a false bound look provable; that encoding is ruled out. The upper bounds keep the additive constant and the lower bound the subtractive exactly as printed.
The two proof steps are stated under the proof's own hypothesis "no element exceeding ", which is weaker than .
A complete development needs invariants of the First-Fit and Best-Fit folds, a lower bound , and exact evaluation of both runs on the construction of part (i). Lemmas about the fold encoding of First-Fit and Best-Fit and about are reusable in the companion missions on the , and bounds of the same paper. Contributions on the Best-Fit upper bound are especially welcome, since the source gives no proof.