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?
Every lower bound in bandit theory rests on one question: how hard is it to tell two probability measures apart from a sample? The answer is quantified by the relative entropy , and the sharpest elementary tool is the Bretagnolle–Huber inequality: for any event , — no test can distinguish from with total error probability below . This mission formalizes Chapter 14 of Lattimore–Szepesvári: the Bretagnolle–Huber inequality (the goal theorem, proved via Le Cam's inequality ), Pinsker's inequality , and the closed-form divergences between Gaussians and Bernoullis. These half-page inequalities power every impossibility result in Missions VII, XI and beyond.
Many convex optimization problems in machine learning and statistics have objectives that are convex but not differentiable: hinge losses, penalties, maxima of finitely many affine functions, and the dual functions of Lagrangian relaxations. Methods that rely on gradients do not apply to them directly, while cutting-plane methods such as the ellipsoid method pay a price that grows with the dimension. The projected subgradient method replaces the gradient by an arbitrary subgradient and restores feasibility by a Euclidean projection. Its guarantee depends on the dimension only through two constants, a radius and a Lipschitz constant . This is the reason it, and its descendants (mirror descent, stochastic gradient descent, online gradient descent), are the standard tools for large-scale nonsmooth problems.
The rate analysed here goes back to the subgradient methods of Shor and Polyak in the 1960s and 1970s and to the lower bounds of Nemirovski and Yudin (1983). The book follows the presentation of Nesterov, Introductory Lectures on Convex Optimization (2004). The strongly convex variant with weights proportional to is from Lacoste-Julien, Schmidt and Bach (2012).
This mission is the third of a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015), and covers the preamble of Chapter 3, Section 3.1 and Section 3.4.1.
Let carry the Euclidean inner product and norm . Let be compact and convex, and let be a convex function on with a minimizer .
A vector is a subgradient of at if for every . The set of subgradients at is written . The projection of a point is the point of nearest to .
Fix step sizes . Projected subgradient descent starts at some and iterates, for ,
Any subgradient may be chosen at each step. In Section 3.1 the step is constant, . The set lies in the Euclidean ball of radius centred at , and the subgradients have norm at most .
A function is -strongly convex on if for all and .
For every horizon , projected subgradient descent with the constant step satisfies
If is -strongly convex and its subgradients are bounded by , then with ,
Theorem 3.2 gives an oracle complexity of for reaching an -optimal point, independent of the ambient dimension. Section 3.5 of the book shows this rate is unimprovable for black-box first-order methods once the dimension is large. Theorem 3.9 shows how strong convexity improves the rate to , with the averaging weights changed from uniform to linear. These two bounds are the reference points against which the rest of Chapter 3 and Chapters 4 to 6 (smooth, accelerated, mirror, stochastic methods) are measured.
The results are classical and their proofs are short. Formalizing them produces a reusable, machine-checked account of the basic projected first-order step: the projection inequality, the one-step distance recursion, and the telescoping argument with Jensen's inequality for averaged iterates. To our knowledge, no machine-checked proof of the averaged-iterate bound for the projected subgradient method exists in Mathlib. Related platform items cover other algorithms or other averaging schemes.
The arithmetic is elementary, and the obvious argument works. The care is in the bookkeeping. The projection must be shown not to increase the distance to , which needs convexity of and the variational characterization of the nearest point. The sum must telescope with a horizon-dependent constant step. Jensen's inequality must be applied to a finite convex combination of points of , which requires showing that the average lies in . In Theorem 3.9 the step sizes and the averaging weights are coupled, so neither can be changed independently. In Lean, the iterates are indexed from with natural-number horizons, and the bounds involve , so these casts need care.
is EuclideanSpace ℝ (Fin n). The iterates are sequences ℕ → EuclideanSpace ℝ (Fin n) with the first iterate at index . The projection is the published relation OnlineConvexOpt.FirstOrder.IsMetricProjection ( is a nearest point to ). Subgradients are taken relative to (Definition 1.2). A run is a predicate on the steps , and every theorem holds for all runs, that is, for every choice of subgradients. Compactness and convexity of , convexity of on and the existence of the minimizer are the book's standing assumptions and appear as hypotheses. , and are explicit, because Lean's division by zero would otherwise turn the step size into a junk value.
The book assumes for every subgradient at every point of . With subgradients relative to a compact , that assumption can never hold at a boundary point, since every outward normal can be added to a subgradient. Stated that way the theorems would be vacuous. The mission therefore assumes the bound only for the subgradients that the run uses. This is a weaker hypothesis and gives a stronger, non-vacuous statement. Bounding only these subgradients is a deliberate choice, not a trivialization: the bound still constrains every quantity the conclusion depends on.
Contributions welcome: proofs of the four inequalities and of the two rates, and a reusable lemma that the convex combination of finitely many points of a convex set lies in the set, together with Jensen's inequality in the form used here.
An airline sells the seats of one flight in several fare classes at different prices, all drawn from one shared cabin. Discount fares are bought early, under advance-purchase restrictions, while most high-fare requests arrive close to departure. Accepting every early low-fare request fills the aircraft with cheap passengers and turns away late high-fare passengers; refusing too many leaves seats empty. Seat inventory control decides how many seats to keep away from the low fare. Peter Belobaba's 1987 MIT thesis (Flight Transportation Laboratory Report R87-7) introduced the expected marginal seat revenue (EMSR) model for this decision, and EMSR-type rules remain the basis of the booking-limit logic in airline revenue management systems.
Timeline. Littlewood (1972, AGIFORS Symposium Proceedings; reprinted 2005) proposed accepting a low-fare request as long as its fare is at least the high fare times the probability of selling all remaining seats to high-fare passengers. Analysts at Trans World Airlines (1973) and Richter at Lufthansa (1982) gave equivalent formulations for the dynamic case. Belobaba (1987, Ch. 5) restated the two-class rule as a static protection level for nested inventories and extended it heuristically to many classes. Brumelle and McGill (Operations Research 41, 1993) and Curry (Transportation Science 24, 1990) later proved optimality of nested protection levels for any number of classes under low-to-high arrivals, and showed that Belobaba's multi-class EMSR levels are not optimal for three or more classes. This mission concerns only the two-class result, which is correct.
A single flight leg has capacity . Class 1 has fare , class 2 has fare , with . The numbers of requests for the two classes are random variables with values in , defined on a probability space and independent. There are no cancellations, no no-shows, and a refused request is lost.
The inventory is nested: a class-1 request is accepted as long as any seat is unsold. A protection level is the number of seats reserved for class 1; it sets the class-2 booking limit . All class-2 requests arrive before any class-1 request. Class 2 therefore books seats and class 1 books , and the realised revenue is
The expected revenue is .
The tail probability of class 1 is , the probability of receiving or more class-1 requests, and the expected marginal seat revenue of the -th class-1 seat is
For a single class with seats the expected revenue is , and is its increment from to seats. The EMSR protection level is the largest integer with
In Lean these objects are nestedRevenue, expectedNestedRevenue, tailProb, classRevenue, emsr and emsrProtectionLevel in SeatInventory.Nested.
The goal fixes no distribution: it holds for every pair of independent -valued demands, and depends only on and the law of .
RevenueManagement.littlewood_marginal_value (Talluri and van Ryzin's Eq. (2.1), proved).The two-class result says that, for a static booking limit set once before sales open and low-fare demand arriving first, the airline needs only the high-fare demand distribution and the fare ratio to set the optimal limit; the low-fare forecast is irrelevant. This is the rule that the thesis then applies class by class in multi-class nested systems, and it is the base case against which the later exact multi-class theory (Brumelle–McGill, Curry) is checked. Milestone 5 makes precise why nested inventories dominate the distinct-inventory allocation of the thesis's Sect. 5.1 with the same class-2 limit.
The result is classical and proved, in the sense that the optimality of a two-class threshold policy follows from Littlewood's argument and from the dynamic-programming treatment in Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004, Ch. 2). On Prove2Me, Littlewood's marginal rule and the dynamic-programming optimality of nested protection levels (RevenueManagement.static_optimal_controls) are formalized, but in Bellman form: there the protection level is defined through the value function of a dynamic program. What is not formalized is the statement in Belobaba's form, where the protection level is the explicit threshold of against and the objective is the explicit expected revenue of a booking limit. Connecting the two forms, and the comparison with distinct inventories, is the work of this mission.
The expected revenue couples the two demands through the capacity left by class 2, so is not a sum of single-class revenues and is not separately concave in an obvious way. The step that requires care is the increment : it is not , as the thesis's sentence after the milestone on p. 112 suggests, because the extra protected seat matters only on the event that class 2 would have reached its limit. Independence of and is what makes that event's probability factor out; without independence the threshold rule is not optimal. The discrete reading matters too: with in place of the rule is off by one seat and the claim fails.
Conventions the Lean statements commit to:
r₁ r₂ : Ω → ℕ on a probability space μ; the goal and milestone 4 assume IndepFun r₁ r₂ μ. The thesis writes continuous densities (Eqs. (5.1)–(5.5)) but requires integer seat counts; the discrete model is used throughout.μ.real; seat counts use truncated subtraction only where .A trivializing formalization is ruled out: is defined by the threshold of (5.15), never as an argmax of expected revenue, and the expected revenue is computed from the realised revenue of the booking process, not postulated as a sum of marginal terms.
The multi-class EMSR levels of Eqs. (5.19)–(5.29) and the dynamic revision of Eqs. (5.31)–(5.32) are out of scope. Proofs need the discrete expectation identity and expectation of products of independent bounded functions, both in Mathlib's reach and reusable for other single-leg revenue models. Proofs of any milestone, and a proof of the goal from milestones 1, 2 and 4 plus the matching lower-half argument, are welcome.
In a short 1997 letter, Max Tegmark argued that, given the other laws of physics, a spacetime with space and time dimensions can host observers who understand and predict their world only when (Tegmark 1997). The argument is physical and anthropic, but each step rests on a precise mathematical fact: the classification of second-order linear PDEs into elliptic, hyperbolic and ultrahyperbolic type, the well-posedness (or ill-posedness) of the corresponding initial-value problems, the potential theory of , the stability of Kepler orbits, and the algebra of curvature tensors in low dimension. This mission collects those mathematical facts as formal targets.
Timeline of the ingredients cited by the letter:
A second-order linear PDE on has the form
with symmetric. Following the paper, at a point it is elliptic if all eigenvalues of are positive or all are negative, hyperbolic if one eigenvalue is positive and the rest negative (or vice versa), and ultrahyperbolic if at least two are positive and at least two negative. Eigenvalues are counted with multiplicity; the Lean development counts them as the positive/negative real roots of the characteristic polynomial (numPosEigenvalues, numNegEigenvalues, IsElliptic, IsHyperbolic, IsUltrahyperbolic).
A spacetime of dimensionality carries a metric with positive (time-like) and negative (space-like) eigenvalues, so that has signature . The covariant field equations (wave) and (Klein–Gordon) have coefficient matrix . The Laplacian on is (laplacian).
For a symmetric with positive and negative eigenvalues,
The goal makes precise the paper's central new observation: the hyperbolicity needed for a well-posed initial-value problem singles out exactly one time dimension (or, in the tachyonic mirror case, one space dimension). The milestones supply the mathematical content behind each of the paper's other claims, namely instability for and the absence of gravity for , as well as the well-posedness and ill-posedness facts behind the "predictability" argument. All of these are classical results; none of them is new mathematics. The value of the mission is a machine-checked record of exactly which mathematical statements the argument uses, under which hypotheses, and with which caveats (for instance the critical coupling in four dimensions).
The goal is linear algebra. The difficulty lies in the milestones: Ásgeirsson's theorem and the Klein–Gordon energy estimate need integration over spheres and balls, a divergence theorem or spherical-mean calculus, and differentiation under the integral sign, and Mathlib supports these only partially. The four-dimensional hydrogen case sits exactly at the Hardy-inequality threshold, where the outcome depends on the coupling constant.
Fin d; eigenvalue counts are root counts of the characteristic polynomial with multiplicity. Classification is pointwise: one constant coefficient matrix.EuclideanSpace ℝ (Fin n); derivatives are Fréchet derivatives, and the Laplacian is the sum of pure second derivatives along the standard basis.Reusable infrastructure: PDE type via eigenvalue signs, spherical means, and local energy estimates for wave-type equations.
The simplex method is the standard algorithm for linear programming, and its correctness rests on one question: does it stop? Each pivot of the method moves from one dictionary to another without decreasing the objective value, but a pivot can leave the objective unchanged. When that happens repeatedly, the method can return to a dictionary it has already visited and loop forever. This behaviour, cycling, is not hypothetical: Vanderbei's Chapter 3 exhibits a problem with four decision variables and three constraints on which the "largest coefficient" entering rule with a natural tie-breaking rule cycles through six dictionaries (Vanderbei 2014, pp. 26–27).
The chapter answers the question with two pivoting rules under which the simplex method provably terminates, and then draws the consequence that makes linear programming a finite theory: the fundamental theorem of linear programming. This mission formalizes the chapter's four numbered theorems in Vanderbei's own setting of standard-form problems with slack variables.
Timeline. Hoffman (1953) and Beale (1955) gave the first examples of cycling. The perturbation and lexicographic methods go back to Charnes (1952) and to Dantzig, Orden and Wolfe (1955). Bland (1977) introduced the smallest-index rule and proved that the simplex method terminates under it (Bland 1977).
A linear program in standard form has constraints and decision variables:
A solution is feasible if it satisfies every constraint, and optimal if in addition it maximizes the objective among feasible solutions. The problem is infeasible if no feasible solution exists, and unbounded if it has feasible solutions with arbitrarily large objective values.
The slack variables are appended to the list of variables as , so that the constraints become the linear system with in . A dictionary is given by a set of basic indices whose columns of are linearly independent; the remaining indices are nonbasic. Solving for the basic variables gives
The basic solution of the dictionary sets the nonbasic variables to zero. The dictionary is feasible if for every , and degenerate if for some .
The simplex method (Phase II) starts at a feasible dictionary and repeats a pivot: an entering variable is chosen among the nonbasic variables with , and a leaving variable among the basic variables with that minimize the ratio ; then becomes basic and nonbasic. The method stops when no is positive (the dictionary is optimal) or when the entering column has no positive (the problem is unbounded). A pivoting rule resolves the remaining choices. Bland's rule chooses both the entering and the leaving variable as the candidate with the smallest index. The lexicographic rule perturbs the right-hand sides by symbols all data and chooses the leaving variable by the perturbed ratio test.
From every feasible dictionary , there is no infinite sequence of pivots
in which both the entering and the leaving variable follow Bland's rule; and a finite sequence of such pivots reaches a dictionary at which the method stops, optimal or exhibiting unboundedness.
The result. Termination under Bland's rule is what turns the simplex method from a heuristic into an algorithm. Combined with Phase I, it yields the fundamental theorem of linear programming, which reduces the search for an optimum to finitely many basic solutions and underlies the duality theory of the following chapters. Bland's rule also needs no perturbation or extra bookkeeping, and it is the anticycling rule used in many correctness proofs of simplex-type and combinatorial pivoting algorithms, including oriented-matroid programming.
Formalizing it. All four theorems are classical and proved. The Prove2Me library has the lexicographic rule and a nondegenerate termination theorem in the tableau setting of Bertsimas and Tsitsiklis (equality form , , full row rank), and the existence of basic feasible and optimal solutions in that form. It has no statement of Bland's theorem, and none of Vanderbei's dictionary formulation over . This mission produces a machine-checkable model of dictionaries and pivoting rules in that formulation, and targets Bland's theorem, whose proof is a genuine combinatorial argument rather than a monotonicity argument.
The natural argument for termination is monotonicity: each pivot increases the objective, so no dictionary repeats. It fails exactly at degenerate pivots, where the step length is zero and the objective and the basic solution do not change. Bland's rule gives no potential function that strictly increases along degenerate pivots, so the proof has to reason about a hypothetical cycle as a whole: which variables enter and leave the basis within it, and how two dictionaries of the cycle, in which the same variable leaves and later enters, constrain each other's coefficients. Relating the coefficients of two different dictionaries of the same problem is the step that has no counterpart in the model's definitions and has to be developed.
For Theorem 3.2, the symbols cannot be replaced by a fixed small real number: the method treats them as formal quantities on separate scales, and the statement is about that symbolic rule.
Vectors are Fin n → ℝ, Fin m → ℝ, and the constraint matrix is Matrix (Fin m) (Fin n) ℝ. The variables are indexed by Fin (n + m) with the decision variables first and the slacks after them, which is the order that Bland's rule compares. A dictionary is a structure holding its basic set, a proof that it has elements and a proof that its columns of are linearly independent; the coefficients are computed as coordinates in the basis of basic columns. A dictionary is therefore determined by its basic set, as the proof of Theorem 3.1 uses. "Basic solution" is defined through such a dictionary, not as a support condition.
Termination is stated as the nonexistence of an infinite run from a feasible dictionary, for Theorems 3.2 and 3.3. The goal adds that a finite Bland run reaches a stopping dictionary, so that it cannot hold because pivots fail to exist. The lexicographic rule is encoded by lexicographic comparison of the coefficient vectors of the perturbed ratios; the symbol is attached in the starting dictionary to its -th basic variable in increasing index order, which for the initial dictionary is the -th constraint. Unboundedness in Theorem 3.4 is "for every a feasible solution with objective ", as defined on p. 7. The statements carry no explicit constants.
A formalization that stated Theorem 3.3 for arbitrary pivot sequences with pairwise distinct bases would be Theorem 3.1's counting argument, not Bland's theorem; the goal is stated for pivots that follow Bland's rule and only those.
A complete development needs: the pivot update of a dictionary and the invariance of the solution set under it, feasibility preservation by the ratio test, the relation between the objective rows of two dictionaries, and finiteness of the set of bases. These are reusable for any later formalization of simplex-type algorithms. Proofs of the milestones, alternative proofs of Theorem 3.3, and Phase I (to connect Theorem 3.4 with the algorithm) are welcome.
Many optimization problems in operations research have objectives that are convex but not differentiable: the maximum of finitely many linear or smooth functions, the value function of a Lagrangian dual, the cost of a two-stage linear program as a function of the first-stage decision. Gradient methods do not apply to these directly. N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer Series in Computational Mathematics 3, 1985; translated by K. C. Kiwiel and A. Ruszczyński from the 1979 Russian edition) develops the algorithms that replace the gradient by a subgradient, and its first chapter sets up the calculus of subgradients these algorithms rely on.
This mission is the first of a series formalizing the book. It covers §1.2 (convex functions and the concept of subgradient) and §1.3 (rules for computing subgradients), printed pages 7–16. Every later mission in the series (the subgradient method, space dilation, the ellipsoid method, decomposition) assumes that a subgradient of the objective can be computed, and §1.3 is where the book explains how: by combining subgradients of simpler pieces.
Write for -dimensional Euclidean space with inner product and norm . A function with domain a convex set is convex if its epigraph is convex, equivalently for and .
Let be an interior point of . A vector is a subgradient (or generalized gradient) of at if
The set of all subgradients is the subdifferential, written or . For differentiable at it is the single gradient; for on it is at .
The one-sided directional derivative of at in direction is
A direction is a direction of steepest descent at if .
For convex on and , the function is convex and, at every ,
Both inclusions are part of the goal.
The result. Theorem 1.12 is the finite-dimensional, finite-valued case of the Moreau–Rockafellar sum rule. With Theorem 1.13 it is the book's recipe for computing subgradients of functions assembled from simple pieces by nonnegative combinations and pointwise maxima, the two operations that produce most nonsmooth convex objectives in practice (Lagrangian duals, penalty functions, piecewise-linear costs). Theorem 1.8 identifies the directional derivative with the support function of the subdifferential; the Corollary and Theorem 1.11 give the optimality condition and the steepest-descent direction that every descent method for nonsmooth convex functions starts from.
Formalizing it. These results are classical and have been proved many times in textbooks (Rockafellar, Convex Analysis, 1970, §23). Mathlib at the pinned revision has convexity, separation theorems and Carathéodory's theorem, but no subdifferential of a convex function on and no max formula. The mission builds that layer: a subdifferential with the book's inequality (1.3), a one-sided directional derivative defined as a right-hand limit, and the calculus rules above. The platform has a Clarke-gradient analogue of Theorem 1.8 for locally Lipschitz functions and a Banach-space sum rule for ; neither states the convex, finite-dimensional results here.
The inclusion "" in Theorem 1.12 is immediate from (1.3). The inclusion "" is the content: a subgradient of the sum is a global object, and nothing in (1.3) splits it into subgradients of the pieces. Adding the inequalities of the pieces only produces vectors of the right form; it does not show every subgradient of arises this way. Any argument has to use the finite dimension and the interior-point setting, which is where Theorems 1.7 and 1.8 (existence of subgradients, compactness of , existence of one-sided derivatives) come in.
Theorem 1.8 in turn needs the existence of a finite right-hand limit of the difference quotient, which requires both monotonicity of the quotient and a lower bound, and the existence of a subgradient attaining the maximum, which is a separation statement. Theorem 1.9's "if" direction must rebuild convexity from one-sided derivative information alone, with no differentiability assumption.
EuclideanSpace ℝ (Fin n) and is inner ℝ x y. A function is f : EuclideanSpace ℝ (Fin n) → ℝ; the domain is a set, convexity on it is ConvexOn ℝ M f (which includes convexity of ), and interior points are x₀ ∈ interior M. Theorems 1.9, 1.10, 1.12 and 1.13 are stated on all of (Set.univ), as the book proves them.subdifferential M f x₀ is the set of with for all . It is defined for any ; the interior-point assumption is a hypothesis of each theorem that needs it.HasOneSidedDirDeriv f x₀ η d is the right-hand limit Tendsto … (𝓝[>] 0) (𝓝 d), not Mathlib's two-sided lineDeriv. Maxima and minima are stated with IsGreatest/IsLeast (attained), never with sSup/sInf.Fin k; and zero coefficients are allowed, as in the book. Theorem 1.13's maximum is Finset.sup' over Fin m with , and it asserts only the inclusion the book states.geometric_hahn_banach_*, Carathéodory and Krein–Milman, ConvexOn.continuousOn_interior) and are not restated.Contributions welcome: proofs of any milestone, a reusable lemma that the difference quotient of a convex function is monotone in , and a general max formula; these are reusable in the later missions of the series, which define subgradients the same way.
Optimal control of queueing systems leads to Markov decision problems whose state space is countably infinite (buffer contents, numbers of customers) and whose costs are unbounded (holding costs grow with the queue). Such a problem cannot be solved on a computer as it stands. The standard remedy is to truncate: solve a finite problem on the states and hope that its value and its optimal policy approximate those of the original problem as grows. Linn Sennott's approximating sequence method (ASM) makes this hope precise. For the expected discounted cost criterion, Sections 4.6–4.7 of Sennott's book (Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999) identify a single condition, Assumption DC(), that is necessary and sufficient for convergence of the truncated values, and give checkable sufficient conditions for it.
The method matters because naive truncation can fail. The book's Example 4.6.1 has a chain whose value at state is finite, yet a natural truncation produces values . How the probability that would leave the truncated set is redistributed decides whether the computation is meaningful.
Earlier truncation schemes (Fox 1971; White 1980, 1982; Hernández-Lerma 1986; Cavazos-Cadena 1986; Whitt 1978–79; see the bibliographic notes on p. 81 of the book and Puterman 1994) require bounded rewards or pass directly to an algorithm. The ASM instead produces a sequence of finite Markov decision chains that can be studied in their own right; the material of Sections 4.6–4.7 is presented in the book as new.
A Markov decision chain (MDC) has a countable state space ; for each state a finite nonempty action set ; nonnegative finite costs ; and transition probabilities with . A policy chooses the action at time at random from a distribution on that may depend on the entire history . A stationary policy always chooses in state . Fix a discount factor . The discounted cost of and the discounted value function are
both in , the infimum over all policies. A policy is discount optimal if .
An approximating sequence consists of finite nonempty sets increasing to and, for and , probability distributions on with as . The finite MDC has state space and the same actions and costs; is its value function and a stationary policy attaining the minimum in its discount optimality equation
An augmentation type approximating sequence (ATAS) keeps the original probabilities inside and redistributes the excess probability , , according to augmentation distributions on : .
Assumption DC(): for every , and .
The following are equivalent:
Under either, every limit point of (a stationary with eventually along a subsequence, for each ) is discount optimal for .
Theorem 4.6.3 turns the question "does truncation work?" into the verification of one inequality between a lim sup and the true value, and it delivers both the value and an optimal stationary policy from finite computations. Propositions 4.7.4–4.7.6 give conditions that hold in the queueing models of the book with unbounded holding costs, and Corollary 4.7.5 supplies the computational form used for the inventory model of Chapter 5. The discounted theory is also the stepping stone to the average cost ASM of Chapter 8, which is built on discounted approximations.
All results are proved in the book. None of them is formalized: the platform has no statement about approximating sequences or state truncation of countable-state MDPs, and Mathlib has no Markov decision processes. The mission produces machine-checked versions of the convergence theorem and its sufficient conditions, for general history-dependent randomized policies and -valued costs.
The value functions are infima over uncountably many history-dependent policies and may be infinite, so no contraction argument applies: costs are unbounded and is only the minimal nonnegative solution of its optimality equation. Passing to the limit in inside is an interchange of limit and infinite sum under a moving probability measure, with no dominating function in general; Example 4.6.1 shows that the interchange genuinely fails. The upper bound of Proposition 4.7.4 requires comparing with along a coupled first passage out of , which needs the taboo-probability estimates of Lemmas 4.7.2–4.7.3. The obvious idea of bounding by works only for bounded costs (Proposition 4.7.1).
The state type S is countable ([Countable S]); actions live in a type Act, with a finite nonempty Finset of admissible actions per state. Costs are ℝ≥0, transition probabilities and all value functions are ℝ≥0∞, so infima over policies are lattice infima and is a legitimate value. A general policy is a function of the history, encoded as the list of past state–action pairs (most recent first) and the current state; the expected cost at time is the -valued sum over histories. is the infimum over all such policies; a stationary policy enters as the policy putting mass one on . The discount factor is α : ℝ≥0 with (the chapter's standing assumption). is an MDC on the subtype ; is extended by when or , a convention that affects finitely many for each fixed and hence no limit in . Limits, lim sups and lim infs are along Filter.atTop in ℝ≥0∞. Taboo probabilities and the first passage quantity (so ) are defined combinatorially from the transition probabilities.
A trivializing formalization is ruled out: is not an infimum over stationary policies only (which would make optimality of limit points close to definitional), DC() keeps both of its conditions, and statement (i) of the goal includes finiteness of .
A complete development needs the minimality of among nonnegative solutions of the discount optimality equation (Theorem 4.1.4, chunk II of this series), Fatou-type lemmas for sums against converging distributions (Appendix A, chunk XI), and compactness of stationary policies (Proposition B.5). Contributions of these as reusable lemmas about countable-state MDCs are welcome.
The solution concept of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944) is defined from two ingredients: a set of imputations and a domination relation between them. A solution is a set of imputations that is internally stable (no member dominates another) and externally stable (every non-member is dominated by some member). In §65 of the book the authors observe that this definition never uses what imputations and domination actually are. They abstract it to an arbitrary set and an arbitrary relation on , and ask which properties of guarantee that exactly one solution exists.
The abstract notion is what graph theory now calls a kernel of a directed graph: draw an arc whenever ; a solution is a set of vertices that is independent and absorbs every vertex outside it. Kernels appear in combinatorial game theory (the losing positions of a finite impartial game form a kernel of its move graph) and in the theory of preference and choice.
Timeline.
Let be an arbitrary set and an arbitrary relation on ; is read " dominates ". A solution (in for ) is a set with
For , an element is a maximum of if and no has ; the set of maxima is .
For , condition says: never with and all . The relation is acyclic if it satisfies every , ; in particular never . It is strictly acyclic if there is no infinite sequence in with for every . Property (65:K) says that every non-empty has . A partial ordering (65:B) is a transitive relation for which at most one of , , holds.
For the main theorem the book constructs a candidate solution by induction (65.7.1): ; ; is the set of elements of dominated by some element of ; . With the first index for which ,
In Lean the elements live in a type α, D V : Set α, and S : α → α → Prop with S x y meaning ; the predicates are IsSolution D S V, maxima E S, IsAcyclic, IsStrictlyAcyclic, HasMaximaProperty, IsPartialOrdering, ConditionG, and the construction stageA, stageB, stageC, V0.
If is finite and is acyclic on , then
The result itself. (65:X) is the most general of the book's three existence-and-uniqueness theorems for solutions (complete ordering, partial ordering, acyclic relation; 65.8.1). For games proper it has no direct application: the set of imputations of an essential game has no maxima, so (65:K) fails (65.9.1). Its role is to isolate a sufficient condition for a unique solution. With (65:Z), and applied to every subset of , it characterizes the finite relations for which every subset has exactly one solution: exactly the acyclic ones (65.8.2). In graph language it is the statement that a finite directed acyclic graph has exactly one kernel. In combinatorial game theory this is the partition of the positions of a finite impartial game into P- and N-positions. The complete- and partial-ordering results (65:E)–(65:I) are the special cases the book treats first.
Formalizing it. The results are classical and fully proved in the book; to the best of our knowledge none of them is on the Prove2Me platform, and Mathlib has well-foundedness (WellFounded, RelEmbedding of ℕ) but no kernel or von Neumann–Morgenstern solution notion for an abstract relation. The mission produces machine-checked proofs of the book's §65 chain: the equivalence of (65:K) with strict acyclicity for arbitrary sets, the finite equivalence of acyclicity and strict acyclicity, the explicit construction of , and the characterization of 65.8.2.
Most of the individual steps are short. The work is in making the book's finite induction precise. The sets are defined recursively and refers to the first empty stage . The uniqueness proof (65:V) is a minimal-counterexample argument over the stage index, which moves between "smallest with " and the disjoint decomposition (65:U) of into the and . A tempting shortcut, taking an arbitrary well-founded rank function instead of the book's construction, proves existence and uniqueness but not that the solution is the of (65:2), which is part of the goal. For (65:P) and (65:O:c) the difficulty is the passage between finite cycles and infinite chains. Going from a chain in a finite set to a repetition needs a pigeonhole argument, and going from a set without maxima to a chain needs dependent choice.
α; D, E, V are Set α; the relation is S : α → α → Prop and is only ever consulted on elements of the set under consideration, so it is the book's relation on (or its restriction to ). Finite and infinite sequences are functions ℕ → α.IsSolution D S V is the set equation (65:1) literally; it forces . Uniqueness in the goal is ∃! over all V : Set α, not over a subtype; there is no degenerate reading in which the solution is fixed by construction.IsAcyclic D S requires for every , all cycle elements in . The case is excluded, as in the book (it would be unsatisfiable). This is equivalent to the absence of a Relation.TransGen loop inside , but the book's form is stated.stageA D S k is the book's . V0 D S is the union of all , which equals because every later is empty.D.Finite and IsAcyclic D S. (65:H) and (65:I) carry the partial-ordering hypothesis (65:B:a), (65:B:b) of 65.5.1, and (65:I) also finiteness of . (65:O:c), (65:P) and (65:Z) are for arbitrary and , as 65.6.2 and 65.8.2 state. The empty is allowed everywhere; there the unique solution is .Set.Finite, dependent choice for (65:P). The definitions are reusable for any later work on kernels of digraphs and on abstract stable sets. Proofs of any milestone, and alternative proofs of the goal, are welcome.The theory of Theory of Games and Economic Behavior (von Neumann and Morgenstern, 1944; 3rd ed. 1953) rests on one object: the characteristic function , the amount a coalition of players can secure for itself whatever the other players do. For zero-sum -person games, Chapter VI defines and proves (25.3.1 and 26.1.1) that the set functions arising this way are exactly those with , and superadditivity. Economic applications, however, are rarely zero-sum: exchange and production create value. Chapter XI extends the theory to general (non-zero-sum) games by adding a fictitious player who absorbs the total gain, and §57 answers the question that decides the scope of this extension: which set functions are characteristic functions of general games?
The answer, that these are exactly the superadditive set functions vanishing on the empty set, is the reason why the cooperative game theory that followed could take "a superadditive with " as its primitive object, usually without any underlying strategic game.
A general -person game in normalized form has players . Player chooses with , without knowing the choices of the others, and receives the real amount . No condition is imposed on . The game is zero-sum if .
The zero-sum extension (56.2.2) adds a fictitious player , who has no move and receives
Write . For , the coalition and its complement play a zero-sum two-person game. The pure strategies of are the tuples of choices of its real members. A mixed strategy of is a single probability distribution over these tuples, so the members of a coalition randomize jointly, and likewise for . The payoff to is . Then
where is the expected payoff to . The function on all is the extended characteristic function; its restriction to is the restricted characteristic function (57.1). For a zero-sum game the restricted function is the characteristic function of Chapter VI.
For every and every set function on the subsets of ,
and for every set function on the subsets of ,
In each direction a single game realizes on every set simultaneously; is not constrained.
The characterization fixes the domain of Chapter XI: every statement about solutions of general games is, by 57.3.4, a statement about superadditive set functions with , and conversely every such function is attained by a strategic game. That converse justifies studying cooperative games abstractly. (57:G) separates the zero-sum and constant-sum subclasses inside this domain. (57:B) and (57:C) quantify how much of a player's strategic role survives when his moves are removed, which is the book's justification for the fictitious player.
Status: all results are proved in the book (1944). To our knowledge none of them is machine-checked; the Prove2Me catalog has superadditive and convex cooperative games, but none tied to a strategic game, and no characteristic function built from a minimax value. The work here is formalizing the known proofs.
Necessity reduces to the zero-sum theory applied to , but still requires the minimax theorem for the coalition's two-person game and a careful treatment of joint mixing when two disjoint coalitions merge. Sufficiency requires building one finite game whose coalition values equal an arbitrary superadditive exactly, for all coalitions at once. The obvious attempt, choosing payoffs coalition by coalition, fails because the payoffs are shared: a construction that gives the right value can change the value of every set that overlaps . The difficulty is to obtain the upper bound for every simultaneously. For the extended function there is a further difficulty. The fictitious player has no move, so the values on sets containing are forced by the others, and they must be reconciled with (57:1:b).
For (57:B), the target game must reproduce an arbitrary zero-sum characteristic function while one prescribed player's choice has no effect on any payoff.
Players are Fin n (book indices become ); sets of players are Finset (Fin n). The extended domain is Fin (n + 1) with the fictitious player Fin.last n, and is the complement in Fin (n + 1). A game (GeneralGame n) has strategies Fin (β k) per player and real payoffs; zero-sum is the predicate IsZeroSum. The fictitious player's single strategy is left out of the coalition's strategy tuples, which does not change the two-person game. Max and Min are ⨆/⨅ over Mathlib's stdSimplex on the coalition's strategy tuples (one joint distribution per coalition). Both simplices are nonempty and the payoff is bounded, so these are attained values and no junk value from an empty or unbounded supremum occurs.
Standing hypotheses and their instantiation:
GeneralGame;Γ.IsZeroSum and the requirement that the replacement game is zero-sum;No normalization is imposed: is arbitrary and nothing is reduced. Every statement is made for all ; the book's is not needed, so this is a strengthening.
A trivializing formalization is ruled out: the characteristic function is defined from the game through the coalition's minimax value, so it is never a free parameter, and the existence claims must produce one game for all coalitions at once.
Needed infrastructure: finite zero-sum two-person games with joint mixed strategies over dependent product types; the minimax theorem ((17:6), on the platform as AGT.zero_sum_minimax for matrices); and product decompositions of coalition strategy tuples. The coalition-value API is reusable for any mission built on characteristic functions (Chapters VI, IX–XI). Contributions of this API as separate lemmas are welcome.
Not stated: (57:E*), (57:F*) (given without proof on p. 535), the open question (57:D), and (57:H), because the notion of a "dummy" it uses (from 46.9 and 56.3) is not defined on these pages.
Many collective decisions are taken by coalitions that either carry the vote or do not: committees, legislatures, shareholder meetings, councils with weighted votes. In such a situation the only aim of a participant is to be part of a coalition that wins, and nothing is left to bargain about except the division of the prize inside the winning coalition. Chapter X of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; 3rd ed. 1953) isolates exactly this class of zero-sum -person games, the simple games, and studies their numerical description by weighted majorities and their finite main simple solutions.
The chapter is the origin of a large later literature: simple games and weighted voting games are the standard model of voting bodies in political science and social choice (for instance the Shapley–Shubik power index, 1954). The characterization of which simple games admit homogeneous weights, and the solutions they carry, starts here.
A zero-sum -person game with players is represented by its characteristic function , a real function on the subsets of with , ( the complement) and for disjoint . An imputation is a vector with and ; dominates if some nonempty has and for ; a solution is a set of imputations none of which dominates another and which dominates every imputation outside it (30.1.1). The game is inessential when its reduced form vanishes identically, essential otherwise.
A coalition is flat if . The losing coalitions are the flat sets, and the winning coalitions are the sets whose complement is flat. The game is simple if it is essential and every coalition is winning or losing. denotes the minimal winning coalitions, those of which no proper subset wins.
Weights define the winning system , and under the conditions (50:B) (non-negative weights, no player with half the total weight, no ties) this is the weighted majority game . The weights are homogeneous if the advantage is the same for all in .
In §50 the game is taken in reduced form with , so . For numbers and a coalition let give to the players outside and to player in . When the satisfy for every , the set of all , , is a main simple solution.
namely the set of , , with , , the common advantage. Conversely, if solve on , then are homogeneous weights for the game if and only if
The result links two descriptions of a simple game. One is numerical: a vector of weights, normalized by homogeneity. The other is game-theoretic: a finite solution in which each minimal winning coalition forms and divides a fixed total among its members. When the weights are homogeneous they are, up to scale, the shares in the main simple solution. When a main simple solution exists, its shares are homogeneous weights exactly under the inequality (50:20). The criterion (50:J) behind it is the chapter's general tool for deciding which systems of "profitable" minimal winning coalitions yield a finite solution. It is used again in the enumeration of simple games in §§51–55.
All of the results are proved in the book. As far as a search of the Prove2Me library shows (queries on simple game, weighted majority, winning coalition and stable set, 2026-09-28), none of them has been machine-checked. The only stable-set statements on the platform concern feasible payoff vectors of convex games, which is a different domain. The mission therefore asks for a formal proof of the known results, including the case analysis of §50.5–50.6, and in doing so it produces a reusable Lean theory of simple games and their winning systems.
The characterizations of §49 are set-theoretic, but they depend on superadditivity to show that subsets of flat sets are flat, and on the strategic-equivalence description of essentiality. The substantial part is (50:J). Deciding whether is a solution means classifying every imputation by the set where it meets the shares .
The natural first attempt is to check only the minimal winning coalitions. It fails, because domination can be exercised through any winning coalition. The book's argument has to exclude sets of with by producing infinitely many undominated imputations against a finite . It also has to handle indifferent players with , whose presence makes larger than the coalition that generated . For the converse half of the goal, the obstacle is the strict inequality : the equations (50:17) are linear and say nothing about it.
Players are Fin n (the book's player is index ), coalitions are Finset (Fin n), and characteristic functions are Finset (Fin n) → ℝ. Imputations are vectors Fin n → ℝ, and systems of coalitions are Set (Finset (Fin n)). A game is identified with its characteristic function (by 26.1 every satisfying (25:3:a)–(25:3:c) arises from a game). The theory is the "old" one of 30.1.1 (49.1.1), with no excess. The definitions of imputation, domination and solution are the same as in mission V of this series and are restated here, because a draft cannot import another draft.
The standing hypotheses, stated in each theorem where the book has them in force:
The numbers are given for every player. Players in no minimal winning coalition, for whom the book defines no , do not affect any . In the converse of (50:K) the derived weights are for every player.
The goal is not the bare solvability of (50:17). A statement that only asserted " exists with (50:7), (50:17)" would reduce to linear algebra. The goal asserts that the set of is a solution in the sense of 30.1.1, with domination requiring a nonempty effective set, and it adds the converse equivalence with (50:20). The set is built from only, never from all of .
Welcome contributions: proofs of the §49 milestones, which form a small reusable library on winning and losing systems; a proof of (50:G) and (50:J); and lemmas connecting of a simple reduced game with the explicit formula (49:2), on and on .
Chapter VI of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; 3rd ed. 1953) opens the general theory of zero-sum games with more than two players. The authors propose to describe everything that can be said about coalitions, compensations between partners and fights between coalitions through one numerical object, the characteristic function : the amount a group of players can secure for itself against all the others (25.2.1). The whole later theory of the book (imputations, domination, solutions, simple games, decomposition) is built on this set function, and the same object, under the name "coalitional game" or "TU game", is the starting point of cooperative game theory as a field (cores, Shapley value, nucleolus).
§§25–27 settle two foundational questions about it. First, which set functions arise as characteristic functions of actual games? Second, which characteristic functions describe the same strategic situation, and how is a canonical representative chosen? The answers (a complete characterization by three conditions, and the reduced form under strategic equivalence) are what later chapters, and much of the cooperative literature, use when they take "a characteristic function" as a primitive without reference to any game.
A zero-sum -person game in normalized form (11.2.3, 25.1.3) has players . Player chooses a pure strategy , , uninformed about the others' choices, and then receives the real amount , subject to (25:1)
Let and, for , . The book defines in 25.1.3 through a fictitious two-person game: all players of form one composite player , all players of another, . The pure strategies of are the aggregates (one choice for each ), those of are the aggregates , and receives (25:2)
A mixed strategy of is a probability vector on the set of all aggregates , and one of is a probability vector on the aggregates . With ,
The coalition therefore randomizes jointly: is one distribution over its members' strategy tuples, not a product of independent mixtures. The empty set and are coalitions too (footnote 2, p. 241).
The three conditions of 25.3.1 on a set function are
From 26.2 on, every set function satisfying them is called a characteristic function.
Two such functions are strategically equivalent (27.1) if for numbers with ((27:1), (27:2)). A function is reduced if all one-element coalitions have the same value, (27:3); with that common value written , (27:5). A game is inessential if the reduced form of its characteristic function is , and essential otherwise (27.3).
The "only if" half is 25.3.1; the "if" half is 26.1.1, which requires a single game realizing on every coalition simultaneously.
The characterization makes the three conditions (25:3:a)–(25:3:c) the complete axiomatics of zero-sum characteristic functions. Every later result in the book that is stated "for a characteristic function" (the solutions of the three-person game in §32, the simple games of Chapter X, the decomposition theory of Chapter IX) is thereby a result about zero-sum games, and conversely no further constraint on is hidden in the game model. The reduced form of §27 cuts the parameter space of characteristic functions by and turns essentiality into a sign condition, which is used throughout the rest of the book.
These results are proved in the book. As far as a search of the Prove2Me catalog shows (queries on characteristic function, coalition, strategic equivalence, inessential, superadditive), none of them is formalized there; the existing cooperative-game definitions on the platform use other normalizations ( only, no complementarity condition) and are not this object. The mission produces a machine-checked link between the non-cooperative model of an -person game and the cooperative set function, including the book's explicit game construction behind 26.1.1.
The "only if" direction requires comparing values of different two-person games: (25:3:c) asks that the coalition can guarantee as much as and separately, which rests on the coalition mixing jointly, and (25:3:b) needs the minimax theorem, since is a Max-Min for the opposite side. The "if" direction is an existence claim: from an abstract one must produce one finite game whose characteristic function matches on all coalitions at once. Producing, for each separately, a game with the right value is easy and proves nothing. The §27 results are finite linear algebra over set functions, but the uniqueness in (27:A) and the boundary equalities in (27:7) depend on using all three conditions.
Players are Fin n (the book's are ), coalitions are Finset (Fin n), is the complement Sᶜ, and set functions are Finset (Fin n) → ℝ. A game is a structure ZeroSumGame n with strategy sets Fin (β k), a field β k > 0 (finitely many and at least one pure strategy per player), real payoffs H τ k, and the zero-sum condition (25:1) as a field. An aggregate is a dependent function on the members of ; mixed strategies are elements of Mathlib's stdSimplex, and the coalition's is a single distribution on aggregates, as in 25.1.3. The Max and Min in are written as ⨆/⨅ over the simplices; these are nonempty and the bilinear form is bounded on them, so no junk value arises. No lower bound on is imposed: the book's statements remain true for and , so dropping the implicit is a harmless strengthening.
Standing hypotheses instantiated in the statements: finiteness of the strategy sets and (25:1) (25.1.3) are part of ZeroSumGame; the §27 results carry (25:3:a)–(25:3:c) as a hypothesis, the book's standing assumption from 26.2 on ("characteristic function"); (27:7) carries reducedness (27:3) and the definition (27:5) of ; strategic equivalence includes (27:1). The reduced form is the explicit function of (27:2), (27:4), with as a real division that only matters for .
A trivializing reading of the goal, "for every there is a game with ", is excluded: the statement asks for one game with as functions. The coalition value is not the value under independent mixtures of the members, which is smaller in general and for which (25:3:c) can fail.
A complete development needs the minimax theorem for finite matrix games (the platform's AGT.zero_sum_minimax covers it for matrices indexed by Fin (m+1), and can be transported to the aggregate types), bookkeeping for splitting and joining strategy profiles along and , and the construction of 26.1 with its zero-sum check. The profile-splitting lemmas and the value facts for coalition games are reusable for the book's Chapter XI (general games) and for any work on coalitional values of strategic games. Contributions welcome: the §27 milestones, which are self-contained, and the two directions of the goal.
A zero-sum two-person game in normalized form is a real matrix : player 1 chooses a row , player 2 simultaneously chooses a column , and player 2 pays player 1 the amount . Matrix games are the base case of non-cooperative game theory, the prototype of every minimax statement in optimization, statistics (Wald's decision theory) and online learning, and, through their equivalence with linear programming, a standard tool of operations research.
Chapter III of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; third edition 1953) gives the book's complete solution of these games. Timeline:
Player 1 has pure strategies , player 2 has pure strategies , and is an arbitrary real matrix (14.1.1). A mixed strategy of player 1 is a probability vector in the simplex
and similarly for player 2. The pure strategy is the coordinate vector . The expected payoff is the bilinear form (17:2)
The good strategies of player 1 form the set of those at which assumes its maximum; those of player 2 form the set of those at which assumes its minimum ((17:B:a), (17:B:b)). A saddle point of is a pair with for all . With pure strategies alone one has and ; the game is specially strictly determined when .
For a general real function (§13) the same notions are , , saddle points, and the sets (maximizers of ) and (minimizers of ), always under the book's standing hypothesis that these maxima and minima exist.
For all and : and if and only if
The statement fixes no value and no constant; it says which pairs of mixed strategies are optimal.
AGT.zero_sum_minimax, proved).After the goal: (17:E) the game is specially strictly determined iff each player has a pure good strategy.
(17:D) is the complementary-slackness description of the optimal strategy pairs of a matrix game: a good strategy puts weight only on pure strategies that are best replies to the opponent's good strategy, and conversely any pair of mutually supported best replies is optimal. It is the basis of support-enumeration methods for matrix games, of the equalizing arguments used to solve small games by hand (the book's Chapter IV applies it to Matching Pennies, Stone–Paper–Scissors and Poker), and of the rectangular structure of the set of optimal pairs. (17:E) connects the mixed-strategy solution to the pure-strategy theory of §14 and to the perfect-information games of §15.
The results are classical and proved in the book. The minimax theorem itself is already machine-checked on the platform (AGT.zero_sum_minimax), and Mathlib contains Sion's minimax theorem and the basic saddle-point lemmas for extended-real functions on sets. This mission adds the book's own chain: the §13 saddle-point calculus under its standing attainment hypothesis, the theorems of the alternative (16:C) and (16:F) in the simplex-normalized form the book uses, the reduction (17:A) to pure strategies, and the characterizations (17:C:f), (17:D), (17:E) of good strategies, which are not on the platform in any form.
The "if" direction of (17:D) cannot be proved from the support conditions alone by local reasoning: that a pair of mutual best replies consists of good strategies uses that the value equals , i.e. the minimax theorem. Without that equality the "if" direction of (13:D*) fails (points of exist but are not saddle points), so the calculus of §13 alone does not suffice. Likewise (16:C) is not a direct instance of the Farkas lemma forms on the platform: its alternatives are normalized to the simplex and the second one is strict, and both the existence and the mutual exclusion must be shown.
Lean conventions, fixed throughout:
Fin β₁, Fin β₂ (numbered from ), the matrix is H : Fin β₁ → Fin β₂ → ℝ, and is Mathlib's stdSimplex ℝ (Fin β).0 < β₁, 0 < β₂, or mixed strategies , , which force it. The theorems of the alternative assume (a matrix with rows and columns).MaxMinAttained φ, which says that , , and are attained. (13:D*) also carries the hypothesis of 13.5.2 that saddle points exist, stated as .⨆, ⨅; they are the book's attained values under the hypotheses above (compactness of the simplex and continuity of for the mixed game). (17:A) asserts attainment explicitly (IsLeast, IsGreatest). "Does not assume its maximum at " in the goal is written without any Max operator.A trivializing formalization is ruled out: and are not taken as hypotheses or defined through the support conditions, strategy sets cannot be empty, and no Max over an empty or unbounded set occurs.
Contributions welcome: proofs of the milestones, especially (16:C) (from Mathlib's convex separation or from a platform Farkas lemma) and the bridge from AGT.zero_sum_minimax to (17:C:f). The §13 lemmas and the (17:A) reduction are reusable by any mission about matrix games or bilinear saddle points.
Game theory as von Neumann and Morgenstern built it measures every outcome by a single number, the utility a player attaches to it, and combines those numbers linearly when an outcome is uncertain: a lottery that yields with probability and with probability is worth . Every later chapter of Theory of Games and Economic Behavior uses this without comment, from the value of a zero-sum game to the characteristic function of a coalition. Section 3 of the book justifies it: it states axioms on preferences and on the combination of alternatives with probabilities, and claims that they force utility to be a number, unique up to the choice of a zero and a unit. The proof, announced in 3.6.1 as "somewhat lengthy", was added as the Appendix The Axiomatic Treatment of Utility in the second edition (1947).
The result, the expected utility theorem, is the foundation of decision theory under risk and of expected-payoff reasoning in game theory, statistics and operations research. The axiomatics were later recast by Marschak (1950), Herstein and Milnor (1953) in the language of mixture spaces (Herstein–Milnor). This mission formalizes the original statement and its original proof structure.
A system of utilities (3.6.1) is an abstract set of entities , together with
The axioms are:
All weights lie strictly between and , and is identity. The expression is notation for an abstract operation: carries no linear structure. The Appendix mostly writes the operation as , and writes for " or ". In the Lean development the system is the structure UtilitySystem U with fields gt and mix; S.cmb γ u v is .
A numerical utility (3.5.1) is a map with
For every system of utilities satisfying (3:A)–(3:C):
The constants are chosen before . No assumption on the size of is made.
The milestones follow the Appendix's own chain:
The theorem turns an ordinal preference over uncertain prospects into a cardinal scale on which expectation is meaningful. It is what licenses replacing a player's preferences by numerical payoffs whose mixtures are averaged, which the rest of the book, and most of game theory and stochastic optimization after it, assumes. The uniqueness part (A:W) states exactly how much freedom the scale has: a positive linear transformation, i.e. zero and unit may be fixed at will and nothing else.
The theorem has been proved many times since 1947, in textbooks and in the mixture-space literature, but the book's axiom system differs from the later ones (it uses a strict order with identity, strict monotony, and the two algebraic axioms (3:C) only). As far as the curators know, neither this axiom system nor the Appendix's derivation has a machine-checked proof, and Mathlib has no mixture-space or expected-utility module. The mission produces a checked proof of the original theorem under its original hypotheses and a reusable abstract mixture-space layer.
The obvious argument treats as a convex set and as a convex combination, then reads the utility off the segment between two reference points. None of that is available. The operation is formal, so identities that hold in a vector space, idempotence included, must be derived from (3:B) and (3:C) alone; only one associativity rule (3:C:b), for a repeated right argument, is given. The correspondence between a utility interval and a numerical interval requires the continuity axioms (3:B:c), (3:B:d) and the completeness of the reals. The local scales on different intervals have to be fitted into one global function, and the linearity for pairs and has to be recovered from the case .
Type*); the relation is gt : U → U → Prop and the operation mix : OpenUnit → U → U → U, where OpenUnit is the subtype of . mix α u v stands for . The operation is not defined at (3.6.1, footnote 4) and is not extended there.UtilitySystem. The items from (A:E) on assume fixed or as explicit hypotheses, as the book does "from now on until we get to (A:V) and (A:W)"; the goal does not, since (A:V), (A:W) hold for every .A complete development needs only order theory and the completeness of the reals from Mathlib. The mixture-space layer (the structure, (A:A)–(A:C), (A:T)) is reusable for any later work on expected utility, including the generalization in §66 and 67 of the book. Proofs of any milestone, alternative routes to the goal (for instance through the Herstein–Milnor axioms, once shown to follow from (3:A)–(3:C)), and statements of the omitted intermediate results (A:G)–(A:Q) are all welcome.
In a two-stage stochastic linear program a decision is taken before random data are observed, and a corrective recourse decision is taken afterwards at a cost. The objective contains the expectation of an optimal value of a linear program, , and for continuous or high-dimensional that integral cannot be evaluated exactly. Practical methods therefore replace by a discrete random vector and control the error by computable lower and upper bounds on the expected recourse cost. Chapter 2 of Ermoliev and Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), by P. Kall, A. Ruszczyński and K. Frauendorfer, surveys these bounds as they were used in the codes of the time: Jensen's inequality from below, the Edmundson–Madansky inequality from above, and the special structure of simple recourse, where the expected cost is available in closed form.
Timeline. Jensen's inequality (1906) gives the lower bound for a convex integrand. A. Madansky, "Bounds on the expectation of a convex function of a multivariate random variable", Ann. Math. Statist. 30 (1959), and H. P. Edmundson (RAND report, 1956) gave the upper bound by the two-point law on the endpoints of an interval, and its product version for independent components. Kall and Stoyan (1982), Huang, Ziemba and Ben-Tal (1977), Frauendorfer and Kall (1988) developed partition refinement of both bounds, the scheme this chapter describes; Frauendorfer (1988) extended the upper bound to dependent data on boxes.
The two-stage problem (2.11) is: minimize subject to , . The recourse cost is the optimal value of the second-stage problem (2.12),
with a deterministic matrix (fixed recourse), and when (2.12) is infeasible. Throughout the chapter the book assumes complete recourse, , and dual feasibility: for every realization of some satisfies . Under these assumptions is finite. The expected recourse function is .
The Edmundson–Madansky law of an interval , , with mean puts mass at and at (2.32). For a box and means , the vector with independent components of these two-point laws sits at the vertex with probability .
Simple recourse is the case , with , deterministic and random only. With the recourse cost splits into one-row costs if , and otherwise.
If has independent components with means , and is convex on , then
The book applies it to ; the goal is stated for every convex , with the explicit weights of (2.32).
The upper bound is the half of the bounding scheme that is not automatic. Jensen's inequality needs only a mean; an upper bound on the expectation of a convex function needs a bounded support and, in the product form, independence. Together they give a certified interval for the optimal value of a two-stage problem, and repeated partitioning of the support shrinks that interval; this is the basis of the sequential approximation methods of §2.2.4 and of later codes. The dual-multiplier bound and the simple-recourse formulas are the pieces that make those intervals cheap to compute.
The results are classical and proved in the literature cited on the page. The one-dimensional Edmundson–Madansky inequality and the general extreme-point form of the upper bound (a measure on the extreme points reproducing the barycentre) are already formalized on Prove2Me in the Introduction to Stochastic Programming series, as is the partition Jensen bound. The product form for independent components is not: deriving it from the extreme-point form requires constructing the product kernel, which is the content of this mission. The recourse properties (b), (d), (e) for a general distribution with finite second moments, the dual-multiplier bound and the simple-recourse formulas are not formalized anywhere known to this mission.
The obvious argument inducts on the dimension, applying the one-dimensional inequality in one coordinate while the others are held fixed. That step needs the conditional law of the remaining coordinates given the first to be their unconditional law, i.e. independence expressed as a product decomposition of the joint law, and it needs with one coordinate replaced by an endpoint to remain convex on the lower-dimensional box and integrable. For dependent components the inequality is false with these weights: on with means and , the product law gives while mass at and at gives . The book's remark that the product law is extremal among all laws on with the given mean fails for this reason when , and is not part of this mission.
For the recourse properties the difficulty is bookkeeping: is an extended-real optimal value, and finiteness, measurability in and integrability must be derived from complete recourse, dual feasibility and the moment hypothesis rather than assumed.
Vectors are functions from finite index types to (ι → ℝ), matrices are Mathlib Matrix, and random data live on a probability space (Ω, P). The recourse cost is an EReal infimum over the feasible set, so infeasibility gives and unboundedness exactly as on p. 39; theorems that integrate it carry complete recourse and dual feasibility, which make it finite. The expected recourse function integrates the real part of the recourse cost. Independence of the components is ProbabilityTheory.iIndepFun; the box is Set.pi univ (fun j => Icc (a j) (b j)), with , and values in the box are required almost surely. The upper bound is the explicit sum over Boolean vertex labels of products of the weights (2.32); no abstract extremal measure is used.
Conventions fixed where the page is silent or ambiguous:
recourseCost, expectedRecourse and dualLowerBound.A goal stated for affine (where it is an equality), or with allowed to be any discrete law with the right mean, would be trivial or a different theorem; the weights are the products of (2.32), and independence of the components is a hypothesis.
A complete development needs: finite-dimensional LP duality with extended-real values (reusable across all recourse missions), measurability and integrability of optimal-value functions, the conditional-independence step for product measures, and the one-dimensional chord inequality. The partitioned upper bound (2.37) and the discrete reformulation (2.21), (2.28) are natural follow-up statements on the same definitions.
A quantum-mechanical Hamiltonian is usually a sum of a kinetic energy (for a free particle, in units with , ) and a potential energy . Observables must be self-adjoint operators, not merely symmetric ones: only then does the spectral theorem apply and the time evolution exist as a unitary group. Self-adjointness of is usually a direct computation. For the sum it is not, because and are unbounded, and the sum of two self-adjoint unbounded operators need not be self-adjoint or even densely defined.
The Kato–Rellich theorem settles this when is small compared with in a precise sense. The result goes back to Rellich's perturbation theory of spectral decompositions (see the notes to Section V.4 of Kato's monograph), and Kato used it in 1951 (Trans. AMS 70, 195–211) to prove that atomic Hamiltonians with Coulomb interactions are self-adjoint. It is the standard first tool in the mathematical theory of Schrödinger operators. This mission formalizes Section 6.1 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009): the notion of relative boundedness, its characterizations, the theorem itself, and the second resolvent formula.
Let be a complex Hilbert space with inner product , conjugate-linear in the first slot. A linear operator is a linear map defined on a subspace , its domain. The sum is defined on . is symmetric if is dense and for . It is self-adjoint if it equals its adjoint , domains included, and essentially self-adjoint if its closure (the operator whose graph is the closure of the graph of ) is self-adjoint. is bounded from below by if for all .
The resolvent set is the set of for which is a bijection with bounded inverse , the resolvent.
An operator is bounded if and there are constants with
The -bound of is the infimum of the admissible . If is bounded, the product is defined on all of for .
Let be self-adjoint and symmetric with -bound less than one. Then
and if is bounded from below by and (6.1) holds with constants and , then
The printed form of (6.3) has where this statement has . The printed version is false: a two-dimensional example with , , has lowest eigenvalue of about . The corrected constant is the one in Kato's monograph (Theorem V.4.11). The lower bound is stated for every admissible pair , not for the -bound itself, which is an infimum and need not be attained.
Kato–Rellich is the entry point to self-adjointness of Schrödinger operators. With the Sobolev estimates of later chapters it gives self-adjointness of on for , which covers the hydrogen atom and, through the -body extension, every atom and molecule with Coulomb interactions. The lower bound (6.3) says the perturbed Hamiltonian is still bounded from below, which is the mathematical form of stability of the ground state. The second resolvent formula is used throughout perturbation theory: to compare spectra (Weyl's theorem on essential spectra), to study resolvent convergence, and in scattering theory.
In a formal library, relative boundedness is the shared layer on which every later statement about Schrödinger operators rests. Mathlib has unbounded operators (LinearPMap), their adjoints and closures, but no relative boundedness, no resolvent of an unbounded operator, and no perturbation theorem for self-adjointness. The theorem is textbook material and has been proved many times; what does not yet exist is a machine-checked proof for unbounded operators in this generality.
Self-adjointness of is a statement about the adjoint , whose domain is defined implicitly. The inclusion follows from symmetry, but the reverse inclusion does not come from any manipulation on . It requires knowing that certain ranges are all of , and that range information is not visible from the inequality (6.1) alone. Relating the -bound, an infimum over constants in an inequality on , to norms of the bounded operators is where the self-adjointness of enters. For the essentially self-adjoint case, the domains of three different closures have to be compared. For the lower bound, the constant depends on and in two regimes, and the printed version of the formula gets one regime wrong.
{H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is not assumed and not needed.LinearPMaps H →ₗ.[ℂ] H; is Mathlib's sum on the intersection of the domains; closures are LinearPMap.closure; self-adjointness is Mathlib's IsSelfAdjoint; symmetric operators include density of the domain.IsRelativelyBoundedWith A B a b contains the domain inclusion and . The -bound relativeBound A B is valued in and equals exactly when is not bounded, so "-bound less than one" cannot hold vacuously.spectrum is not used. resolvent A z is off , and statements use it only at points of or eventually along rays that lie in .opNorm) are valued in ; " is bounded" means everywhere defined with finite norm.A complete development needs basic facts about resolvents of self-adjoint operators ( and the norm estimates for ), the closed graph theorem for closable operators, and Neumann series. All of these are reusable in later missions of this series: Weyl's theorem, the free Schrödinger operator, atomic Hamiltonians. Contributions that build these as general LinearPMap lemmas are welcome.
Algorithmic mechanism design asks for algorithms whose inputs are held by self-interested parties. Each party reports its private data, the algorithm computes an outcome, and payments are arranged so that no party gains by misreporting. Nisan and Ronen introduced the field in Algorithmic Mechanism Design (Games Econ. Behav. 35, 2001). Their running example is task scheduling on unrelated machines: tasks are distributed among machines owned by different agents, each agent knows only its own processing times, and the designer wants to minimize the make-span.
Without incentives the problem is classical: minimizing make-span on unrelated machines is NP-hard and admits a polynomial 2-approximation (Lenstra, Shmoys, Tardos, 1990). With selfish agents the question changes: which approximation ratios can a truthful mechanism guarantee? This mission formalizes the paper's upper bound, the MinWork mechanism, which is the benchmark every later lower bound for truthful scheduling is compared with.
Timeline.
There are agents and tasks. Agent 's type is the vector of positive times, being the time agent needs to perform task . A type vector is . An allocation sends each task to one agent; is the set of tasks agent receives. The make-span of is
and agent 's valuation is .
A direct mechanism asks every agent to declare a type, computes an allocation from the declared vector , and hands agent a payment . Agent 's utility is , with its true type. The mechanism is truthful if declaring maximizes agent 's utility for every declaration of the others, and strongly truthful if truth-telling is the only such dominant strategy. An allocation rule is a -approximation if for every type vector and every allocation .
The MinWork mechanism allocates each task to an agent with minimal declared time for it, breaking ties arbitrarily. For each task it wins, an agent receives the second-best declared time :
The Lean development uses the same names: load, makespan, IsTruthful, IsStronglyTruthful, IsApprox, IsMinWorkAlloc, secondBest, minTime, minWorkPay.
For and every MinWork allocation rule with payments as above,
The theorem gives the first positive result for truthful scheduling: a mechanism that is truthful in the strongest sense and is within a factor of optimal, whatever the tie-breaking rule. Every lower bound in the paper (Theorems 4.6, 4.10 and 4.12) and in the later literature measures itself against this ratio. Since the 2023 resolution of the Nisan–Ronen conjecture, the ratio is known to be tight for deterministic truthful mechanisms.
The result is proved in the paper; it is not known to be formalized in any proof assistant. The platform already has Groves' theorem in an abstract form (AGT.vcg_incentive_compatible). This mission connects that abstract statement to a concrete combinatorial mechanism, and it adds the strict part of strong truthfulness for any number of tasks and agents, which the paper proves only for one task and two agents. The vocabulary (make-span over unrelated machines, direct scheduling mechanisms, strong truthfulness) is shared with the seven later missions of this series.
Truthfulness follows from Groves' theorem once MinWork is identified as a VGC mechanism. The identification requires the payment identity at every declared vector and under every tie-breaking rule, including ties at the winning time. The main difficulty is the strict part of strong truthfulness. A misreport that differs from the truth only on one task must still be shown to lose strictly for some declarations of the others. Those declarations must stay positive, and on every other task they must leave the outcome unchanged. The paper's proof covers only one task and two agents and leaves the general case as "similar". Its printed inequality also has the two utilities in the wrong order (see below), so it cannot be transcribed directly.
Fin n and tasks are Fin k. An allocation is a function Fin k → Fin n, and an agent may receive no task. Types are positive reals, and every truthfulness and approximation quantifier ranges over positive true types, positive misreports and positive declarations of the others.IsMinWorkAlloc). Every result holds for every tie-breaking rule, including rules that depend on the whole declared vector. No particular argmin is fixed.Finset.sup' / Finset.inf' over nonempty finite sets, so they are true maxima and minima with no default values.AGT.vcg_incentive_compatible.Hilbert's Nullstellensatz ("theorem of zeros") is the basic link between algebra and geometry. It was proved by David Hilbert in his second major paper on invariant theory in 1893, after his 1890 paper that proved the basis theorem, and it is a foundational result of algebraic geometry. It gives an algebraic criterion for when a system of polynomial equations over an algebraically closed field has a solution, and an algebraic criterion for when one polynomial vanishes wherever a given family does. Every dictionary between affine varieties and ideals — points and maximal ideals, algebraic sets and radical ideals, irreducible sets and prime ideals — is a consequence.
This mission follows the Wikipedia article Hilbert's Nullstellensatz (snapshot of 27 September 2026): its introduction, its section Formulations, the statement of Zariski's lemma from Proofs, and the first theorem of Generalizations (finitely generated algebras over Jacobson rings).
Let be a field and an algebraically closed field extension of (every non-constant polynomial over has a root in ). Write for the polynomial ring in variables. A point is an -tuple , and is the value of a polynomial at .
If vanishes on , then
This is the statement of the article's section Formulations, with the coefficient field and the algebraically closed field allowed to differ.
The Nullstellensatz makes the zero sets of polynomial systems accessible through ideals: solvability of a system becomes the ideal-membership question , and the geometry of algebraic sets becomes the algebra of radical ideals. Consequences include the identification of the points of with the maximal ideals of , the description of irreducible algebraic sets by prime ideals, and the reduction of the fundamental theorem of algebra to the case . The Jacobson-ring version extends the first equality of the intersection formula to every finitely generated algebra over a field.
All statements here are classical and proved. Mathlib already contains versions of several of them in its own vocabulary (Jacobson rings, Zariski's lemma, and a Nullstellensatz over an algebraically closed coefficient field). What this mission adds is a single set of statements matching the article's formulations: the version with separate fields , the explicit systems-of-equations form, the point-ideal and irreducibility correspondences over , and the intersection formula — and, for solvers, the bridges from these concrete statements to Mathlib's abstract ones.
The inclusion is immediate; the content is the reverse inclusion, which requires producing a point of from purely algebraic data. When the ideal lives over while the points live over , so a result stated only for does not apply directly: an ideal of must be related to the ideal it generates in without losing membership information. For the correspondences, the explicit ideals and the closed-set definition of irreducibility must be matched with the abstract notions (maximal spectrum, irreducible closed subsets) used in the library.
MvPolynomial (Fin n) k. When , is a -algebra and evaluation of a polynomial over at a point of goes through .Polynomial.degree, with .MvPolynomial.zeroLocus, MvPolynomial.vanishingIdeal, and IsJacobsonRing.Column generation solves linear programs with far too many variables to list: one works with a small subset of the columns, the restricted master problem (RMP), and adds columns of negative reduced cost as a pricing problem finds them (Lübbecke and Desrosiers 2005, §2.1). Many integer programs from vehicle routing, crew scheduling and crew pairing are reformulated so that the master problem is a set-partitioning problem: every row (a customer, a flight leg, a task) must be covered by exactly one selected column (a route, a pairing, a schedule). The linear relaxation of such a master is solved by column generation, and an integer solution is then sought by branch-and-price, branch-and-bound with column generation at every node.
Branching in branch-and-price is not free. Fixing a master variable to does not stop the pricing problem from regenerating the same column, and handling that complicates the pricing problem. The rule that avoids this for set partitioning goes back to Ryan and Foster (1981): branch on a pair of rows, requiring them to be covered either by the same column or by two different columns. Both requirements are constraints the pricing problem can respect directly. Lübbecke and Desrosiers call it "the most common scheme in conjunction with column generation" (§7.3, p. 1020) and state the proposition that makes it well defined as their Proposition 3.
Timeline:
Rows are indexed by and columns by a finite set . A matrix has every entry equal to or ; column covers row when . The set-partitioning system of the RMP's linear relaxation is
A vector is a basic feasible solution of this system when it satisfies all its constraints and, among the constraints active at (the equality rows, and the constraints with ), there are linearly independent ones. Equivalently, is feasible and the columns of in the support of are linearly independent. A solution is fractional when it is not a vector, .
For two rows the Ryan–Foster quantity is , written pairCover A lam r s in Lean: the total weight on the columns that cover both rows. For it is the row sum, equal to on every feasible .
For every matrix and every fractional basic feasible solution of , ,
The two rows are automatically distinct. The statement concerns every fractional basic solution, not only an optimal one, and no cost vector enters it.
For every solution of and every pair of rows ,
This is the paper's requirement that "integer solutions remain intact" (p. 1019), specialised to the two branches "" and "" of the paragraph after Proposition 3.
Proposition 3 is what makes Ryan–Foster branching a valid branching scheme in the sense of §7.3: the current fractional solution violates both branches for the chosen pair, so it is excluded from both children, while by the milestone every integer solution survives in one of them. The same pair-of-rows idea underlies branching in bin packing, graph colouring, vehicle routing and crew scheduling codes, where it is used because both branches translate into constraints on the pricing problem rather than on individual master variables.
The paper states the result and refers its proof to Ryan and Foster (1981); no machine-checked version of the proposition is known. This mission produces a formal statement tied to a standard, representation-aware definition of basic solutions (Bertsimas–Tsitsiklis Definition 2.9, already on the platform) and, once proved, a verified lemma that any formal development of branch-and-price for set partitioning can cite.
An argument that uses only feasibility and a fractional coordinate cannot work. Without basicness the claim is false: with one row and two identical columns, , the vector is feasible and fractional, yet the only pair of rows is , whose quantity is . The difficulty is to turn basicness, a linear-algebra condition, into a combinatorial statement about which rows the fractional columns cover. A set-partitioning matrix need not have full row rank, so the familiar description of basic solutions through an invertible basis matrix is not available in general.
Fin m and columns Fin n, so is identified with . is a real matrix Matrix (Fin m) (Fin n) ℝ with the hypothesis IsZeroOneMatrix A (every entry or ); is lam : Fin n → ℝ, since λ is a Lean keyword. Columns are vectors; the equivalent reading as subsets of the rows is only prose.LinearOptimization.IsBasicFeasibleSolution (LinearOptimization.stdFormSystem A (fun _ => 1)) lam, from the platform definitions BasicSolution and ActiveConstraints. This definition needs no full-row-rank assumption, which a set-partitioning matrix need not satisfy, and it is not replaced by an ad hoc support condition.¬ IsZeroOneVector lam.A complete development needs linear-algebra facts about basic solutions of standard-form systems without a rank assumption (support columns linearly independent), which are reusable beyond this mission. Contributions welcome: that characterization as a lemma, and proofs of the milestone and of the goal.
Linear systems of ordinary differential equations are the first case of the general theory in which solutions can be described structurally rather than merely shown to exist. They arise directly (circuits, mechanical vibrations, Hill's equation for the stability of periodic motions, the Mathieu equation for parametric resonance) and indirectly, as the linearization of a nonlinear system along an equilibrium or a periodic orbit. In the second role they decide stability: the linearized stability theorems of later chapters, the Poincaré map of a periodic orbit and the stable-manifold theory all reduce questions about nonlinear flows to questions about linear systems with constant or periodic coefficients.
For periodic coefficients the central structural result is due to Gaston Floquet (Sur les équations différentielles linéaires à coefficients périodiques, Annales scientifiques de l'École Normale Supérieure 12 (1883), 47–88, doi:10.24033/asens.220), preceded by G. W. Hill's 1877 work on the lunar perigee, which studied the same equation in the scalar second-order case. Liouville's formula for the Wronski determinant goes back to Abel (1829) and Liouville (1838). This mission follows Chapter 3 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012), in the author's preliminary version.
Fix , an interval and a continuous matrix function . A solution of the linear first-order system
on is a function with values in that at every has derivative (one-sided at an endpoint of ). In Lean this is TeschlODE.Linear.IsSolution A I x.
The principal matrix solution is, for each , the matrix function that solves the matrix initial value problem
Its columns are the solutions of (3.79) starting at the canonical basis vectors, and every solution is . In Lean the property is TeschlODE.Linear.IsPrincipalMatrixSolution A I Φ (the Lean name of is Φ). The Wronski determinant of solutions is .
A system is periodic if and for all , for some (3.117). Its monodromy matrix is (3.119). A logarithm of a square matrix is any matrix with (3.200), where is the matrix exponential.
Let be -periodic with and its principal matrix solution. For every there exist and with
In attack order:
Milestone 6 is not needed for the goal; it completes the linear theory of Section 3.4 on the same definitions and is the input to the perturbation results of Section 3.7.
Floquet's theorem reduces a periodic linear system to one with constant coefficients by a periodic change of variables. Its consequences in the book are the real version with doubled period (Corollary 3.16), the stability criterion in terms of Floquet multipliers (the eigenvalues of , Corollary 3.17), the reduction to (Corollary 3.18), and the stability analysis of Hill's equation. Later in the book, the stability of a periodic orbit of a nonlinear system is read off from the Floquet multipliers of its linearization, via the Poincaré map.
All results of this mission have been proved for more than a century. What the mission adds is a machine-checked development: Mathlib has the matrix exponential (NormedSpace.exp, with Matrix.exp_add_of_commute), Picard–Lindelöf and Gronwall-type uniqueness for ODEs, but no principal matrix solution, no Liouville formula, no matrix logarithm and no Floquet theory. The two platform nodes named after Floquet's and Liouville's theorems are retired placeholders whose statement is True; no faithful formalization exists on the platform.
The obvious guess for the solution, , is wrong as soon as the values do not commute, so neither Floquet's theorem nor the variation-of-constants formula can be obtained from the constant-coefficient theory by substitution. Floquet's theorem as stated is equivalent to the existence of a logarithm of the monodromy matrix: once is available, the periodicity of follows from Lemma 3.14. The existence of a matrix logarithm for every invertible complex matrix is the main missing piece of infrastructure; the logarithm is not unique and not continuous in the matrix, and a real invertible matrix need not have a real logarithm (a negative eigenvalue with a single Jordan block prevents it), which is why is complex. Liouville's formula, which gives , needs the derivative of a determinant along a matrix solution.
Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ; is Matrix.mulVec. The goal and Lemma 3.34 use Matrix (Fin n) (Fin n) ℂ for , and the complex logarithm; is compared with after coercing its entries to .Set.OrdConnected I; continuity is ContinuousOn A I. Derivatives are HasDerivWithinAt … I t at every (one-sided at endpoints in ); the matrix derivative in (3.83) is taken entrywise. In Section 3.6 (Lemma 3.14 and the goal) and is Continuous.IsPrincipalMatrixSolution A Set.univ Φ. Theorem 3.10 shows such a exists and Theorem 3.9 shows it is unique on , so this hypothesis names the principal matrix solution, not an arbitrary function.0 < T and ∀ t, A (t + T) = A t. The periodicity of is required with the same and for all , together with . Without the periodicity of the goal would be trivial (, ); with it, the goal carries the full content of the theorem.NormedSpace.exp. "Logarithm" means any with NormedSpace.exp B = M; no branch is fixed. In the third claim of Lemma 3.34 the hypothesis is explicit: the book states it in the paragraph containing the lemma, and without it the claim fails at .In quantum mechanics an observable is a self-adjoint operator on a complex Hilbert space . Physics, however, usually hands over a symmetric operator: a differential expression such as or on a convenient domain of smooth functions, on which integration by parts shows . Symmetry is easy to check and self-adjointness is not. Two questions then decide whether the formal expression defines a physical theory: does have a self-adjoint extension at all, and if so, how many? Different extensions correspond to different boundary conditions and to different dynamics (via Stone's theorem), so the answer is physically meaningful.
John von Neumann answered both questions in 1929–1930 with the Cayley transform and the defect indices (von Neumann 1930). His criterion is the goal of this mission, in the form given in Chapter 2 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS Graduate Studies in Mathematics 99, 2009), from which every statement of the mission is taken.
Let be a complex Hilbert space with inner product , conjugate-linear in the first argument. A linear operator is a linear map defined on a linear subspace , its domain. An operator extends , written , if and for .
is symmetric if is dense and for all . For densely defined the adjoint has domain and acts by . is self-adjoint if , domains included, and essentially self-adjoint if its closure (the operator whose graph is the closure of the graph of ) is self-adjoint.
For , is the operator on . The resolvent set is the set of for which is a bijection with bounded inverse , and the spectrum is .
For symmetric the defect spaces and defect indices are
where is the Hilbert dimension (the cardinality of an orthonormal basis, possibly infinite). The Cayley transform of is
For every symmetric operator ,
In the order of the book:
The criterion is the standard tool for deciding whether a formal Hamiltonian is a legitimate observable, and for classifying its realizations: by the parametrization (2.103)–(2.104), the self-adjoint extensions correspond to the unitary maps . Theorem 2.28 turns the criterion into a practical test, since every real differential operator, for example a Schrödinger operator with real potential, is -real for complex conjugation and therefore has self-adjoint extensions. Lemma 2.7 and Theorem 2.18 are the everyday criteria for self-adjointness and the basic spectral facts on which Chapters 3–6 of the book rest. The Friedrichs extension, Weyl's limit point/limit circle theory and the Kato–Rellich theorem all refine these statements.
All of these results are classical and proved in every text on unbounded operators (for example Schmüdgen 2012, Chapters 3 and 13). None is formalized in Mathlib, which provides the adjoint, closure and self-adjointness of a LinearPMap but no resolvent set, spectrum, Cayley transform or defect theory for unbounded operators. The platform's existing material on essential self-adjointness is stated for specific Hamiltonians on bespoke structures, not for general operators. A formal proof here supplies the unbounded-operator layer that every later mission in this series (spectral theorem, Kato–Rellich, Weyl's theorem, Sturm–Liouville theory) restates.
The obvious reduction, "a self-adjoint extension is a unitary extension of the Cayley transform, and a unitary exists iff the dimensions agree", hides most of the work. The correspondence between extensions of and extensions of runs through the inverse Cayley transform , which requires injectivity of and careful bookkeeping of partial domains. Extending an isometry to a unitary requires passing to closures of when is not closed. Equal Hilbert dimension must be converted into an actual unitary between the defect spaces. Theorem 2.18 needs the self-adjointness criterion of Lemma 2.7 in the direction "spectrum real implies self-adjoint", where the range conditions come from the resolvent set rather than from symmetry. Each of these steps is routine on paper and requires explicit domain management in Lean.
Operators are Mathlib LinearPMaps H →ₗ.[ℂ] H on a complex Hilbert space (InnerProductSpace ℂ H, CompleteSpace H). Separability, part of the book's standing assumption, is not needed by any statement and is not assumed. Extension is the order A ≤ B. Self-adjointness is Mathlib's IsSelfAdjoint (equality with LinearPMap.adjoint), and symmetry includes density of the domain, so every adjoint in the mission is taken of a densely defined operator and is the book's . The closure is LinearPMap.closure; closedness is LinearPMap.IsClosed.
The mission uses the series' shared definitions TeschlQM.Shared.IsSymmetric, TeschlQM.Shared.IsEssentiallySelfAdjoint and TeschlQM.Shared.IsResolventAt, resolventSet, spectrum, and defines, in the namespace TeschlQM.SelfAdjoint: addScalar, rangeAdd, kerAdd for , , ; IsCayleyTransform, IsIsometric, rangeOneSub; defectPlus, defectMinus, HasEqualDefectIndices; IsConjugation, IsCReal. Nothing that the book derives is taken as data: the Cayley transform is a relation that determines from , and its existence and uniqueness are part of Theorem 2.25.
Conventions that matter:
spectrum. For a non-closed operator this makes .K₊ ≃ₗᵢ[ℂ] K₋, which is equivalent to equality of Hilbert dimensions. Reading "self-adjoint extension" with the order reversed, or taking as kernels of (which are trivial for symmetric ), would make the goal trivial; neither is used.Reusable parts: the resolvent/spectrum layer and the Cayley transform are needed throughout the rest of the book. Proofs of any milestone, and API lemmas about rangeAdd, kerAdd and adjoints (such as and the reversal ), are welcome.
Many optimization problems in engineering, simulation-based design and machine learning give access only to function values: the objective is the output of a simulator or a black-box program, and its gradient is unavailable or too expensive. Derivative-free (or zeroth-order) methods address this setting. Nesterov and Spokoiny (Found. Comput. Math. 17 (2017)) showed that a very simple oracle, the finite difference of along a random Gaussian direction, can replace the gradient in standard first-order schemes at the price of a factor depending only on the dimension. Their analysis became the reference point for later work on zeroth-order stochastic optimization and on gradient-free methods in reinforcement learning and adversarial attacks.
This mission covers Section 6 of the paper: the accelerated random method and its rate, Theorem 9. It is the third mission of a series; the first covers random search for nonsmooth problems (Theorem 6), the second the random gradient method for smooth problems (Theorem 8).
Let be a real inner product space of dimension with norm (the paper's space with operator is with the inner product ). Let be a standard Gaussian vector in , and write for expectation over .
The objective is differentiable with Lipschitz gradient, with , and strongly convex with parameter :
The value is allowed (plain convexity). The condition number is . The problem is assumed solvable, with minimizer .
For the Gaussian approximation is , and the random gradient-free oracle is
The paper (p. 548) sets and . This mission uses ; the reason is given under Formalization scope. Method (Eq. (60)) chooses , and with , and at every iteration :
Write (expectation over ), and for , with and (p. 550).
For all ,
where
The two regimes are a rate for convex and a linear rate with ratio for strongly convex , both up to a bias proportional to .
In attack order: Lemma 1 (Gaussian moments, (16)–(17)); Theorem 3.1 (the bound (32) on the second moment of ); Theorem 1's (19), ; Eq. (12), ; Lemma 5, the bound (37) on in terms of ; Eq. (21), ; and Eq. (11), for convex .
Theorem 9 shows that the -fold slowdown of gradient-free methods relative to their gradient counterparts survives acceleration: reaches accuracy in iterations for convex , against for the non-accelerated random gradient method. The analysis also quantifies how small the finite-difference step must be for this to hold. The result is used as the baseline accelerated zeroth-order rate in later work.
The theorem is proved in the paper. As far as is known it has not been machine-checked, and Mathlib has no Gaussian smoothing, no random gradient-free oracle and no analysis of an accelerated method driven by random directions. A formal proof also settles the constant question raised by the printed (see below).
The deterministic fast gradient method is analysed by an estimate-sequence argument in which the gradient step is exact. Here the step uses , which is an unbiased estimate of and not of , and whose second moment is of order plus a bias term. The step size and the coupling parameter must absorb this second moment, and the argument must be run for rather than . The estimate sequence then has to be passed through expectations over the history , which requires the independence of from and integrability of every quantity involved. Transporting the result from back to uses (11) and (19), and requires that inherits strong convexity with the same parameter , a fact the paper uses without stating it.
is an arbitrary finite-dimensional real inner product space (InnerProductSpace ℝ E, FiniteDimensional ℝ E, Borel measurable), is Module.finrank ℝ E, and the Gaussian is Mathlib's stdGaussian E. The operator is absorbed into the inner product, so is gradient f and is . This is not a restriction to on . All expectations are Bochner integrals; under the hypotheses every integrand is integrable, so no integrability hypothesis is added.
The run is a structure over a probability space : directions that are measurable, mutually independent (iIndepFun) and standard Gaussian; deterministic sequences satisfying step a) as equations; and random points satisfying steps b)–d) for every outcome. The smoothing parameter satisfies , and at the oracle is . The goal pins and . and are definitions computed from .
The constant . The paper prints . The proof (pp. 549–550) needs , and , which hold only with . With the printed value is larger than the first inequality allows, and the argument does not go through. The mission therefore states Theorem 9 with ; all other constants are as printed.
Two trivializing formalizations are ruled out. First, the bound carries the hypothesis : at the paper's value is , while Lean's division by zero would turn it into , which is false. and are definitions from the run, not free variables that only satisfy the bounds. Second, the oracle is the random finite difference along i.i.d. standard Gaussian directions, not the exact gradient (which would give Nesterov's deterministic method) and not an arbitrary direction sequence.
A complete development needs Gaussian integration by parts in an inner product space, moment bounds for , differentiation under the integral sign for , and conditional expectation along an i.i.d. sequence. The smoothing layer (Lemma 1, (11), (12), (19), (21), (32), (37)) is reusable for any zeroth-order method, and contributions of these components as separate lemmas are welcome.
Many optimization problems in engineering, simulation-based design and machine learning give access to the objective only through its values: the function is computed by a black-box code, and derivatives are unavailable or too expensive to program. Zeroth-order (derivative-free) methods address this setting. Classical derivative-free methods (pattern search, Nelder–Mead, model-based trust regions) come with weak or no global complexity guarantees for convex problems.
Nesterov and Spokoiny (Found. Comput. Math. 17 (2017) 527–566) showed that replacing the gradient by a finite difference along a random Gaussian direction yields methods whose expected complexity is that of the corresponding gradient method multiplied by a factor proportional to the dimension. Their paper is a standard reference for zeroth-order convex optimization and for Gaussian smoothing, and its oracle and analysis are reused in bandit convex optimization, zeroth-order stochastic optimization (e.g. Ghadimi–Lan 2013) and derivative-free reinforcement learning.
This mission concerns Section 5 of the paper: the random gradient method for smooth convex functions and its linear rate for strongly convex ones.
Let be a real inner product space of finite dimension , with norm . (The paper works with a space carrying an operator and norm ; choosing as the inner product gives exactly this setting, and the dual norm becomes the norm of the Riesz representative.)
A function belongs to with constant if it is differentiable and for all . It is strongly convex with parameter if for all .
Let be a standard Gaussian vector of (coordinates in any orthonormal basis are independent ). The Gaussian approximation of with parameter is , and the moments are . The random gradient-free oracle returns, for a sampled direction ,
and the symmetric oracle is .
Consider for a convex , assumed solvable with a minimizer , and . The random gradient method (Eq. (54), p. 546) is:
Method : Choose . Iteration . a). Generate and corresponding . b). Compute .
The directions are independent standard Gaussian vectors, and (with ).
With step size and any , for every ,
and, if is strongly convex with parameter , then with ,
Both bounds are one theorem with one proof in the paper, so the goal states their conjunction, with every constant as printed.
The milestones are the results the paper's proof of Theorem 8 rests on, in attack order:
The result. Theorem 8 shows that a method using two function values per iteration reaches accuracy on a smooth convex problem in iterations, and in iterations under strong convexity, provided is small enough. This is times the complexity of the deterministic gradient method, which is the natural price for replacing an -dimensional gradient by one directional estimate. The strongly convex bound makes explicit the bias floor caused by the finite-difference step, and shows that it vanishes for the limiting method .
Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of it has a machine-checked proof. A formalization produces a reusable Gaussian-smoothing layer on Mathlib's stdGaussian (moments of the Gaussian norm, differentiation of under the integral, variance bounds of random oracles) and a complete expected-complexity proof of a randomized first-order method, in which the probabilistic structure (independent directions, iterates depending only on past directions, tower property) has to be handled explicitly.
The deterministic part of the argument is the textbook analysis of gradient descent. The difficulty is in the Gaussian facts it uses. The obvious bound on the oracle's second moment, , loses a factor of and would give a quadratic dependence on dimension; the of (32) needs a sharper computation. The moment bounds of Lemma 1 for non-integer and the differentiation under the integral in (21) are measure-theoretic steps that Mathlib does not package. Finally, the step from per-iteration inequalities to bounds on requires conditioning on the past directions, which must be set up on a probability space carrying the whole sequence .
is an arbitrary finite-dimensional real inner product space with MeasurableSpace and BorelSpace, is Module.finrank ℝ E, and is Mathlib's gradient. Expectations over are Bochner integrals against ProbabilityTheory.stdGaussian E. A run of lives on a probability space : measurable directions , jointly independent (iIndepFun) with law stdGaussian E, iterates with deterministic and the update holding for every and outcome. is ∫ ω, f (x k ω) ∂P. The oracle is defined by cases, with at ( the one-sided directional derivative of Eq. (23), a Filter.limUnder, which equals fderiv ℝ f x u for differentiable ), so the goal covers every as the paper claims. and are any constants satisfying the defining inequalities. The standing assumptions of Section 5 (convexity, a global minimizer , ) and are explicit hypotheses; is needed for the constant .
A trivializing formalization is ruled out: the oracle is the random finite difference along i.i.d. standard Gaussian directions, not the true gradient (which would be deterministic gradient descent), and every expectation in the statements is of a quantity that is integrable under the stated hypotheses, so no bound holds through a junk value of a non-integrable integral.
A complete development needs Gaussian moment computations in finite dimension, differentiation under the integral sign for , the variance bounds of the oracles, and a conditional-expectation argument for the iteration. The smoothing layer is reusable for the companion missions on random search for nonsmooth problems and on the accelerated random method, and for other zeroth-order methods. Contributions of any of the milestones, of general Gaussian-integrability lemmas, or of alternative proofs are welcome.
Many optimization problems in engineering, simulation-based design and machine learning give access to the values of an objective function but not to its gradient: the function is computed by a black-box program, by a simulator, or by a model whose derivatives are unavailable or too expensive. Zeroth-order (or derivative-free) methods use only function values. Classical direct-search methods of this kind usually come without complexity bounds.
Nesterov and Spokoiny (Found. Comput. Math. 17 (2017) 527–566) showed that a very simple randomized scheme has explicit, dimension-dependent worst-case complexity bounds. The idea is to replace the gradient by a finite difference of along a random Gaussian direction. The resulting oracle is an unbiased estimate of the gradient of a smoothed version of . Their analysis is the reference point for the later literature on zeroth-order stochastic optimization, bandit convex optimization and gradient-free training.
This mission covers the paper's result for nonsmooth convex problems over a closed convex set: the projected random search method and its convergence bound, Theorem 6.
Let be a real inner product space of finite dimension , with norm . (The paper works with a space carrying a positive definite operator and the norm . This is the same thing as an arbitrary finite-dimensional inner product space, with encoding the inner product, and the development is written in that generality.)
A function is Lipschitz continuous with constant if for all . The paper calls this class and writes for the constant.
Let be a standard Gaussian vector in : its coordinates in any orthonormal basis are independent variables. For the Gaussian smoothing of is
and the Gaussian moments are .
For the random gradient-free oracle at draws and returns the vector
It costs two function values.
The problem is
where is closed and convex, is convex and Lipschitz, and is a minimizer. With the Euclidean projection onto , positive steps and a starting point , the random search method iterates
drawing a fresh independent Gaussian direction at every iteration. The iterates are random. Write and .
For every ,
The step sizes, the smoothing parameter and the horizon are left free, so every step-size rule in the paper follows from this one inequality. The constants are the paper's.
The facts about smoothing and the oracle on which the goal rests, in the paper's order:
Theorem 6 shows that a method using only function values, with no subgradient, solves nonsmooth convex problems with the classical projected-subgradient guarantee. Two things change: is multiplied by , and a bias appears, which can be made as small as desired. With suitable , and an -accurate expected value is reached in oracle calls. The factor quantifies the cost of not having gradients. The same analysis carries over to stochastic objectives (the paper's Theorem 7).
The results are proved in the paper. As far as is known, none of them has a machine-checked proof. The mission produces a Lean development of Gaussian smoothing on an arbitrary finite-dimensional inner product space: the moment bounds, the approximation, convexity and gradient identities, and the oracle variance bound. On top of it sits the full convergence theorem for a randomized projected method, stated for the actual random process rather than for an idealized expectation recursion. The smoothing layer is reusable: the same facts underlie the smooth and accelerated random methods of the same paper and most Gaussian-smoothing analyses in zeroth-order optimization.
A plain subgradient analysis does not apply. The vector is not a subgradient of , nor an unbiased estimate of one. It is an unbiased estimate of the gradient of a different function, , and its second moment grows with the dimension. The argument therefore has to move between and at exactly the right places, using properties of that hold for every nonsmooth Lipschitz .
Those properties are genuinely analytic. Differentiating requires differentiating a Gaussian integral of a function that need not be differentiable. The moment bounds need estimates of for real . In the probabilistic part, depends on , and each one-step estimate has to be integrated using the independence of from the past. Mathlib provides the standard Gaussian measure and independence, but no Gaussian smoothing, no projection onto convex sets and no conditional-expectation argument for this kind of recursion.
The space is E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E], and is Module.finrank ℝ E. No lower bound on is assumed. The Gaussian is ProbabilityTheory.stdGaussian E, and expectations are Bochner integrals against it. is the definition smoothing, is moment (with real exponent Real.rpow), and is oracle.
The projection is the relation IsMetricProjection Q y z ( and is a nearest point of to ). The run is the predicate IsRandomSearchRun: directions on a probability space , measurable, mutually independent (iIndepFun) and each with law stdGaussian E; a deterministic ; and the update above for every and every outcome.
is . The Lipschitz constant is any constant satisfying the Lipschitz inequality. It is an explicit hypothesis, because the paper's bound uses , which presupposes . The smoothing parameter satisfies and every step satisfies .
Two trivializing formalizations are ruled out. First, an expectation of a non-integrable function would be as a Bochner integral; Lipschitz continuity of makes every expectation in the mission integrable, and no statement relies on the junk value. Second, a run whose directions are not independent standard Gaussians, or whose update uses a subgradient instead of the finite difference, is a different theorem (the projected subgradient method). The run predicate fixes the paper's process exactly. A run exists for every closed containing (on the countable product of Gaussians), so the goal is not vacuous.
A complete development needs:
The smoothing lemmas, the moment bounds and the projection facts are reusable beyond this mission. Contributions are welcome at every level: proofs of the milestones, general lemmas about stdGaussian and projections, and alternative proofs of Lemma 1 (for example through the chi distribution).
Almost every existence theory for elliptic, parabolic and hyperbolic partial differential equations works in Sobolev spaces: function spaces defined through weak derivatives and integrability rather than classical differentiability. Energy methods produce solutions whose derivatives are known only to be square-integrable. Sobolev embedding theorems are what turn that information back into integrability or continuity of the solution itself, and they are used at every step of the regularity theory.
This mission covers Chapter 3, §3.1–3.8 of J. K. Hunter's graduate lecture notes Notes on Partial Differential Equations (UC Davis, revised 6/18/2014): weak derivatives, the spaces , approximation by test functions, and the two embedding regimes and .
Timeline. S. L. Sobolev proved the embedding for in 1938 by potential-theoretic methods. E. Gagliardo (1958) and L. Nirenberg (1959) independently gave the elementary proof, including , that the notes follow. The inequality behind it, for products of functions of variables, is also known as the Loomis–Whitney inequality (1949). C. B. Morrey (1940) proved the Hölder estimate for . The sharp constants were found by Federer–Fleming and Maz'ya (1960, , equivalent to the isoperimetric inequality) and by G. Talenti (1976, ).
Throughout, carries Lebesgue measure and the Euclidean norm , and is open. A test function is infinitely differentiable, and its support is a compact subset of . For a multi-index with , .
A locally integrable has weak derivative if
The Sobolev space , for and , consists of the whose weak derivatives , , exist and lie in . It is normed by , with the maximum of the suprema when .
For the Sobolev conjugate is , so that . For , is the gradient, its Euclidean length, and . The Hölder seminorm is .
For , and every ,
The goal's constant is explicit, and it is not the sharp one. A later sharp constant (Talenti's) would strengthen the goal but would not invalidate it.
The result. Theorem 3.28 is the quantitative core of the embedding . Density (Theorem 3.24) extends it to all of , giving Theorem 3.31. From there, extension operators and Rellich–Kondrachov compactness follow, and with them the existence and regularity of weak solutions to elliptic equations (Chapters 4–6 of the same notes). Morrey's inequality is the complementary statement for and yields continuity of Sobolev functions. Without these estimates, a weak solution obtained by the Lax–Milgram or Galerkin method carries no pointwise or integrability information.
Formalizing it. Mathlib contains a Gagliardo–Nirenberg–Sobolev inequality for compactly supported functions with a non-explicit constant (MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq, restated on the platform as FamousTheorems.gagliardo_nirenberg_sobolev and included here as a reference item). Mathlib has no weak derivatives in the integral form used here, no spaces on open sets, no density theorem for them, no embedding, and no Morrey inequality. This mission asks for the explicit constant, the Loomis–Whitney-type product inequality in the form the proof uses, and the first results on Sobolev spaces built from integral-form weak derivatives.
The explicit constant cannot be read off Mathlib's existing inequality, whose constant is defined through its own proof. It has to come from the one-dimensional bound (Lemma 3.26) combined with the product inequality (3.10). Theorem 3.27 is an induction on dimension in which Hölder's inequality is applied on sections of and then integrated over the remaining coordinate. Expressing " with the th coordinate omitted" and Fubini across those splittings of is the bulk of the measure-theoretic bookkeeping. For the argument has to be applied to , which is only .
Theorems 3.24 and 3.31 need weak derivatives to commute with mollification and cutoff. They also need the weak derivative of a limit to be identified, and completeness of . None of this is available for the integral-form definition. Morrey's inequality needs averages over balls and polar-coordinate integration.
EuclideanSpace ℝ (Fin n) with volume. Coordinates are 0-based (i : Fin n), and multi-indices are Fin n → ℕ. is ‖gradient f x‖, which equals the operator norm of fderiv ℝ f x. norms are eLpNorm in , with real exponents coerced by ENNReal.ofReal.ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞). ContDiff ℝ ⊤ means analytic in current Mathlib, and using it for test functions would leave only the zero function, making every function weakly differentiable. A test function on has HasCompactSupport φ and tsupport φ ⊆ Ω, so the test class is all of . A smaller class would trivialize weak differentiability, and this formalization rules that out.MemW k p Ω f is membership in . sobolevNorm is the norm of Definition 3.23, valued in and built from a chosen weak derivative (unique a.e.). For it uses the essential supremum.The capacitated vehicle routing problem (CVRP) asks for delivery routes of minimum cost. Each route starts and ends at a depot, every customer is visited exactly once, and the demand served on a route does not exceed the vehicle capacity. The problem is central in logistics and one of the most studied problems in combinatorial optimization. Its standard exact methods are branch-and-cut algorithms built on the two-index vehicle flow formulation, a 0/1 program over arcs whose capacity constraints are the rounded capacity inequalities (RCIs); see Laporte, Nobert and Desrochers (1985) and Semet, Toth and Vigo (2014).
In practice customer demands are uncertain. A chance-constrained CVRP requires each route to respect its capacity with probability at least under a known distribution. That distribution is rarely known. Most solution methods also need independent demands. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) study the distributionally robust chance-constrained CVRP. There the chance constraint must hold for every distribution in an ambiguity set of plausible distributions. The ambiguity set may contain dependent distributions and uncountably many of them, so it is not clear a priori that the problem can be solved by the usual branch-and-cut machinery. This mission formalizes the paper's answer to that question: its Theorem 1 and the counterexample that precedes it.
The graph is complete and directed. Its nodes are and its arcs are . Node is the depot and are the customers. There are vehicles, indexed by , each of capacity . Traversing the arc costs ; costs may be asymmetric.
A route is an ordered list of customers, with . A route set partitions into nonempty ordered routes. Its cost is .
The demand vector is random. The ambiguity set is a set of probability distributions of and is the risk level. The problem RVRP() minimizes over route sets such that
With , the demand estimator of the paper's Eq. (2) is
The problem 2VF() minimizes over with in- and out-degree at every customer and at the depot, and with the RCIs
A route set induces the arc vector with exactly when for some (the paper's Eq. (3)). The estimator satisfies the subadditivity condition (S) if for all .
Assume -a.s. for all , and assume is real valued and satisfies (S). Then:
Theorem 1 separates the modeling question from the algorithmic one. Whenever the ambiguity set yields a subadditive estimator, the distributionally robust CVRP is solved exactly by a two-index flow branch-and-cut. The only change from the deterministic case is the right-hand side of the RCIs, however many distributions contains. The companion missions of this series show that (S) holds for every moment ambiguity set (Theorem 2 of the paper) and compute for several classes of such sets. Example 1 shows that the hypothesis cannot be dropped: ambiguity sets that pin down each customer's marginal distribution break the equivalence.
The paper's proofs are in its online supplement; no machine-checked version of these statements exists. Formalizing them produces a checked reduction between a stochastic routing model and an integer program. It also produces reusable definitions of route sets, induced arc flows and RCIs over directed graphs with a depot.
Direction (ii) is a graph decomposition. A 0/1 vector with the prescribed degrees splits into depot cycles plus possibly depot-free subtours. The RCIs, through the in , must exclude the subtours, and the RCI on the customers of a single route must enforce that route's chance constraint. Uniqueness up to reordering requires that directed routes are recovered from arcs.
Direction (i) is where (S) enters. The naive argument bounds the number of vehicles entering by directly from the chance constraints. It fails because the chance constraints control each route separately, while looks at the joint worst case of the demands in ; Example 1 is exactly this failure. A set is typically visited by several routes, each covering only part of it. Relating the per-route guarantees to the joint quantity needs both hypotheses of the theorem: nonnegative demands and (S).
Customers are Fin n (0-based; the paper's customer is i - 1). Nodes are Fin (n+1) with the depot 0 and customer i at i.succ, and vehicles are Fin m. A route set is R : Fin m → List (Fin n): every route is nonempty and the concatenated routes are a permutation of all customers. Arc vectors are ℕ-valued functions on ordered node pairs, with values in and the non-arcs fixed to .
Distributions are measures on Fin n → ℝ, and the ambiguity set is a set of probability measures. Chance constraints are written ENNReal.ofReal (1 - ε) ≤ P {q | …}. Value-at-risk is the published MultistageStochastic.valueAtRisk at level 1 - ε. The worst-case VaR is a real sSup and is integer valued.
Two conventions implicit on the page are explicit hypotheses:
A real sSup of an unbounded set is in Lean. Without the boundedness hypothesis every such estimator would silently equal and (ii) would fail. For an empty ambiguity set the Lean estimator equals on nonempty sets, as the paper's does.
The RCIs range over all nonempty customer sets with the depot on the outside. The estimator keeps the ceiling and the . 2VF feasibility mentions neither routes nor chance constraints. RVRP feasibility does not mention . A formalization in which either side refers to the other, or in which drops the , is not this theorem.
Useful contributions include lemmas on the decomposition of degree-constrained 0/1 arc vectors into depot cycles, monotonicity of VaR under almost-sure ordering, and the CDF right-continuity behind milestone 1.
Related platform work: SupplyChainTheory_vrp formalizes a different, symmetric, unit-demand VRP and is not reused.