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?
In best arm identification with fixed confidence, a learner samples unknown distributions ("arms") one at a time, and must eventually stop and name the arm with the largest mean, with an error probability at most a prescribed risk , while using as few samples as possible. The problem goes back to the sequential design of experiments (Chernoff, 1959; Even-Dar, Mannor and Mansour, 2006) and underlies adaptive A/B testing, clinical trial design and hyperparameter selection.
Any fixed-confidence strategy consists of three parts: a sampling rule, a stopping rule and a decision rule. Garivier and Kaufmann (arXiv:1602.04589, COLT 2016) proposed the Track-and-Stop strategy, the first shown to match the asymptotic lower bound on the expected sample complexity. Its stopping rule is a generalized likelihood ratio (GLR) test, Chernoff's stopping rule. Its correctness, the guarantee that the recommended arm is wrong with probability at most , must hold whatever the sampling rule, which is what allows the sampling rule to be tuned freely for efficiency. This mission formalizes that guarantee for Bernoulli arms, Theorem 10 of the paper, with its explicit threshold .
The arms are . A Bernoulli bandit model is a mean vector : pulling arm returns reward with probability and otherwise, independently of the past. The class contains the models with a unique optimal arm , i.e. for all .
At round the learner chooses an arm as a (possibly randomized) function of the past observations and observes a reward . Write for the number of pulls of arm among the first rounds, for the number of those pulls that returned , and for the empirical mean. The likelihood of arm 's observations under mean is .
The GLR statistic for "arm is at least as good as arm " is
Chernoff's stopping rule with exploration rate is
and the decision rule recommends .
The Krichevsky–Trofimov (KT) distribution on binary sequences is , the Bernoulli likelihood mixed over the Beta prior.
For every , every sampling strategy, and the threshold ,
is a probability law on , and for ,
With , for all arms with ,
Theorem 10 decouples correctness from efficiency. Because the guarantee holds for every sampling strategy, any sampling rule, including the C-Tracking and D-Tracking rules of Track-and-Stop, the uniform rule, or a heuristic, inherits -correctness as soon as it is paired with Chernoff's stopping rule at this threshold. The asymptotic optimality result of the paper (Theorem 14) then only has to control the sample complexity. The threshold is explicit, with no unspecified constant, in contrast to the deviational threshold of Proposition 12.
The result is proved in the paper, in Appendix C.1, and rests on Lemma 11, which the paper quotes from the universal coding literature without proof. As far as the platform's catalog shows, none of these results is formalized. The platform holds a machine-checkable statement of the analogous result for Gaussian arms with the Lattimore–Szepesvári threshold (BanditAlgorithm.chernoff_stopping_rule_sound, Lemma 33.7 of Bandit Algorithms), which is a different model and a different threshold. Formalizing Theorem 10 adds a proof of Lemma 11 (the KT regret bound, reusable in information theory and universal prediction), the Bernoulli GLR statistic, and a change of measure from the true bandit law to a Bayesian mixture law on the trajectory space.
The obvious approach bounds, for each fixed , the probability that exceeds by a concentration inequality and sums over . This fails: the sampling strategy is arbitrary and adaptive, so and are random and depend on the past rewards, and a fixed-sample-size deviation bound does not apply; a union bound over the possible values of the counts loses more than the threshold allows. The maximum likelihood in the numerator of is also not a probability density, so the likelihood ratio cannot directly be read as a change of measure. The argument must control the whole trajectory law under an arbitrary randomized policy, and must handle empty samples (an arm never pulled contributes likelihood ) and the boundary means and .
The formalization is in Lean 4 with Mathlib and reuses the platform's canonical bandit model: StochasticBandit, BanditPolicy (a Markov kernel per round from the observed history to the next arm, so randomized strategies are included), banditTrajMeasure (the law of the infinite trajectory, where coordinate is round ) and IsSoundBAI from BanditTrajectory; bernoulliBandit from bernoulliRelativeEntropy; and only the pull counts trajPullCount and empirical means trajEmpiricalMean from TrackAndStop. The Gaussian GLR and threshold of TrackAndStop are not used.
Conventions committed to:
Fin K. Bernoulli means range over , degenerate laws included; the paper's exponential-family mean space is , so the statement implies the paper's.Disclosed deviations from the page: Lemma 11's ratio bound is stated for , since at the printed bound reads ; the use of the lemma in Appendix C.1 is unaffected. Appendix C.1 calls the result "Proposition 10" (a slip for Theorem 10) and prints the KT density as (a slip for of Lemma 11, which is the normalized one); the formalization follows Lemma 11.
A trivializing formalization is ruled out: stating the result for Gaussian arms or with the Lattimore–Szepesvári threshold is the platform's existing Lemma 33.7 and is not Theorem 10, and a free decision rule without the argmax hypothesis would make the claim false rather than faithful.
Contributions welcome: a proof of Lemma 11; a change-of-measure lemma for banditTrajMeasure under a mixture of environments; and the union-bound reduction from the goal to the pairwise claim.
In a combinatorial auction a seller offers several indivisible items at once, and bidders value bundles of items rather than items one at a time. Allocating the items to maximize total value is the central optimization problem of the area, and it arises in spectrum licensing, procurement and transport contracting (Cramton, Shoham and Steinberg, Combinatorial Auctions, MIT Press, 2006). Two obstacles meet. Computationally, a valuation has numbers, so an algorithm can only query it, and even then optimization is hard. Strategically, the valuations are private: a bidder reports whatever maximizes its own utility, so an algorithm that is a good approximation on true inputs may be useless on reported ones.
The classical answer to the strategic obstacle is the VCG payment scheme, which makes truthful reporting a dominant strategy but requires the exact optimum. Nisan and Ronen (2007) showed that an approximation algorithm becomes truthful under VCG payments essentially only when it is maximal in range: it fixes a restricted set of allocations in advance and optimizes exactly over that set. Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010, §5) give such an algorithm for complement-free (subadditive) bidders that uses only value queries and loses a factor of order . For general valuations in the value-query model the paper cites a lower bound of order (Dobzinski and Schapira, working paper 2005; Blumrosen and Nisan, Hebrew University Discussion Paper 381, 2005; see the paper's references [7] and [2]), and the same paper (Theorem 6.1) shows that even XOS bidders cannot be approximated within with polynomially many value queries.
A set of items is sold to bidders. Bidder has a valuation that assigns a real number to every bundle . Throughout, valuations are normalized, , and monotone, . A valuation is complement free (CF) if for all bundles . An allocation gives the bidders pairwise disjoint bundles (items may stay unallocated), and its social welfare is .
The mechanism receives reports and runs the following algorithm :
Its range is the set of allocations that give all of to one bidder, together with the allocations in which every bidder receives at most one item. Under VCG payments bidder receives , so its utility is . The mechanism is incentive compatible on a class of valuations if no bidder can raise its utility by misreporting within that class, whatever the others report.
For every choice of the maximum-weight matching and of the top bidder as functions of the reports, for every profile of normalized, monotone, CF valuations and every allocation ,
and the mechanism is incentive compatible on the CF valuations.
AGT.vcg_incentive_compatible).The theorem shows that, for subadditive bidders, the barrier known for general valuations can be matched by a truthful mechanism that asks each bidder only value queries. It is one of the early examples of maximal-in-range mechanism design, a template later used for many truthful approximation mechanisms in combinatorial auctions, and it sits against Theorem 6.1 of the same paper, which shows that for XOS bidders no value-query algorithm with polynomially many queries does better than .
The result is proved in the paper. What this mission adds is a machine-checked proof: a formal model of VCG-based mechanisms over a restricted range, a proof that the §5.2 algorithm is maximal in range for every tie-breaking of its two optimization steps, and the explicit constant in the bound. To our knowledge neither half of Theorem 5.1 is formalized elsewhere; the general VCG theorem exists on the platform in the setting of arbitrary outcome sets.
The approximation argument partitions the bidders of a reference allocation by whether their bundles have at least items, and the two cases need different facts: disjointness bounds the number of large bundles by , and subadditivity bounds each small bundle by its size times its best item. A naive transcription breaks at degenerate inputs: the page divides by and writes strict inequalities, both of which fail when a bundle is empty or all values are zero, so the formal statement must be organized around non-strict bounds.
Incentive compatibility has a different obstacle. It holds only if the allocation rule depends on the reports alone and optimizes exactly over its range, including at ties between the grand bundle and the matching. The matching and the top bidder are not unique, so the proof must work for an arbitrary but fixed tie-breaking, and the welfare of the matching allocation must be identified with the matching weight, which uses normalization of every bidder who receives nothing.
Bidders are Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. Normalization and monotonicity (the paper's standing assumptions, p. 1) and complement freedom are hypotheses; IsCFValuation bundles all three. An allocation is a family of pairwise disjoint bundles; unallocated items are allowed. A matching is a partial map Fin m → Option (Fin n) with no bidder matched twice.
Conventions the formalization commits to:
Real.sqrt m.mat, top of the report profile, each with a specification hypothesis; the goal is stated for every such pair. The algorithm reads only the reports; the tie between and goes to the matching, as on the page.AGT.MechIncentiveCompatible on outcomes .A trivializing formalization is ruled out: the ratio is the explicit rather than an existential constant, incentive compatibility is over the full CF domain (not additive reports only) for a rule that cannot see true valuations, and the rules mat, top are satisfiable (a maximum over the finitely many matchings exists; a top bidder exists when ).
Useful infrastructure: finite maximum-weight matchings on complete bipartite graphs, subadditivity bounds over Finset sums, and a reusable lemma that maximal-in-range rules with VCG payments are truthful. Contributions of any milestone are welcome; milestones 2 and 4 are self-contained.
A Markov decision process (MDP) is solved by dynamic programming only when its transition probabilities are known. In practice they are estimated from data, and the optimal policy of the estimated model can perform badly on the true one. Nilim and El Ghaoui (Oper. Res. 53(5), 2005) showed that, when the uncertainty on the transition matrices has a product ("rectangular") structure, the robust problem, in which the controller minimises the worst expected cost over all admissible transition matrices, keeps the structure of dynamic programming. The robust Bellman operator replaces the expectation of the next-stage value by a support function of the uncertainty set. That operator is the basis of later work on robust MDPs and robust reinforcement learning.
Timeline:
The state space is and the action set is finite and nonempty. Each state–action pair has a cost , and costs are discounted by a factor : the cost at stage is .
Write for the probability simplex. For each action and state a nonempty set is given. It is the set of distributions of the next state that nature may use from state under action . No convexity or closedness is assumed. Uncertainty is rectangular: the admissible transition matrices for action form the product , so every row is chosen independently.
A stationary control policy applies one decision rule at every stage; is the set of them. A stationary policy of nature fixes one matrix for each action and uses it forever. Nature chooses after the controller.
From an initial state , the state distribution evolves as , . The discounted cost is
The support function of a set is . The robust Bellman operator and, for a stationary policy , the robust evaluation operator act on by
The two values of the game are
There is a unique with , i.e.
value iteration converges to from every starting vector (20), and
In addition, every policy that picks a minimising action in (19) is optimal (21), every nature policy whose rows attain is optimal for nature (22), and for each stationary the worst-case cost is , where is the unique fixed point of (23).
The theorem makes the robust discounted problem as tractable as the nominal one. The optimal robust policy is stationary, deterministic and computed by value iteration. Each iteration evaluates one support function per state–action pair, and the paper computes these efficiently for likelihood and entropy uncertainty sets (§§5–6). Perfect duality means that the order of play does not change the value: announcing the policy to an adversarial nature costs nothing. The sequel in this series (Theorem 4) uses Theorem 3 to show that restricting to stationary policies loses nothing.
The result is proved in the paper and, independently, by Iyengar (2005). No machine-checked proof of it is known to exist. Mathlib provides the Banach fixed-point theorem, but it has no MDP library, no discounted cost along a Markov chain and no robust Bellman operator. The mission produces that layer.
The fixed-point half is a direct application of the Banach fixed-point theorem once the -contraction is established. The substance is the link between the fixed point and the probabilistic cost, and the duality.
Fin n → ℝ, with the componentwise order and Mathlib's sup metric, which is .RobustMDP.Discounted.Model) carries the costs, the discount (the range printed in Theorem 3; §4 prints ) and the row sets. The row sets are assumed nonempty and contained in and nothing else. Nonemptiness is implicit in the paper.Fin n → A. is the subtype of A → Fin n → Fin n → ℝ whose rows lie in the row sets, which encodes rectangularity.tsum of the discounted stage costs along the forward state distribution. The terms are nonnegative and at most , so the series is summable and the tsum is the limit of the -stage costs, the paper's definition.sSup. It is the genuine supremum because every set it is applied to is nonempty and inside .IsLUB, or ⨆ inside , whose inner sets are shown bounded by conclusion (23). Minima over the finite and over are ⨅ and Finset.inf'. The argmax rows of (22) appear only as a hypothesis on a given nature policy that attains them.A convex polytope has two standard descriptions: as the convex hull of finitely many points, and as the intersection of finitely many half-spaces. Linear programming uses both at once. The feasible region of a linear program is given by inequalities, while the simplex method and the theory of basic solutions work with its vertices. That the two descriptions define the same class of sets is the Minkowski–Weyl theorem.
Hermann Weyl's 1935 paper Elementare Theorie der konvexen Polyeder (Comment. Math. Helv., 1935, pp. 290–306) gave an elementary, self-contained proof of this equivalence. An English translation appeared in Contributions to the Theory of Games I (Annals of Mathematics Studies 24, 1950), where it served as the polyhedral foundation for the minimax theorem and linear inequality theory in early game theory and linear programming.
Timeline:
Write for vectors of . A point system is a finite set . It is non-degenerate if no has for all . A vector is a support of if for all . A support is an extreme support if equality holds at linearly independent points of . A point is representable by if with all .
Read as inequalities , , the same defines the cone of solutions. An extreme solution is a nonzero at which linearly independent inequalities of are tight. The dual system consists of the inequalities , one for each extreme solution , and is the cone it defines.
For polytopes, Weyl passes to the hyperplane , identified with , . A convex polyhedron is for a finite whose affine span is all of . Given a finite index set , normals and constants , the inequalities cut out a region
In Weyl's notation, row is , with and .
Assume no row is identically zero ( or ). Then
In words, the normals must positively span and must contain an inner point. The goal is the equivalence, not either half alone.
LinearOptimization.farkas_cone_corollary.The result. §4 II gives both directions of the Minkowski–Weyl theorem for full-dimensional polytopes, together with a test on the data : positive spanning of the normals is equivalent to boundedness, and a strictly feasible point is equivalent to full dimension. Several parts of LP theory start from this equivalence: finiteness of the vertex set of a bounded feasible region, the existence of an optimal vertex, and the passage between the primal (inequality) and dual (generator) descriptions used in polyhedral combinatorics.
Formalizing it. The theorem has been proved since 1935; the work here is formalization. Mathlib has convex hulls, extreme points, and pointed cones with their duals, but no Minkowski–Weyl theorem for polytopes or for cones. On this platform, Farkas-type lemmas (LinearOptimization.farkas_cone_corollary) and the statement that a nonempty bounded polyhedron is the hull of its extreme points (Bertsimas–Tsitsiklis Thm 2.9) are published. Neither gives the "only if" direction, the positive-spanning criterion, or full-dimensionality.
The "only if" direction and the reduction from a strictly feasible bounded region to cones are routine. The hard step is the finiteness statement: why a finite set of inequalities has only finitely many generators, and why these generate the whole region. Mathlib's compactness results give "a compact convex set is the closed hull of its extreme points" (Krein–Milman). That result does not show that the extreme points are finite in number, nor that there are finitely many of them in a form that can be computed from the inequalities. Weyl's route avoids topology. It goes through the Hauptsatz, proved by induction on dimension, and the duality between and . Each step of that duality needs non-degeneracy, and keeping that hypothesis alive through the dualization (Satz 9) is where care is needed.
Fin n → ℝ, with dot product ⬝ᵥ. Point systems are Finsets; the zero vector is allowed in them. "Representable" is an explicit nonnegative sum over the Finset.span = ⊤.Fin m → ℝ, a point standing for Weyl's . Linear independence of homogenized points becomes affine independence of points, and non-degeneracy becomes affineSpan ℝ S = ⊤.Fin n → ℝ, extreme rays of pointed polyhedral cones, and the homogenization dictionary between cones in and polytopes in . Proofs of any milestone, and alternative routes to the goal (e.g. via Fourier–Motzkin elimination), are welcome.The augmented Lagrangian method (method of multipliers) of Hestenes, Powell and Rockafellar solves a constrained nonlinear program by repeatedly minimizing an unconstrained merit function in the primal variables and then updating the multipliers. For inequality constraints, the augmented Lagrangian in the form the paper takes from Rockafellar (Rockafellar 1981) is continuously differentiable but not twice differentiable, even when all problem data are smooth: its Hessian jumps across the surfaces where a constraint switches between the "active" and "inactive" formula. Newton's method for the inner minimization therefore has no classical Hessian to work with on those surfaces.
Qi and Sun (Math. Programming 58, 1993) extended Newton's method to equations with locally Lipschitz, replacing the Jacobian by an element of Clarke's generalized Jacobian, and proved local superlinear convergence when is semismooth. Section 4 of the paper, an example suggested by Rockafellar, shows that the gradient of the augmented Lagrangian of a program is semismooth, so the nonsmooth Newton method applies to the stationarity equation . This mission formalizes that result, Theorem 4.1.
Let be of class and consider
Fix . For a constraint value and a multiplier put
(the two cases agree when ). The augmented Lagrangian is the function of
For a locally Lipschitz map between finite-dimensional spaces, let be the set where is differentiable. Clarke's generalized Jacobian is . is semismooth at if it is locally Lipschitz near and, for every direction , the limit of over , , , exists.
For a single constraint function the proof works with on , and with the surface on which the two formulas for meet.
For and :
All three clauses are the theorem; the last two together cover every point.
The result places the inner problem of the augmented Lagrangian method inside the scope of the paper's convergence theory: with , the generalized-Jacobian Newton iteration converges locally superlinearly at a root where every element of is nonsingular. Its practical content is that second-order methods can be run on even though is only , with the elements of playing the role of Hessians. The same pattern (a merit function with semismooth gradient) recurs in extended linear-quadratic programming and in semismooth Newton methods for complementarity problems.
The theorem is proved in the paper by direct computation. As far as a search of the platform showed, none of the objects involved (Clarke's generalized Jacobian, semismoothness, Rockafellar's augmented Lagrangian) has a published formalization there, and Mathlib has none of them. The mission produces a machine-checked version of the computation and, as a by-product, reusable statements about functions obtained by gluing two pieces along a hypersurface.
Clauses 1 and 3 are calculus with a case split: one has to check that the two formulas for and for its gradient match on the surface. Clause 2 is where the argument is not routine. On the surface, is not differentiable, and the generalized Jacobian there contains convex combinations of the two one-sided Hessians of (4.2). Semismoothness asks that have a single limit over all such , for all approaches , , including approaches that cross the surface infinitely often. The two one-sided Hessians are different matrices, so no single derivative describes near the surface, and the existence of the limit must be shown for approaches that alternate between the two sides and for the convex combinations that contains on the surface itself. General theorems that piecewise-smooth maps are semismooth appear in later literature but are not available in Mathlib, so they cannot be invoked as a shortcut. A second obstacle is infrastructure: Mathlib has no generalized Jacobian, so every fact about (which limits of derivatives occur near the surface) must be derived from the definition.
EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); is a function on their product, and on EuclideanSpace ℝ (Fin n) × ℝ.i : Fin m with paper index i.val + 1; equality constraints are i.val < p, inequality constraints p ≤ i.val. The paper's implicit is not assumed (for there are no inequality constraints).ContDiff ℝ 2 on all of ; "smooth" is the paper's continuously differentiable, ContDiffAt ℝ 1 of the gradient at the point.fderiv, limits are along sequences, and no closure is taken in the convex hull. Semismoothness is the explicit – form of the paper's limit, uniform over .A formalization that states only , or only the semismoothness of one term , is not Theorem 4.1; the goal contains all three clauses for the full . The combination step from the terms to uses that sums of semismooth maps and maps with locally Lipschitz derivative are semismooth; the paper cites this without proof, and a solver will need to prove it.
Contributions welcome: the lemmas above; general facts about clarkeJac (it contains fderiv at points of strict differentiability; it is a singleton for maps; behaviour under sums and linear maps); and the semismoothness of sums.
A decision maker who chooses a portfolio of risky assets with random return vector receives the scalar return and evaluates it by an expected utility . In practice the law of is not known; what can be estimated with some confidence are its mean and covariance . The robust mean-covariance objective replaces the unknown law by the worst law consistent with these two moments:
Ioana Popescu (Operations Research 55(1), 2007) showed that depends on only through and , and that for large classes of utilities it has a closed form or reduces to a one-dimensional search. This turns a robust stochastic program into a parametric mean-variance program, which is the practical point of the paper. This mission formalizes the closed form for concave utilities with a monotone second derivative (Proposition 7), a class that contains the exponential utility and all concave quadratics. The reduction to is the subject of the companion mission Robust Mean-Covariance Solutions for Stochastic Optimization I; the two-point case is mission II.
The underlying univariate question is a moment problem in the tradition of Chebyshev-type bounds: the extremal value of over all laws with prescribed mean and variance. Scarf (1958) solved an instance for a piecewise-linear inventory cost, and Birge and Dulá (1991) treated two-point extremal laws on bounded domains.
Fix and . The mean-variance class is the set of Borel probability measures on with , and (Lean: MeanVarClass m (s ^ 2)). For a utility the robust objective is
with read, as in the paper, "in the wide sense of ", so the value is allowed. The paper's is .
For the two-point law puts mass on and mass on ; these are exactly the two-point laws of . Its expected utility is the two-point objective (8),
A supporting quadratic of is with on ; the set of their coefficients is . Since every has , each element of gives a lower bound on (Proposition 3). The function has the one-point support property with respect to (Definition 3, OnePointSupportWrt u m s) if some supporting quadratic touches at and as or as ; it has one-point support (OnePointSupport u) if this holds for every and every .
Let be concave and twice differentiable with monotone .
(a) If is convex, then
(b) If is concave, the same holds with .
In each part the limit of exists in . When is finite the goal asserts that is integrable under every law of every class, that is the greatest lower bound of the expected utilities, and that has one-point support. When and it asserts .
An additional item states Proposition 8: a monotone convex has one-point support and .
Proposition 7 turns the worst-case expected utility into a mean-variance criterion with an explicit risk weight: a prudent investor ( convex) is penalized by per unit of variance, an imprudent one by the limit at . With Proposition 1, the robust portfolio problem becomes , a concave mean-variance program. For exponential utility the weight is (Example 3 of the paper), so the robust investor must eliminate variance entirely; this is a qualitative statement about robustness that follows only from the case of the theorem.
The result is published with a proof in the appendix of the paper. It has, to the best of our search, no machine-checked version, and the platform currently holds no statement of Propositions 3, 7 or 8 or Definition 3. A formal proof would also check two points where the printed argument is incomplete: the proof's step "" fails for affine , where the theorem nevertheless holds, and the claim that "has one-point support" fails when (see the scope section). Related platform work on worst-case expectations over ambiguity sets is the mission Wasserstein Distributionally Robust Optimization II, which uses a different ambiguity set.
The infimum ranges over all laws with two prescribed moments, an infinite-dimensional set with no compactness, and in the relevant cases it is not attained. The natural first idea, restricting to two-point laws and minimizing over , gives only an upper bound (display (7)), and here the minimizing runs off to the boundary: the extremal law puts vanishing mass on a point escaping to . Identifying the limiting value requires controlling as , a second-order asymptotic statement about at . The matching lower bound requires a supporting quadratic whose curvature is exactly ; showing that it lies below everywhere, not only near , is a global statement that uses the convexity of on the whole line. The finite-limit and infinite-limit cases also behave differently: in the second, no supporting quadratic exists at all.
Laws are Measure ℝ with IsProbabilityMeasure, finite second moment is MemLp id 2, and the class is parameterized by mean and variance with . The statements are univariate: of the paper is the univariate objective at by Proposition 1 of the paper (mission I). Derivatives are deriv u and deriv (deriv u); "twice differentiable" is differentiability of and of . Limits of are explicit hypotheses (Tendsto … atBot (𝓝 L) or Tendsto … atBot atBot), never limUnder. Limits in are one-sided inside . Expectations under two-point laws are written by the explicit formula (8).
"Min" is never a real ⨅, which Lean evaluates to on sets unbounded below. The finite case uses IsGLB together with integrability of under every law of the class; the infinite case asserts that integrable laws with arbitrarily small expected utility exist; Proposition 3 is stated as "every value every value". Proposition 3 assumes integrable under the law; Proposition 8 takes the infimum over laws under which is integrable, which for convex loses nothing.
One correction to the printed statement: Proposition 7 opens with "then has one-point support", which is false when , since no quadratic lies below on . The formalization asserts one-point support only in the finite-limit case and the value in the other. A formalization that took as a real infimum, dropped the integrability conjunct, or asserted one-point support unconditionally would be either trivially satisfiable or false; none of these is used.
A complete development needs: moments of two-point laws, a second-order l'Hôpital or Taylor argument at , the trapezoid inequality for convex functions, and Jensen-type integration of quadratic lower bounds. The mean-variance class, the two-point objective and the supporting-quadratic lemmas are reusable for mission II and for other moment-problem bounds. Proofs of any milestone, and of part (b), are welcome.
Many polytopes of combinatorial optimization have exponentially many facets, yet linear optimization over them is tractable because they are projections of simpler convex sets: affine slices of a nonnegative orthant (linear programming) or of the cone of positive semidefinite matrices (semidefinite programming). The size of such a representation, the number of variables of the extended formulation, is the natural measure of how compactly a polytope can be optimized over. Yannakakis (Expressing combinatorial optimization problems by linear programs, JCSS 1991) characterized polyhedral representations through nonnegative factorizations of the slack matrix. Gouveia, Parrilo and Thomas (arXiv:1111.3164, Mathematics of Operations Research 2013) extended the characterization to lifts into arbitrary closed convex cones, in particular to cones of positive semidefinite matrices.
The stable set polytope of a graph is the standard test case. For a perfect graph on vertices it is a linear image of an affine slice of the cone of positive semidefinite matrices (Lovász's theta body construction, stated in the paper as Theorem 5.1 with a citation to Lovász & Schrijver, SIAM J. Optim. 1991); this is the reason the maximum weight stable set problem is solvable in polynomial time on perfect graphs. The question addressed by this mission is whether a smaller matrix size could suffice. Theorem 5.2 of Gouveia–Parrilo–Thomas answers it: for every graph on vertices, matrices of size do not suffice.
Let be a graph with vertex set . A set is stable if no edge joins two of its elements, and its incidence vector has exactly when . The stable set polytope is
Let be the cone of real symmetric positive semidefinite matrices, with the trace inner product , under which it is self-dual. For a closed convex cone , a set has a -lift if for an affine subspace and a linear map ; the lift is proper if meets the interior of .
For a polytope with vertices and facet inequalities , the slack matrix is the nonnegative matrix . A -factorization of a nonnegative matrix assigns to each row and to each column with . In Lean the objects are stab, HasPSDLift, HasConeLift, HasProperConeLift, IsSlackMatrix, HasConeFactorization and HasPSDFactorization in the namespace ConeLifts.StableSet.
For every and every graph on vertices,
The statement excludes all lifts, proper or not, and holds for every graph, perfect or not.
has no -factorization.
Theorem 5.2 shows that the semidefinite representation of for perfect graphs has the smallest possible matrix size: cannot be lowered to . As Remark 5.3 of the paper notes, the same argument shows that no polytope in with a vertex at which it locally looks like the nonnegative orthant has an -lift. It is also an instance of the factorization method: a statement about all possible semidefinite representations is reduced to a finite obstruction on a small submatrix of the slack matrix.
The theorem is proved in the paper. To the best of our knowledge no machine-checked proof of it, of the factorization theorem for cone lifts, or of any positive semidefinite lower bound for a polytope exists in Mathlib or on this platform. A formalization produces reusable statements about positive semidefinite factorizations, slack matrices and lifts, and a verified instance of the general lower-bound technique.
The step from lifts to factorizations is where the direct argument fails. Theorem 3.3 applies only to proper lifts and only to polytopes with the origin in their interior, while the goal concerns all lifts of a polytope that has the origin as a vertex. Applying Theorem 3.3 to and an arbitrary lift therefore does not match its hypotheses, and the printed proof does not spell out how the two gaps are closed (see Formalization scope). Theorem 3.3 itself is a consequence of the general factorization theorem of the paper (Theorem 2.4), whose proof rests on conic duality. The core lemma about is a statement about every family of positive semidefinite matrices, so it cannot be settled by any finite search.
is EuclideanSpace ℝ (Fin n); vertex of the paper is i : Fin n; graphs are SimpleGraph (Fin n) and stability is SimpleGraph.IsIndepSet. Vertices of a polytope are Set.extremePoints ℝ. is the set of real matrices satisfying Matrix.PosSemidef (which includes symmetry), and the ambient space of a positive semidefinite lift is all matrices; this does not change which sets have lifts, because a lift in the symmetric matrices extends linearly and a lift in all matrices restricts to them. Positive semidefinite factorizations require both factor families to be positive semidefinite and use .
Reading decisions: the goal assumes , the paper's meaning of "a graph with vertices", since for the polytope is the image of and the printed statement fails. Milestone 3 also assumes , and so does Milestone 1 (Theorem 3.3): in the point has a proper lift to the whole space , whose dual cone cannot factor the slack matrix . In Milestone 4 the column is an arbitrary real vector. The slack matrices of Theorem 3.3 are encoded through the identification on p. 9 of the paper: rows are vertices of , columns are extreme points of the polar , the canonical entry is , and every slack matrix is the canonical one with positively scaled columns. Facets in Milestone 3 are nonempty proper exposed faces of dimension one less than the polytope.
The goal must not be weakened to proper lifts, and lifts must use equality with linear and affine; with inclusion, or with arbitrary maps, the statement becomes trivial or false. The core lemma is meaningful only with both factor families positive semidefinite; without that requirement factors trivially.
Beyond the milestones, a complete proof of the goal needs two facts the paper uses without stating them as claims of this proof: (a) an -lift that is not proper is a proper lift to a face of (p. 5), every face of is isomorphic to some with (Example 4.2, p. 12), and an -factorization yields an -factorization; (b) lifts are preserved by affine maps (Proposition 2.9, pp. 6–7), and translating a polytope changes its slack matrices only by positive column scalings, which is how Theorem 3.3 applies to , whose origin is a vertex rather than an interior point. Stating (a) and (b) as separate lemmas is welcome.
Needed infrastructure: positive semidefinite matrices and the trace pairing, the face structure of , invariance of lifts under affine maps, and conic duality for Theorem 3.3. All of these are reusable beyond this mission. Contributions welcome: proofs of the milestones, the bridging facts (a) and (b), and alternative routes to the goal.
Matroids abstract the combinatorial content of linear independence: which sets of columns of a matrix are independent, which are maximal (bases), and how bases relate to each other. This abstraction, isolated independently by Whitney (1935) and van der Waerden's school, turned out to be exactly the right level of generality for a large family of greedy and augmenting-path algorithms — a base of a matroid can always be reached from another by a sequence of single-element swaps, and this exchange property is what makes local search on bases correct and efficient.
A natural question, raised in the 1980s once matroid-based combinatorial optimization was mature, is what happens when bases are not merely present or absent but carry real-valued weights that must interact well with the exchange structure. Dress and Wenzel answered this with the notion of a valuated matroid: a real-valued function on the bases of a matroid satisfying a weighted strengthening of the exchange axiom. Their motivation was explicitly algorithmic — valuated matroids are exactly the structures for which a greedy algorithm computes an optimal basis under linear objectives, and more generally under the family of "tilted" objectives obtained by adding an arbitrary linear functional. Independently, valuated matroids arise from the classical Grassmann–Plücker relation applied to matrices over a field with a valuation (hence the name), connecting them to tropical geometry.
This mission formalizes the two theorems of Murota's Discrete Convex Analysis (2003, §2.4) that make this story precise: the classical correspondence between a matroid's base family and its rank function (Theorem 2.29), and the characterization of valuations by a perturbation-robustness property (Theorem 2.32). Theorem 2.32 is also historically the entry point of the book's central theme — it is the special case, for the two-valued lattice , of the general local-exchange criterion for M-convex functions that occupies chapters 6 and 7.
Let be a finite set (the ground set). A matroid on is a pair where , the base family, is a nonempty family of subsets of satisfying the simultaneous exchange axiom (B): for every and every , there exists such that both
Equivalently (Theorem 2.29 below), a matroid can be described by its rank function , a set function satisfying:
A valuation of a base family is a function satisfying the axiom (VM): for every and , there is with and
The pair is then a valuated matroid. For , the perturbation of by is
The right-hand side says: for every linear perturbation , the set of -maximal bases is again the base family of a matroid. The universal quantifier over is not optional — a version of this statement quantified over a single fixed is either vacuous or false, and does not capture what makes valuated matroids useful.
The maps
are mutually inverse bijections between nonempty families satisfying (B) and set functions satisfying (R1)-(R3). This is weaker groundwork than the goal, stated first because it fixes the exact axiomatic vocabulary — (B) and (R) — that Theorem 2.32 is built on.
The result itself. Theorem 2.32 is the reason valuated matroids are the right object for weighted combinatorial optimization on matroids: it says a function on bases behaves correctly under every linear re-weighting of the ground set exactly when it satisfies the local exchange inequality (VM). This is what guarantees, for instance, that a greedy algorithm which is correct for the unweighted matroid extends correctly to families of tilted objectives, and it is the germ of the general local-optimality criterion for M-convex functions (chapters 6–7), which underlies most of the algorithmic content of the rest of the book. Theorem 2.29 is the classical result — due jointly to the development of matroid theory from the 1930s onward — that the base-exchange and rank-submodularity axiomatizations of a matroid carry the same information; it is the finite, unweighted precursor of Theorem 2.32.
Formalizing it. Neither theorem has a machine-checked proof on the platform prior to this
mission (see Formalization scope for the prior-art check). Theorem 2.29's own proof is
elementary but has two independent halves (each map preserves its target axiom class, and the
two maps compose to the identity in both directions) that must all be established; Theorem
2.32's proof, as given in the source, defers entirely to a later, more general chapter-6
theorem, so a solver working only from this mission must either reconstruct a direct
combinatorial argument for this special case or await chunk 06 (DiscreteConvex.MConvexFunctions,
a separate mission) and specialize its main theorem.
The obvious approach to Theorem 2.32 — fix an optimal basis for and try to
show the exchange condition on maximizers directly from (VM) — proves one direction (VM implies
the maximizer property) in a few lines, since perturbing does not change which exchange moves
are available. The converse is the substantial direction: from "the maximizer set is always a
matroid, for every ," one must recover the single global inequality (VM) that must hold for
all pairs , not just optimal ones. The standard argument constructs, for
a given non-optimal pair, a perturbation under which that specific pair becomes
simultaneously optimal, and this construction is exactly the step the book skips by citing
chapter 6's general theorem. A formalization attempting to bypass this by only checking the
maximizer property for a finite or generic sample of perturbations would trivialize the
statement to something false or vacuous — a pitfall the goal's explicit ∀ p is designed to
prevent.
The ground set is a Fintype with DecidableEq; is represented as
Finset (Finset V), and as a plain function type. The rank function is
-valued (matching the book's own convention for matroid rank, as opposed to the
-valued conventions used from chapter 6 onward for general M-convex functions);
RankOfFamily is implemented with Finset.sup over rather than a partial max',
so that it is a total function — its junk value at the empty family is never invoked, since
every hypothesis in this mission supplies nonemptiness explicitly, matching the book's own
phrasing.
A trivializing formalization of the goal is one that quantifies over a single fixed , or allows to be empty; both are explicitly excluded by keeping a hypothesis and universally quantified inside the theorem statement itself.
Checked against Mathlib (commit 0df444a360eaa60ab8c11dca51a86af692955474): Mathlib's
Matroid structure is axiomatized via the single-element (asymmetric) exchange property,
classically but not definitionally equivalent to Murota's simultaneous axiom (B) used
throughout this book, and Mathlib provides no constructor recovering a base family or a
Matroid from a bare rank function satisfying (R1)-(R3). Theorem 2.29 is therefore genuine,
reusable infrastructure, not a restatement of existing Mathlib API. No reference item was found
on the platform for either theorem (GET /theorems?q=matroid, q=valuated matroid return only
unrelated tropical-geometry and k-server results). Contributions to a shared
DiscreteConvex.Combinatorial definitions layer (the exchange and rank axioms) are welcome
from later chunks of this series that build on matroid or base-polyhedron structure.
Many decision problems under uncertainty take the form of a stochastic program: choose a decision from a feasible set to maximise the expected utility , where the distribution of the uncertain parameter is known only through i.i.d. samples . The standard remedy, sample average approximation, maximises instead. Its consistency (convergence of the optimal expected utility of its solutions to the true optimum) is classical, but it needs regularity assumptions of its own, for example those of King and Wets (Stochastics and Stochastic Reports, 1991), cited on p. 98 of the paper; the paper presents its construction as a route to consistency under weaker conditions.
Robust optimization (RO) takes a different route: it protects each sample by an uncertainty set and optimises against the worst point in it. Xu, Caramanis and Mannor (Math. Oper. Res. 2012) show that RO over several overlapping uncertainty sets is equivalent to a distributionally robust stochastic program (their Theorem 2.1, the subject of mission I of this series). Section 3 of the paper uses that equivalence to show that a specific robustification of the sampled problem, with boxes of shrinking radius around each sample, is consistent under only boundedness and equicontinuity of . This mission formalizes that result, Theorem 3.1.
Equip with the sup norm , its Borel -algebra and Lebesgue measure . The data are:
For a sample the boxes are , and the box-robust sample objective is
The RO solution is a maximiser of over . The equicontinuity modulus of is
The proof works with the distribution set of probability measures with for every , and with the uniform box kernel density estimator
Assume for all ; as ; and . Then for every choice of maximisers , with probability one,
Milestones 1–4 are deterministic statements about a fixed sample; milestone 5 is the only probabilistic input.
Theorem 3.1 gives consistency of a tractable robust reformulation of a sampled stochastic program under conditions the paper notes are weaker than those of King and Wets for sampled stochastic programs: need only be bounded and equicontinuous in , uniformly in , and the true distribution need only have a density. It also gives an explicit schedule for the size of the uncertainty set, with , the bandwidth condition of kernel density estimation. Section 4 of the paper applies the same distributional interpretation to regularised learning methods such as the support vector machine and the Lasso.
The result is proved in the paper, with the consistency of kernel density estimators (Devroye 1983; Devroye and Györfi 1985) cited rather than proved. No part of it is formalized in Lean or on this platform as far as a search of the platform found. A complete development would produce, besides Theorem 3.1, a machine-checked strong consistency theorem for kernel density estimators, which is a basic result of nonparametric statistics in its own right.
The deterministic part (milestones 1–4) is measure-theoretic bookkeeping: the kernel integrates to one only because the box is a sup-norm ball of volume , and every infimum and supremum must be handled with care, since need not attain them.
The obstacle is milestone 5. Almost-sure convergence of to an arbitrary density , with no continuity or support assumption, does not follow from the strong law of large numbers applied pointwise: is an average of terms whose law changes with through , and almost-sure convergence at each fixed does not give convergence of the integral along a single sample path. The theorem needs both a bias estimate valid for every integrable density and a concentration estimate for the random error. Mathlib has Lebesgue differentiation and the strong law, but no kernel density estimator and no such concentration result.
Fin m → ℝ, whose Mathlib norm is the sup norm; boxes are Metric.closedBall. The integrals are Bochner integrals against Lebesgue measure of integrable integrands.X : ℕ → Ω → Fin m → ℝ on a probability space, independent (iIndepFun) and each with law volume.withDensity h*; become X 0, X 1, …, and the -th problem uses the first . "With probability one" is ∀ᵐ ω ∂P.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.
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.