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?
Many engineering and economic planning problems must meet random requirements with a prescribed reliability: a reservoir must satisfy demand with probability at least , a power system must cover load except on rare days, an inventory must avoid shortage with high probability. Probabilistic constrained programming (also called chance-constrained programming) models this by requiring that a system of random inequalities hold jointly with probability at least .
The first obstacle to solving such problems is structural. The probability that random constraints are satisfied is, in general, neither concave nor convex in the decision, so the feasible set need not be convex and local search can stall. Prékopa's theory of logarithmically concave measures (1971–1973) removed that obstacle for a large class of distributions, and it is the basis of the numerical methods of Chapter 5 of Ermoliev and Wets, Numerical Techniques for Stochastic Optimization (Springer 1988). This mission formalizes the structural theorems of that chapter.
Timeline:
Let be a random vector in on a probability space and let . The chapter studies problem (5.1):
The function is the probability function (chanceProb in Lean). In the special case it equals , where is the joint distribution function of .
A function is logarithmically concave on a convex set if
Where this is concavity of ; the power form also makes sense where . Nondegenerate normal densities, uniform densities on convex bodies and exponential densities are log-concave.
Section 5.7 introduces the polynomial distribution (5.19) on the cube :
(polyDistF in Lean).
If are jointly concave on and has a log-concave density on , then
Its immediate consequence is that the feasible set is convex for every .
The platform theorem ConvexOptimization.prekopa_marginal_log_concave (Prékopa's marginal theorem, proved) is included as a reference item.
Theorem 5.1 turns a probabilistic constraint into a convex constraint after taking logarithms. This is what makes convergence proofs for nonlinear programming methods (SUMT with logarithmic penalty, supporting hyperplanes, reduced gradients) applicable to (5.1) and to the reliability maximization problem (5.4); without it, those methods have no guarantee of finding a global optimum. Theorems 5.2.1 and 5.2.2 are the two facts that make the SUMT method of §5.2 well defined and convex on the interior of the feasible set. Theorem 5.7.2 shows that probabilistic constraints under the polynomial distribution define convex sets, so they can be added to geometric programmes.
On status: Theorem 5.1 is a classical result, proved in Prékopa's papers (the chapter itself refers to Prékopa's survey for the proof). Prékopa's marginal theorem and the Prékopa–Leindler inequality are already machine-checked on this platform; Theorem 5.1 and the §5.2 and §5.7 theorems are, as far as a search of the platform shows, not formalized. The work is formalizing known proofs, in the log-concavity predicate the platform already uses.
The obvious argument for Theorem 5.1, "the constraint set is convex and the density is log-concave, so the probability is log-concave", hides the real content: log-concavity of a probability as a function of a parameter is a statement about integrals, and it does not follow from pointwise properties of the integrand without a Prékopa–Leindler-type inequality. Concavity of each separately in and in is not enough; joint concavity in is used essentially. The probability function vanishes on large regions in typical examples, so any argument that takes logarithms pointwise fails at the boundary of its support.
For Theorem 5.2.2 the naive argument fails at the index : nothing about is assumed directly, and log-concavity of is exactly Theorem 5.1. For Theorem 5.7.1 the difficulty is a sign condition on a covariance; without the ordering hypothesis the mixed derivative can be negative.
and are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin q); the constraint functions take pairs in the product, and concavity is ConcaveOn ℝ Set.univ on that product (joint concavity). A "continuous probability distribution with density " is stated as P.map ξ = volume.withDensity (ENNReal.ofReal ∘ f) with and measurable and a probability measure. Log-concavity is the platform definition ConvexOptimization.LogConcaveOn (nonnegativity plus the power inequality), imported as a reference item; concavity of Real.log ∘ h₀ would be a different, wrong property because Lean's Real.log 0 = 0. Indices are 0-based (Fin r, Fin m, Fin N, Fin n); the probabilistic constraint of Theorem 5.2.2 is stated separately from . The polynomial distribution is a formula on Fin n → ℝ with real powers, used only on the cube.
No constant of the book is replaced by an explicit value: every result of this chapter is qualitative.
Corrections of the printed text, recorded in each item's Formalization Note:
deriv.Theorem 5.2.2 carries all six assumptions of §5.2, including compactness of the feasible set and the Slater point; it does not assume log-concavity of , which must be derived from the density and concavity hypotheses. A trivializing formalization, such as one with a density hypothesis that no probability law satisfies or a log-concavity predicate that holds for every function vanishing somewhere, is ruled out: the density hypotheses are satisfiable (checked locally) and LogConcaveOn is the multiplicative inequality at every pair of points.
Needed infrastructure: Prékopa's marginal theorem (available), log-concavity of indicators of convex sets and of products, measurability of the constraint set, and Artin's theorem that a sum of log-convex functions is log-convex (for Theorem 5.7.2). Artin's theorem and closure properties of LogConcaveOn are reusable beyond this mission, and contributions of them are 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.
Many design problems in control, finance and operations research are convex programs with uncertain constraints: a decision must satisfy for a parameter that is not known in advance. Enforcing the constraint for every possible (robust optimization) is often intractable or too conservative, and a chance-constrained formulation needs the distribution of , which in practice is rarely known. The scenario approach replaces the uncertain constraint by the constraints of observed samples and solves the resulting ordinary convex program. The question it answers is how much of the unseen uncertainty the resulting decision still violates.
The answer, the generalization theorem of the scenario approach, is distribution-free: the probability that the scenario solution violates more than a fraction of the uncertainty is bounded by a binomial tail that depends only on and on the number of decision variables. This mission formalizes that theorem as it is presented in Chapters 3 and 5 of Campi and Garatti's textbook Introduction to the Scenario Approach (SIAM/MOS 2018), the first mission of a series on the book.
Timeline. Calafiore and Campi introduced scenario programs and bounded the violation of their solutions through the count of support constraints (Math. Program. 2005; IEEE TAC 2006). Campi and Garatti proved in 2008 that the binomial-tail bound of Theorem 3.7 holds for every convex scenario program under existence and uniqueness of the solution, and that it is attained with equality by fully supported problems (SIAM J. Optim. 2008), which settled the tightness question. The textbook (DOI 10.1137/1.9781611975444) presents the theorem with a complete proof for fully supported problems in the plane.
Fix a cost vector , a domain , a measurable space of uncertainty instances with a probability , and a constraint set for each .
A solution is a feasible point of least cost. With i.i.d. samples its solution is denoted ; it is a random vector, a function of the sample, and is a random variable in .
For and every , under Assumptions 3.4 and 3.6,
The right-hand side is the upper tail of a Beta distribution. The statement leaves , and the constraint family completely unspecified beyond the two assumptions.
Theorem 3.7 is what makes the scenario approach usable as a design method: it certifies the reliability of a decision computed from data without any knowledge of the data-generating distribution, requiring only independence of the samples. Theorems 3.8 and 1.3 are its two most used consequences, an expected-violation bound and an explicit sample size, and later chapters of the book (constraint removal, the FAST algorithm, empirical-cost results) build on the same statement. Equality for fully supported problems shows that the bound cannot be improved for any and .
The theorem is proved in the literature; it has no machine-checked proof. A formalization produces, beyond the result itself, a reusable library of scenario programs, violation probabilities and support constraints on which the rest of the series (constraint removal, nonconvex support sets) can be stated, and it checks the measure-theoretic content that the book deliberately leaves aside ("measurability issues are glossed over throughout", p. 33).
The deterministic part, at most support constraints, is a short consequence of Helly's theorem. The probabilistic part is where the obvious approach fails. A uniform-convergence argument over all (Vapnik–Chervonenkis theory, footnote 11 of the book) gives bounds of the wrong order and can be vacuous, because it ignores that only the solution matters. The sharp bound is an exact statement about the law of , not a union bound, and problems with fewer than support constraints, or with degenerate configurations of constraints, must be shown to be no worse than fully supported ones; the book treats the general case only in the plane and refers to Campi & Garatti 2008 for general . Handling the null sets and the exchangeability of the samples under the product measure is a substantial part of the work.
EuclideanSpace ℝ (Fin d); the cost is inner ℝ c θ. A sample of size is ω : Fin m → Δ with law Measure.pi (fun _ : Fin m => P), and P is a probability measure.(P {δ | θ ∉ Θδ δ}).toReal; probabilities of events over the sample are compared in through ENNReal.ofReal.θstar : (Fin N → Δ) → EuclideanSpace ℝ (Fin d) together with the hypothesis that θstar ω solves the program for every sample; it is never an arbitrary map.θstar is measurable (the book's p. 33 convention); ; .Finset.card over Fin m.A statement in which is any feasible point of the program, or merely a measurable function of the sample, is false and does not count as a formalization of Theorem 3.7; nor does one in which Assumption 3.6 is weakened to almost every sample. Contributions of general infrastructure are welcome: exchangeability arguments for product measures, the binomial–beta identity, and Helly-type counting lemmas are reusable well beyond this mission.
The free Schrödinger operator is the Hamiltonian of a quantum particle, or of non-interacting particles, moving in without external forces. Every Schrödinger operator studied in quantum mechanics is a perturbation of it, and each standard tool of the theory refers back to : the Kato–Rellich theorem asks that be relatively bounded with respect to , Weyl's theorem compares essential spectra with that of , and scattering theory compares the dynamics with the free dynamics . Knowing exactly what is (its domain, its self-adjointness, its spectrum and its time evolution) is therefore the base case of the spectral theory of Schrödinger operators.
All of this is obtained from one tool, the Fourier transform, which turns differentiation into multiplication. This mission follows Chapter 7 of G. Teschl, Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), doi:10.1090/gsm/099. The chapter first develops the Fourier transform on the Schwartz space, on and on , and then applies it to . The same material appears in Reed–Simon (Vol. II, Sec. IX.1 and IX.7).
Write for Euclidean space with and . For an integrable the Fourier transform and its inverse are
The Schwartz space consists of the smooth functions all of whose derivatives decay faster than any polynomial. and are the usual Lebesgue spaces, and denotes the continuous functions vanishing at infinity. The convolution of is .
The Sobolev space is . The free Schrödinger operator is
in units with and mass . Its time evolution is . For a linear operator with domain , the resolvent set is the set of for which maps bijectively onto the Hilbert space with a bounded inverse , and the spectrum is . For self-adjoint and a vector , the spectral measure is the finite Borel measure on with for all . The absolutely continuous, singular continuous and pure point spectra are the spectra of restricted to the vectors whose spectral measures are of the respective type. A subspace is a core if the closure of is .
For , is self-adjoint and
In the Lean statement the spectral-type part is the equivalent assertion that every spectral measure of is absolutely continuous with respect to Lebesgue measure.
The result. Theorem 7.8 says that a free quantum particle has no bound states and that its energy spectrum is purely absolutely continuous and fills . Combined with the RAGE theorem this gives the escape of every free wave packet from bounded regions, and Lemma 7.10 makes the escape quantitative: at large times the position distribution is the momentum distribution rescaled by . The self-adjointness of on and the core are the inputs to the Kato–Rellich treatment of atomic Hamiltonians, and is the reference spectrum of Weyl's theorem and of the HVZ theorem.
Formalizing it. The results are classical. Mathlib contains the Fourier transform on , Schwartz space and in the normalization (including Fourier inversion, Riemann–Lebesgue and the isometry), and the Prove2Me corpus holds several of these as FamousTheorems in that normalization. What is missing is Teschl's normalization with its constants, the spectrum of the Fourier transform, the operator as an unbounded self-adjoint operator, its resolvent spectrum and spectral type, and the free dynamics. This mission produces these objects in a form the later chapters (Kato–Rellich for atoms, Weyl, HVZ, scattering) can build on.
The Fourier-analytic milestones are close to Mathlib but not in it: every constant has to be transported from the -in-the-exponent convention to Teschl's convention, including the branch of in Lemma 7.3 and the phase in Lemma 7.10. The lower bound in Theorem 7.5 needs an eigenfunction for each fourth root of unity, which the book defers to the Hermite functions of Section 8.3.
For the goal, self-adjointness and require working with the resolvent spectrum of an unbounded LinearPMap, which Mathlib does not provide, and transporting self-adjointness and resolvents through the unitary Fourier transform. The spectral-type statement requires identifying the spectral measure of an unbounded operator from its resolvent alone, without a spectral theorem in the library, and showing that it has a density for every , not only for nice . Lemma 7.9 is a statement about the graph norm of , which is not controlled by the norm alone.
is EuclideanSpace ℝ (Fin n), so that and are the Euclidean ones, and is Lp ℂ 2 volume. fourier and fourierInv are Teschl's integrals (7.3) and (7.8) with the prefactor . The transform (fourierL2) is Mathlib's unitary transform rescaled by , and Theorem 7.5 asserts that it is the unitary extension of (7.3). (freeHamiltonian) and (timeEvolution) are defined as Fourier conjugates of the maximal multiplication operator by the symbol of and of multiplication by , written with Mathlib's transform, where the symbol is . These are the same operators as Teschl's, and the domain is exactly . Unbounded operators are Mathlib LinearPMaps, self-adjointness is Mathlib's IsSelfAdjoint, and the resolvent and spectrum are the bijective-with-bounded-inverse notions of Teschl, p. 73, not Mathlib's Banach-algebra spectrum, which is used only for the bounded operator in Theorem 7.5. Statements that need it carry , which the book leaves implicit.
No projection-valued measure or functional calculus is taken as data. The spectral types in (7.25) are expressed through the spectral measures , and these are pinned down intrinsically by their Borel transforms .
A trivializing formalization is ruled out: is the resolvent spectrum of the operator, not the essential range of , so is not a computation on a multiplication symbol. The absolutely continuous measure in the goal must reproduce the actual resolvent matrix elements, so it cannot be chosen freely, and is not defined by its integral kernel (7.30).
A complete development needs change of normalization lemmas for the Fourier transform, the Hermite eigenfunctions of , unitary equivalence of LinearPMaps and its effect on adjoints and resolvents, self-adjointness of maximal real multiplication operators, polar coordinates on , and graph-norm approximation by cut-offs. The normalization bridge and the multiplication-operator results are reusable across the series. Contributions of either are welcome.
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.
In best arm identification with fixed confidence, a learner samples unknown distributions ("arms") one at a time, and must eventually stop and name the arm with the largest mean, with an error probability at most a prescribed risk , while using as few samples as possible. The problem goes back to the sequential design of experiments (Chernoff, 1959; Even-Dar, Mannor and Mansour, 2006) and underlies adaptive A/B testing, clinical trial design and hyperparameter selection.
Any fixed-confidence strategy consists of three parts: a sampling rule, a stopping rule and a decision rule. Garivier and Kaufmann (arXiv:1602.04589, COLT 2016) proposed the Track-and-Stop strategy, the first shown to match the asymptotic lower bound on the expected sample complexity. Its stopping rule is a generalized likelihood ratio (GLR) test, Chernoff's stopping rule. Its correctness, the guarantee that the recommended arm is wrong with probability at most , must hold whatever the sampling rule, which is what allows the sampling rule to be tuned freely for efficiency. This mission formalizes that guarantee for Bernoulli arms, Theorem 10 of the paper, with its explicit threshold .
The arms are . A Bernoulli bandit model is a mean vector : pulling arm returns reward with probability and otherwise, independently of the past. The class contains the models with a unique optimal arm , i.e. for all .
At round the learner chooses an arm as a (possibly randomized) function of the past observations and observes a reward . Write for the number of pulls of arm among the first rounds, for the number of those pulls that returned , and for the empirical mean. The likelihood of arm 's observations under mean is .
The GLR statistic for "arm is at least as good as arm " is
Chernoff's stopping rule with exploration rate is
and the decision rule recommends .
The Krichevsky–Trofimov (KT) distribution on binary sequences is , the Bernoulli likelihood mixed over the Beta prior.
For every , every sampling strategy, and the threshold ,
is a probability law on , and for ,
With , for all arms with ,
Theorem 10 decouples correctness from efficiency. Because the guarantee holds for every sampling strategy, any sampling rule, including the C-Tracking and D-Tracking rules of Track-and-Stop, the uniform rule, or a heuristic, inherits -correctness as soon as it is paired with Chernoff's stopping rule at this threshold. The asymptotic optimality result of the paper (Theorem 14) then only has to control the sample complexity. The threshold is explicit, with no unspecified constant, in contrast to the deviational threshold of Proposition 12.
The result is proved in the paper, in Appendix C.1, and rests on Lemma 11, which the paper quotes from the universal coding literature without proof. As far as the platform's catalog shows, none of these results is formalized. The platform holds a machine-checkable statement of the analogous result for Gaussian arms with the Lattimore–Szepesvári threshold (BanditAlgorithm.chernoff_stopping_rule_sound, Lemma 33.7 of Bandit Algorithms), which is a different model and a different threshold. Formalizing Theorem 10 adds a proof of Lemma 11 (the KT regret bound, reusable in information theory and universal prediction), the Bernoulli GLR statistic, and a change of measure from the true bandit law to a Bayesian mixture law on the trajectory space.
The obvious approach bounds, for each fixed , the probability that exceeds by a concentration inequality and sums over . This fails: the sampling strategy is arbitrary and adaptive, so and are random and depend on the past rewards, and a fixed-sample-size deviation bound does not apply; a union bound over the possible values of the counts loses more than the threshold allows. The maximum likelihood in the numerator of is also not a probability density, so the likelihood ratio cannot directly be read as a change of measure. The argument must control the whole trajectory law under an arbitrary randomized policy, and must handle empty samples (an arm never pulled contributes likelihood ) and the boundary means and .
The formalization is in Lean 4 with Mathlib and reuses the platform's canonical bandit model: StochasticBandit, BanditPolicy (a Markov kernel per round from the observed history to the next arm, so randomized strategies are included), banditTrajMeasure (the law of the infinite trajectory, where coordinate is round ) and IsSoundBAI from BanditTrajectory; bernoulliBandit from bernoulliRelativeEntropy; and only the pull counts trajPullCount and empirical means trajEmpiricalMean from TrackAndStop. The Gaussian GLR and threshold of TrackAndStop are not used.
Conventions committed to:
Fin K. Bernoulli means range over , degenerate laws included; the paper's exponential-family mean space is , so the statement implies the paper's.Disclosed deviations from the page: Lemma 11's ratio bound is stated for , since at the printed bound reads ; the use of the lemma in Appendix C.1 is unaffected. Appendix C.1 calls the result "Proposition 10" (a slip for Theorem 10) and prints the KT density as (a slip for of Lemma 11, which is the normalized one); the formalization follows Lemma 11.
A trivializing formalization is ruled out: stating the result for Gaussian arms or with the Lattimore–Szepesvári threshold is the platform's existing Lemma 33.7 and is not Theorem 10, and a free decision rule without the argmax hypothesis would make the claim false rather than faithful.
Contributions welcome: a proof of Lemma 11; a change-of-measure lemma for banditTrajMeasure under a mixture of environments; and the union-bound reduction from the goal to the pairwise claim.
In a combinatorial auction a seller offers several indivisible items at once, and bidders value bundles of items rather than items one at a time. Allocating the items to maximize total value is the central optimization problem of the area, and it arises in spectrum licensing, procurement and transport contracting (Cramton, Shoham and Steinberg, Combinatorial Auctions, MIT Press, 2006). Two obstacles meet. Computationally, a valuation has numbers, so an algorithm can only query it, and even then optimization is hard. Strategically, the valuations are private: a bidder reports whatever maximizes its own utility, so an algorithm that is a good approximation on true inputs may be useless on reported ones.
The classical answer to the strategic obstacle is the VCG payment scheme, which makes truthful reporting a dominant strategy but requires the exact optimum. Nisan and Ronen (2007) showed that an approximation algorithm becomes truthful under VCG payments essentially only when it is maximal in range: it fixes a restricted set of allocations in advance and optimizes exactly over that set. Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010, §5) give such an algorithm for complement-free (subadditive) bidders that uses only value queries and loses a factor of order . For general valuations in the value-query model the paper cites a lower bound of order (Dobzinski and Schapira, working paper 2005; Blumrosen and Nisan, Hebrew University Discussion Paper 381, 2005; see the paper's references [7] and [2]), and the same paper (Theorem 6.1) shows that even XOS bidders cannot be approximated within with polynomially many value queries.
A set of items is sold to bidders. Bidder has a valuation that assigns a real number to every bundle . Throughout, valuations are normalized, , and monotone, . A valuation is complement free (CF) if for all bundles . An allocation gives the bidders pairwise disjoint bundles (items may stay unallocated), and its social welfare is .
The mechanism receives reports and runs the following algorithm :
Its range is the set of allocations that give all of to one bidder, together with the allocations in which every bidder receives at most one item. Under VCG payments bidder receives , so its utility is . The mechanism is incentive compatible on a class of valuations if no bidder can raise its utility by misreporting within that class, whatever the others report.
For every choice of the maximum-weight matching and of the top bidder as functions of the reports, for every profile of normalized, monotone, CF valuations and every allocation ,
and the mechanism is incentive compatible on the CF valuations.
AGT.vcg_incentive_compatible).The theorem shows that, for subadditive bidders, the barrier known for general valuations can be matched by a truthful mechanism that asks each bidder only value queries. It is one of the early examples of maximal-in-range mechanism design, a template later used for many truthful approximation mechanisms in combinatorial auctions, and it sits against Theorem 6.1 of the same paper, which shows that for XOS bidders no value-query algorithm with polynomially many queries does better than .
The result is proved in the paper. What this mission adds is a machine-checked proof: a formal model of VCG-based mechanisms over a restricted range, a proof that the §5.2 algorithm is maximal in range for every tie-breaking of its two optimization steps, and the explicit constant in the bound. To our knowledge neither half of Theorem 5.1 is formalized elsewhere; the general VCG theorem exists on the platform in the setting of arbitrary outcome sets.
The approximation argument partitions the bidders of a reference allocation by whether their bundles have at least items, and the two cases need different facts: disjointness bounds the number of large bundles by , and subadditivity bounds each small bundle by its size times its best item. A naive transcription breaks at degenerate inputs: the page divides by and writes strict inequalities, both of which fail when a bundle is empty or all values are zero, so the formal statement must be organized around non-strict bounds.
Incentive compatibility has a different obstacle. It holds only if the allocation rule depends on the reports alone and optimizes exactly over its range, including at ties between the grand bundle and the matching. The matching and the top bidder are not unique, so the proof must work for an arbitrary but fixed tie-breaking, and the welfare of the matching allocation must be identified with the matching weight, which uses normalization of every bidder who receives nothing.
Bidders are Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. Normalization and monotonicity (the paper's standing assumptions, p. 1) and complement freedom are hypotheses; IsCFValuation bundles all three. An allocation is a family of pairwise disjoint bundles; unallocated items are allowed. A matching is a partial map Fin m → Option (Fin n) with no bidder matched twice.
Conventions the formalization commits to:
Real.sqrt m.mat, top of the report profile, each with a specification hypothesis; the goal is stated for every such pair. The algorithm reads only the reports; the tie between and goes to the matching, as on the page.AGT.MechIncentiveCompatible on outcomes .A trivializing formalization is ruled out: the ratio is the explicit rather than an existential constant, incentive compatibility is over the full CF domain (not additive reports only) for a rule that cannot see true valuations, and the rules mat, top are satisfiable (a maximum over the finitely many matchings exists; a top bidder exists when ).
Useful infrastructure: finite maximum-weight matchings on complete bipartite graphs, subadditivity bounds over Finset sums, and a reusable lemma that maximal-in-range rules with VCG payments are truthful. Contributions of any milestone are welcome; milestones 2 and 4 are self-contained.
A Markov decision process (MDP) is solved by dynamic programming only when its transition probabilities are known. In practice they are estimated from data, and the optimal policy of the estimated model can perform badly on the true one. Nilim and El Ghaoui (Oper. Res. 53(5), 2005) showed that, when the uncertainty on the transition matrices has a product ("rectangular") structure, the robust problem, in which the controller minimises the worst expected cost over all admissible transition matrices, keeps the structure of dynamic programming. The robust Bellman operator replaces the expectation of the next-stage value by a support function of the uncertainty set. That operator is the basis of later work on robust MDPs and robust reinforcement learning.
Timeline:
The state space is and the action set is finite and nonempty. Each state–action pair has a cost , and costs are discounted by a factor : the cost at stage is .
Write for the probability simplex. For each action and state a nonempty set is given. It is the set of distributions of the next state that nature may use from state under action . No convexity or closedness is assumed. Uncertainty is rectangular: the admissible transition matrices for action form the product , so every row is chosen independently.
A stationary control policy applies one decision rule at every stage; is the set of them. A stationary policy of nature fixes one matrix for each action and uses it forever. Nature chooses after the controller.
From an initial state , the state distribution evolves as , . The discounted cost is
The support function of a set is . The robust Bellman operator and, for a stationary policy , the robust evaluation operator act on by
The two values of the game are
There is a unique with , i.e.
value iteration converges to from every starting vector (20), and
In addition, every policy that picks a minimising action in (19) is optimal (21), every nature policy whose rows attain is optimal for nature (22), and for each stationary the worst-case cost is , where is the unique fixed point of (23).
The theorem makes the robust discounted problem as tractable as the nominal one. The optimal robust policy is stationary, deterministic and computed by value iteration. Each iteration evaluates one support function per state–action pair, and the paper computes these efficiently for likelihood and entropy uncertainty sets (§§5–6). Perfect duality means that the order of play does not change the value: announcing the policy to an adversarial nature costs nothing. The sequel in this series (Theorem 4) uses Theorem 3 to show that restricting to stationary policies loses nothing.
The result is proved in the paper and, independently, by Iyengar (2005). No machine-checked proof of it is known to exist. Mathlib provides the Banach fixed-point theorem, but it has no MDP library, no discounted cost along a Markov chain and no robust Bellman operator. The mission produces that layer.
The fixed-point half is a direct application of the Banach fixed-point theorem once the -contraction is established. The substance is the link between the fixed point and the probabilistic cost, and the duality.
Fin n → ℝ, with the componentwise order and Mathlib's sup metric, which is .RobustMDP.Discounted.Model) carries the costs, the discount (the range printed in Theorem 3; §4 prints ) and the row sets. The row sets are assumed nonempty and contained in and nothing else. Nonemptiness is implicit in the paper.Fin n → A. is the subtype of A → Fin n → Fin n → ℝ whose rows lie in the row sets, which encodes rectangularity.tsum of the discounted stage costs along the forward state distribution. The terms are nonnegative and at most , so the series is summable and the tsum is the limit of the -stage costs, the paper's definition.sSup. It is the genuine supremum because every set it is applied to is nonempty and inside .IsLUB, or ⨆ inside , whose inner sets are shown bounded by conclusion (23). Minima over the finite and over are ⨅ and Finset.inf'. The argmax rows of (22) appear only as a hypothesis on a given nature policy that attains them.A discrete function defined only on the integer lattice cannot, by itself, be minimized by the tools of continuous optimization — gradients and convexity in the classical sense simply do not apply. Murota's theory of M-convex functions closes this gap by showing that the exchange axiom alone, a purely combinatorial condition, is enough to guarantee that a discrete function behaves exactly like a convex one: its minimizers form a well-structured (M-convex) set, it can be extended to a genuine convex function on real space without gaining any new local minima, and its behavior under a change of price vector (in the economic interpretation where the function is a cost and its argument a bundle of goods) satisfies the same gross substitutes law economists have studied since Kelso and Crawford's matching-market models. This mission develops the second half of that connection: from local optimality (established in the companion mission) to the full structural picture — minimizer sets, price-substitution laws, and the extension of M-convex functions to genuine convex functions in real variables.
Companion mission 06-mconvex-functions-i (Discrete Convex Analysis V) and sibling mission
22-ch06b-mconvexfunctions (Discrete Convex Analysis XXI) cover this chapter's optimality
theory (the M-optimality criterion, the exchange axiom as sequential improvement) and its
algebraic toolkit (domain operations, worked examples). This mission builds the vocabulary those
results also need (redeclared here, since sibling drafts cannot yet import one another) and
proves the results on minimizer structure, gross substitutability, and convex extension that
this chapter's remaining sections develop: the M-convexity of minimizer sets, the gross
substitutes and stepwise gross substitutes properties and their characterizing role, a
minimizer-cut theorem with scaling, integral convexity of M♮-convex functions, and — this
mission's goal — the theorem characterizing M-convexity entirely through the polyhedral
structure of a function's convex extension.
Fix a finite ground set . For with nonempty effective domain, write for the linear reweighting by , and for the minimizer set of any function . The convex closure of at a real point is the infimum, over finite convex combinations of points of representing , of the corresponding combination of function values; is convex extensible if agrees with on , and integrally convex if can always be computed using only points from 's own integral neighborhood (the integer vectors within one unit of in every coordinate). A polyhedral convex function is (polyhedral) M-convex if it satisfies the real-variable exchange axiom (M-EXC[R]): for and , some and make the exchange inequality hold for every .
For with nonempty effective domain,
with the M♮-analogue using M♮-convex polyhedra (Theorem 6.43). This is the weakest stable form: it characterizes M-convexity purely by properties of the (unique) convex closure, without reference to any specific algorithm for computing it or any bound on the polyhedron's complexity.
Ten further results build the toolkit this goal draws on and the picture it completes: the M-convexity of minimizer sets (Proposition 6.29), the gross substitutes and stepwise gross substitutes properties and the theorems showing they characterize M-convexity and M♮-convexity among convex-extensible functions (Propositions 6.32-6.33, 6.35, Theorems 6.34, 6.36), a minimizer-cut theorem with scaling used algorithmically in Chapter 10 (Theorem 6.39), integral convexity of M♮-convex functions (Theorem 6.42), a shared-coefficient convex-combination theorem for pairs of M♮-convex functions used in Chapter 8's separation theorem (Theorem 6.44), and the polyhedral-M-convexity of an M-convex function's convex extension together with the correspondence between polyhedral M♮-convexity and the real exchange axiom (Theorems 6.45, 6.47).
Theorem 6.43 is what makes the whole edifice of M-convex function theory a genuine extension of M-convex set theory (chapters 4-5) rather than a separate parallel development: it says that knowing a function's convex extension is polyhedral, with every price-weighted minimizer set an M-convex polyhedron, is not merely a consequence of M-convexity but an exact characterization of it. This is the theorem that lets later results (the discrete conjugacy theorem of Chapter 8, the separation theorems for M♮-convex functions) move freely between the discrete and continuous pictures. The gross substitutes property (Propositions 6.32-6.36) is independently significant outside this book: it is the exact condition, discovered independently in mathematical economics (Kelso-Crawford, Gul-Stacchetti), under which competitive equilibria with indivisible goods are guaranteed to exist — Murota's theorem that gross substitutability characterizes M-convexity (among convex-extensible functions) is what unifies the economic and combinatorial literatures on this question, taken up again in Chapter 11.
None of these results are open — they are Murota's systematic account of a theory with roots in
matroid theory, submodular optimization, and mathematical economics. What this mission
contributes is a faithful, machine-checked formal statement of each, extending the shared Lean
vocabulary (MExchangeAxiom, ConvexClosureVal, ArgMinOn) the Discrete Convex Analysis
series builds on; no comparable formalization exists on the platform (see Formalization scope).
The forward direction of Theorem 6.43 (M-convex convex extensible with polyhedral minimizers) is comparatively direct given Theorem 6.42 and Proposition 6.29. The converse is substantial: it must show that a function whose weighted minimizer sets are all M-convex polyhedra — a purely global, polyhedral condition — satisfies the local exchange axiom (M-EXCloc[Z]), and the book's proof does this by an edge-direction argument on the polyhedron : every edge of an M-convex polyhedron must be parallel to some , a fact borrowed from the combinatorial structure of chapter 4's base polyhedra applied to a carefully perturbed weight vector. No shortcut through convex analysis alone succeeds, because ordinary polyhedral theory says nothing about which combinatorial directions a polyhedron's edges must follow — that content comes entirely from the M-convexity of the minimizer sets, not from convexity of the closure by itself.
Ground-set elements are a Fintype V with DecidableEq; functions are (V→ℤ)→WithTop ℝ
(integer domain) or (V→ℝ)→WithTop ℝ (real domain, for the polyhedral theorems). The convex
closure is built directly from finite convex-combination representations rather than an abstract
closure operator, and integral convexity compares it against the same construction restricted to
each point's integral neighborhood (Fintype.piFinset of per-coordinate Finset.Icc). Real
M-convex/M♮-convex polyhedra are defined as convex hulls of M-convex/M♮-convex integer sets,
reusing chapters 4-5's own characterization. The real-variable exchange axioms (Theorems 6.45,
6.47) are formalized from the book's primal (interval-of-) definition, not the
directional-derivative reformulation (M-EXC'[R]); Theorem 6.47's own three-way equivalence is
correspondingly stated with only its first two legs (see Difficulty and
MODERATION_NOTES.md/HARD.md — this is a documented scope choice, not a trivializing
omission, since the six results using the primal axiom already exercise the chapter's real-
variable machinery in full). No numeric constants are hard-coded anywhere in this mission beyond
the book's own literal coefficients in Theorem 6.39's cut bound ((n-1)(α-1)). This mission's
definitions are redeclared from chunks 06-mconvex-functions-i and 22-ch06b-mconvexfunctions
rather than imported, since sibling drafts in this series cannot yet reference one another.
Contributions completing any of the twelve sorrys are welcome; the goal's converse direction
and Theorem 6.44's shared-coefficient construction carry the most independent proof content.
A convex polytope has two standard descriptions: as the convex hull of finitely many points, and as the intersection of finitely many half-spaces. Linear programming uses both at once. The feasible region of a linear program is given by inequalities, while the simplex method and the theory of basic solutions work with its vertices. That the two descriptions define the same class of sets is the Minkowski–Weyl theorem.
Hermann Weyl's 1935 paper Elementare Theorie der konvexen Polyeder (Comment. Math. Helv., 1935, pp. 290–306) gave an elementary, self-contained proof of this equivalence. An English translation appeared in Contributions to the Theory of Games I (Annals of Mathematics Studies 24, 1950), where it served as the polyhedral foundation for the minimax theorem and linear inequality theory in early game theory and linear programming.
Timeline:
Write for vectors of . A point system is a finite set . It is non-degenerate if no has for all . A vector is a support of if for all . A support is an extreme support if equality holds at linearly independent points of . A point is representable by if with all .
Read as inequalities , , the same defines the cone of solutions. An extreme solution is a nonzero at which linearly independent inequalities of are tight. The dual system consists of the inequalities , one for each extreme solution , and is the cone it defines.
For polytopes, Weyl passes to the hyperplane , identified with , . A convex polyhedron is for a finite whose affine span is all of . Given a finite index set , normals and constants , the inequalities cut out a region
In Weyl's notation, row is , with and .
Assume no row is identically zero ( or ). Then
In words, the normals must positively span and must contain an inner point. The goal is the equivalence, not either half alone.
LinearOptimization.farkas_cone_corollary.The result. §4 II gives both directions of the Minkowski–Weyl theorem for full-dimensional polytopes, together with a test on the data : positive spanning of the normals is equivalent to boundedness, and a strictly feasible point is equivalent to full dimension. Several parts of LP theory start from this equivalence: finiteness of the vertex set of a bounded feasible region, the existence of an optimal vertex, and the passage between the primal (inequality) and dual (generator) descriptions used in polyhedral combinatorics.
Formalizing it. The theorem has been proved since 1935; the work here is formalization. Mathlib has convex hulls, extreme points, and pointed cones with their duals, but no Minkowski–Weyl theorem for polytopes or for cones. On this platform, Farkas-type lemmas (LinearOptimization.farkas_cone_corollary) and the statement that a nonempty bounded polyhedron is the hull of its extreme points (Bertsimas–Tsitsiklis Thm 2.9) are published. Neither gives the "only if" direction, the positive-spanning criterion, or full-dimensionality.
The "only if" direction and the reduction from a strictly feasible bounded region to cones are routine. The hard step is the finiteness statement: why a finite set of inequalities has only finitely many generators, and why these generate the whole region. Mathlib's compactness results give "a compact convex set is the closed hull of its extreme points" (Krein–Milman). That result does not show that the extreme points are finite in number, nor that there are finitely many of them in a form that can be computed from the inequalities. Weyl's route avoids topology. It goes through the Hauptsatz, proved by induction on dimension, and the duality between and . Each step of that duality needs non-degeneracy, and keeping that hypothesis alive through the dualization (Satz 9) is where care is needed.
Fin n → ℝ, with dot product ⬝ᵥ. Point systems are Finsets; the zero vector is allowed in them. "Representable" is an explicit nonnegative sum over the Finset.span = ⊤.Fin m → ℝ, a point standing for Weyl's . Linear independence of homogenized points becomes affine independence of points, and non-degeneracy becomes affineSpan ℝ S = ⊤.Fin n → ℝ, extreme rays of pointed polyhedral cones, and the homogenization dictionary between cones in and polytopes in . Proofs of any milestone, and alternative routes to the goal (e.g. via Fourier–Motzkin elimination), are welcome.The augmented Lagrangian method (method of multipliers) of Hestenes, Powell and Rockafellar solves a constrained nonlinear program by repeatedly minimizing an unconstrained merit function in the primal variables and then updating the multipliers. For inequality constraints, the augmented Lagrangian in the form the paper takes from Rockafellar (Rockafellar 1981) is continuously differentiable but not twice differentiable, even when all problem data are smooth: its Hessian jumps across the surfaces where a constraint switches between the "active" and "inactive" formula. Newton's method for the inner minimization therefore has no classical Hessian to work with on those surfaces.
Qi and Sun (Math. Programming 58, 1993) extended Newton's method to equations with locally Lipschitz, replacing the Jacobian by an element of Clarke's generalized Jacobian, and proved local superlinear convergence when is semismooth. Section 4 of the paper, an example suggested by Rockafellar, shows that the gradient of the augmented Lagrangian of a program is semismooth, so the nonsmooth Newton method applies to the stationarity equation . This mission formalizes that result, Theorem 4.1.
Let be of class and consider
Fix . For a constraint value and a multiplier put
(the two cases agree when ). The augmented Lagrangian is the function of
For a locally Lipschitz map between finite-dimensional spaces, let be the set where is differentiable. Clarke's generalized Jacobian is . is semismooth at if it is locally Lipschitz near and, for every direction , the limit of over , , , exists.
For a single constraint function the proof works with on , and with the surface on which the two formulas for meet.
For and :
All three clauses are the theorem; the last two together cover every point.
The result places the inner problem of the augmented Lagrangian method inside the scope of the paper's convergence theory: with , the generalized-Jacobian Newton iteration converges locally superlinearly at a root where every element of is nonsingular. Its practical content is that second-order methods can be run on even though is only , with the elements of playing the role of Hessians. The same pattern (a merit function with semismooth gradient) recurs in extended linear-quadratic programming and in semismooth Newton methods for complementarity problems.
The theorem is proved in the paper by direct computation. As far as a search of the platform showed, none of the objects involved (Clarke's generalized Jacobian, semismoothness, Rockafellar's augmented Lagrangian) has a published formalization there, and Mathlib has none of them. The mission produces a machine-checked version of the computation and, as a by-product, reusable statements about functions obtained by gluing two pieces along a hypersurface.
Clauses 1 and 3 are calculus with a case split: one has to check that the two formulas for and for its gradient match on the surface. Clause 2 is where the argument is not routine. On the surface, is not differentiable, and the generalized Jacobian there contains convex combinations of the two one-sided Hessians of (4.2). Semismoothness asks that have a single limit over all such , for all approaches , , including approaches that cross the surface infinitely often. The two one-sided Hessians are different matrices, so no single derivative describes near the surface, and the existence of the limit must be shown for approaches that alternate between the two sides and for the convex combinations that contains on the surface itself. General theorems that piecewise-smooth maps are semismooth appear in later literature but are not available in Mathlib, so they cannot be invoked as a shortcut. A second obstacle is infrastructure: Mathlib has no generalized Jacobian, so every fact about (which limits of derivatives occur near the surface) must be derived from the definition.
EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); is a function on their product, and on EuclideanSpace ℝ (Fin n) × ℝ.i : Fin m with paper index i.val + 1; equality constraints are i.val < p, inequality constraints p ≤ i.val. The paper's implicit is not assumed (for there are no inequality constraints).ContDiff ℝ 2 on all of ; "smooth" is the paper's continuously differentiable, ContDiffAt ℝ 1 of the gradient at the point.fderiv, limits are along sequences, and no closure is taken in the convex hull. Semismoothness is the explicit – form of the paper's limit, uniform over .A formalization that states only , or only the semismoothness of one term , is not Theorem 4.1; the goal contains all three clauses for the full . The combination step from the terms to uses that sums of semismooth maps and maps with locally Lipschitz derivative are semismooth; the paper cites this without proof, and a solver will need to prove it.
Contributions welcome: the lemmas above; general facts about clarkeJac (it contains fderiv at points of strict differentiability; it is a singleton for maps; behaviour under sums and linear maps); and the semismoothness of sums.
A decision maker who chooses a portfolio of risky assets with random return vector receives the scalar return and evaluates it by an expected utility . In practice the law of is not known; what can be estimated with some confidence are its mean and covariance . The robust mean-covariance objective replaces the unknown law by the worst law consistent with these two moments:
Ioana Popescu (Operations Research 55(1), 2007) showed that depends on only through and , and that for large classes of utilities it has a closed form or reduces to a one-dimensional search. This turns a robust stochastic program into a parametric mean-variance program, which is the practical point of the paper. This mission formalizes the closed form for concave utilities with a monotone second derivative (Proposition 7), a class that contains the exponential utility and all concave quadratics. The reduction to is the subject of the companion mission Robust Mean-Covariance Solutions for Stochastic Optimization I; the two-point case is mission II.
The underlying univariate question is a moment problem in the tradition of Chebyshev-type bounds: the extremal value of over all laws with prescribed mean and variance. Scarf (1958) solved an instance for a piecewise-linear inventory cost, and Birge and Dulá (1991) treated two-point extremal laws on bounded domains.
Fix and . The mean-variance class is the set of Borel probability measures on with , and (Lean: MeanVarClass m (s ^ 2)). For a utility the robust objective is
with read, as in the paper, "in the wide sense of ", so the value is allowed. The paper's is .
For the two-point law puts mass on and mass on ; these are exactly the two-point laws of . Its expected utility is the two-point objective (8),
A supporting quadratic of is with on ; the set of their coefficients is . Since every has , each element of gives a lower bound on (Proposition 3). The function has the one-point support property with respect to (Definition 3, OnePointSupportWrt u m s) if some supporting quadratic touches at and as or as ; it has one-point support (OnePointSupport u) if this holds for every and every .
Let be concave and twice differentiable with monotone .
(a) If is convex, then
(b) If is concave, the same holds with .
In each part the limit of exists in . When is finite the goal asserts that is integrable under every law of every class, that is the greatest lower bound of the expected utilities, and that has one-point support. When and it asserts .
An additional item states Proposition 8: a monotone convex has one-point support and .
Proposition 7 turns the worst-case expected utility into a mean-variance criterion with an explicit risk weight: a prudent investor ( convex) is penalized by per unit of variance, an imprudent one by the limit at . With Proposition 1, the robust portfolio problem becomes , a concave mean-variance program. For exponential utility the weight is (Example 3 of the paper), so the robust investor must eliminate variance entirely; this is a qualitative statement about robustness that follows only from the case of the theorem.
The result is published with a proof in the appendix of the paper. It has, to the best of our search, no machine-checked version, and the platform currently holds no statement of Propositions 3, 7 or 8 or Definition 3. A formal proof would also check two points where the printed argument is incomplete: the proof's step "" fails for affine , where the theorem nevertheless holds, and the claim that "has one-point support" fails when (see the scope section). Related platform work on worst-case expectations over ambiguity sets is the mission Wasserstein Distributionally Robust Optimization II, which uses a different ambiguity set.
The infimum ranges over all laws with two prescribed moments, an infinite-dimensional set with no compactness, and in the relevant cases it is not attained. The natural first idea, restricting to two-point laws and minimizing over , gives only an upper bound (display (7)), and here the minimizing runs off to the boundary: the extremal law puts vanishing mass on a point escaping to . Identifying the limiting value requires controlling as , a second-order asymptotic statement about at . The matching lower bound requires a supporting quadratic whose curvature is exactly ; showing that it lies below everywhere, not only near , is a global statement that uses the convexity of on the whole line. The finite-limit and infinite-limit cases also behave differently: in the second, no supporting quadratic exists at all.
Laws are Measure ℝ with IsProbabilityMeasure, finite second moment is MemLp id 2, and the class is parameterized by mean and variance with . The statements are univariate: of the paper is the univariate objective at by Proposition 1 of the paper (mission I). Derivatives are deriv u and deriv (deriv u); "twice differentiable" is differentiability of and of . Limits of are explicit hypotheses (Tendsto … atBot (𝓝 L) or Tendsto … atBot atBot), never limUnder. Limits in are one-sided inside . Expectations under two-point laws are written by the explicit formula (8).
"Min" is never a real ⨅, which Lean evaluates to on sets unbounded below. The finite case uses IsGLB together with integrability of under every law of the class; the infinite case asserts that integrable laws with arbitrarily small expected utility exist; Proposition 3 is stated as "every value every value". Proposition 3 assumes integrable under the law; Proposition 8 takes the infimum over laws under which is integrable, which for convex loses nothing.
One correction to the printed statement: Proposition 7 opens with "then has one-point support", which is false when , since no quadratic lies below on . The formalization asserts one-point support only in the finite-limit case and the value in the other. A formalization that took as a real infimum, dropped the integrability conjunct, or asserted one-point support unconditionally would be either trivially satisfiable or false; none of these is used.
A complete development needs: moments of two-point laws, a second-order l'Hôpital or Taylor argument at , the trapezoid inequality for convex functions, and Jensen-type integration of quadratic lower bounds. The mean-variance class, the two-point objective and the supporting-quadratic lemmas are reusable for mission II and for other moment-problem bounds. Proofs of any milestone, and of part (b), are welcome.
Many polytopes of combinatorial optimization have exponentially many facets, yet linear optimization over them is tractable because they are projections of simpler convex sets: affine slices of a nonnegative orthant (linear programming) or of the cone of positive semidefinite matrices (semidefinite programming). The size of such a representation, the number of variables of the extended formulation, is the natural measure of how compactly a polytope can be optimized over. Yannakakis (Expressing combinatorial optimization problems by linear programs, JCSS 1991) characterized polyhedral representations through nonnegative factorizations of the slack matrix. Gouveia, Parrilo and Thomas (arXiv:1111.3164, Mathematics of Operations Research 2013) extended the characterization to lifts into arbitrary closed convex cones, in particular to cones of positive semidefinite matrices.
The stable set polytope of a graph is the standard test case. For a perfect graph on vertices it is a linear image of an affine slice of the cone of positive semidefinite matrices (Lovász's theta body construction, stated in the paper as Theorem 5.1 with a citation to Lovász & Schrijver, SIAM J. Optim. 1991); this is the reason the maximum weight stable set problem is solvable in polynomial time on perfect graphs. The question addressed by this mission is whether a smaller matrix size could suffice. Theorem 5.2 of Gouveia–Parrilo–Thomas answers it: for every graph on vertices, matrices of size do not suffice.
Let be a graph with vertex set . A set is stable if no edge joins two of its elements, and its incidence vector has exactly when . The stable set polytope is
Let be the cone of real symmetric positive semidefinite matrices, with the trace inner product , under which it is self-dual. For a closed convex cone , a set has a -lift if for an affine subspace and a linear map ; the lift is proper if meets the interior of .
For a polytope with vertices and facet inequalities , the slack matrix is the nonnegative matrix . A -factorization of a nonnegative matrix assigns to each row and to each column with . In Lean the objects are stab, HasPSDLift, HasConeLift, HasProperConeLift, IsSlackMatrix, HasConeFactorization and HasPSDFactorization in the namespace ConeLifts.StableSet.
For every and every graph on vertices,
The statement excludes all lifts, proper or not, and holds for every graph, perfect or not.
has no -factorization.
Theorem 5.2 shows that the semidefinite representation of for perfect graphs has the smallest possible matrix size: cannot be lowered to . As Remark 5.3 of the paper notes, the same argument shows that no polytope in with a vertex at which it locally looks like the nonnegative orthant has an -lift. It is also an instance of the factorization method: a statement about all possible semidefinite representations is reduced to a finite obstruction on a small submatrix of the slack matrix.
The theorem is proved in the paper. To the best of our knowledge no machine-checked proof of it, of the factorization theorem for cone lifts, or of any positive semidefinite lower bound for a polytope exists in Mathlib or on this platform. A formalization produces reusable statements about positive semidefinite factorizations, slack matrices and lifts, and a verified instance of the general lower-bound technique.
The step from lifts to factorizations is where the direct argument fails. Theorem 3.3 applies only to proper lifts and only to polytopes with the origin in their interior, while the goal concerns all lifts of a polytope that has the origin as a vertex. Applying Theorem 3.3 to and an arbitrary lift therefore does not match its hypotheses, and the printed proof does not spell out how the two gaps are closed (see Formalization scope). Theorem 3.3 itself is a consequence of the general factorization theorem of the paper (Theorem 2.4), whose proof rests on conic duality. The core lemma about is a statement about every family of positive semidefinite matrices, so it cannot be settled by any finite search.
is EuclideanSpace ℝ (Fin n); vertex of the paper is i : Fin n; graphs are SimpleGraph (Fin n) and stability is SimpleGraph.IsIndepSet. Vertices of a polytope are Set.extremePoints ℝ. is the set of real matrices satisfying Matrix.PosSemidef (which includes symmetry), and the ambient space of a positive semidefinite lift is all matrices; this does not change which sets have lifts, because a lift in the symmetric matrices extends linearly and a lift in all matrices restricts to them. Positive semidefinite factorizations require both factor families to be positive semidefinite and use .
Reading decisions: the goal assumes , the paper's meaning of "a graph with vertices", since for the polytope is the image of and the printed statement fails. Milestone 3 also assumes , and so does Milestone 1 (Theorem 3.3): in the point has a proper lift to the whole space , whose dual cone cannot factor the slack matrix . In Milestone 4 the column is an arbitrary real vector. The slack matrices of Theorem 3.3 are encoded through the identification on p. 9 of the paper: rows are vertices of , columns are extreme points of the polar , the canonical entry is , and every slack matrix is the canonical one with positively scaled columns. Facets in Milestone 3 are nonempty proper exposed faces of dimension one less than the polytope.
The goal must not be weakened to proper lifts, and lifts must use equality with linear and affine; with inclusion, or with arbitrary maps, the statement becomes trivial or false. The core lemma is meaningful only with both factor families positive semidefinite; without that requirement factors trivially.
Beyond the milestones, a complete proof of the goal needs two facts the paper uses without stating them as claims of this proof: (a) an -lift that is not proper is a proper lift to a face of (p. 5), every face of is isomorphic to some with (Example 4.2, p. 12), and an -factorization yields an -factorization; (b) lifts are preserved by affine maps (Proposition 2.9, pp. 6–7), and translating a polytope changes its slack matrices only by positive column scalings, which is how Theorem 3.3 applies to , whose origin is a vertex rather than an interior point. Stating (a) and (b) as separate lemmas is welcome.
Needed infrastructure: positive semidefinite matrices and the trace pairing, the face structure of , invariance of lifts under affine maps, and conic duality for Theorem 3.3. All of these are reusable beyond this mission. Contributions welcome: proofs of the milestones, the bridging facts (a) and (b), and alternative routes to the goal.
Matroids abstract the combinatorial content of linear independence: which sets of columns of a matrix are independent, which are maximal (bases), and how bases relate to each other. This abstraction, isolated independently by Whitney (1935) and van der Waerden's school, turned out to be exactly the right level of generality for a large family of greedy and augmenting-path algorithms — a base of a matroid can always be reached from another by a sequence of single-element swaps, and this exchange property is what makes local search on bases correct and efficient.
A natural question, raised in the 1980s once matroid-based combinatorial optimization was mature, is what happens when bases are not merely present or absent but carry real-valued weights that must interact well with the exchange structure. Dress and Wenzel answered this with the notion of a valuated matroid: a real-valued function on the bases of a matroid satisfying a weighted strengthening of the exchange axiom. Their motivation was explicitly algorithmic — valuated matroids are exactly the structures for which a greedy algorithm computes an optimal basis under linear objectives, and more generally under the family of "tilted" objectives obtained by adding an arbitrary linear functional. Independently, valuated matroids arise from the classical Grassmann–Plücker relation applied to matrices over a field with a valuation (hence the name), connecting them to tropical geometry.
This mission formalizes the two theorems of Murota's Discrete Convex Analysis (2003, §2.4) that make this story precise: the classical correspondence between a matroid's base family and its rank function (Theorem 2.29), and the characterization of valuations by a perturbation-robustness property (Theorem 2.32). Theorem 2.32 is also historically the entry point of the book's central theme — it is the special case, for the two-valued lattice , of the general local-exchange criterion for M-convex functions that occupies chapters 6 and 7.
Let be a finite set (the ground set). A matroid on is a pair where , the base family, is a nonempty family of subsets of satisfying the simultaneous exchange axiom (B): for every and every , there exists such that both
Equivalently (Theorem 2.29 below), a matroid can be described by its rank function , a set function satisfying:
A valuation of a base family is a function satisfying the axiom (VM): for every and , there is with and
The pair is then a valuated matroid. For , the perturbation of by is
The right-hand side says: for every linear perturbation , the set of -maximal bases is again the base family of a matroid. The universal quantifier over is not optional — a version of this statement quantified over a single fixed is either vacuous or false, and does not capture what makes valuated matroids useful.
The maps
are mutually inverse bijections between nonempty families satisfying (B) and set functions satisfying (R1)-(R3). This is weaker groundwork than the goal, stated first because it fixes the exact axiomatic vocabulary — (B) and (R) — that Theorem 2.32 is built on.
The result itself. Theorem 2.32 is the reason valuated matroids are the right object for weighted combinatorial optimization on matroids: it says a function on bases behaves correctly under every linear re-weighting of the ground set exactly when it satisfies the local exchange inequality (VM). This is what guarantees, for instance, that a greedy algorithm which is correct for the unweighted matroid extends correctly to families of tilted objectives, and it is the germ of the general local-optimality criterion for M-convex functions (chapters 6–7), which underlies most of the algorithmic content of the rest of the book. Theorem 2.29 is the classical result — due jointly to the development of matroid theory from the 1930s onward — that the base-exchange and rank-submodularity axiomatizations of a matroid carry the same information; it is the finite, unweighted precursor of Theorem 2.32.
Formalizing it. Neither theorem has a machine-checked proof on the platform prior to this
mission (see Formalization scope for the prior-art check). Theorem 2.29's own proof is
elementary but has two independent halves (each map preserves its target axiom class, and the
two maps compose to the identity in both directions) that must all be established; Theorem
2.32's proof, as given in the source, defers entirely to a later, more general chapter-6
theorem, so a solver working only from this mission must either reconstruct a direct
combinatorial argument for this special case or await chunk 06 (DiscreteConvex.MConvexFunctions,
a separate mission) and specialize its main theorem.
The obvious approach to Theorem 2.32 — fix an optimal basis for and try to
show the exchange condition on maximizers directly from (VM) — proves one direction (VM implies
the maximizer property) in a few lines, since perturbing does not change which exchange moves
are available. The converse is the substantial direction: from "the maximizer set is always a
matroid, for every ," one must recover the single global inequality (VM) that must hold for
all pairs , not just optimal ones. The standard argument constructs, for
a given non-optimal pair, a perturbation under which that specific pair becomes
simultaneously optimal, and this construction is exactly the step the book skips by citing
chapter 6's general theorem. A formalization attempting to bypass this by only checking the
maximizer property for a finite or generic sample of perturbations would trivialize the
statement to something false or vacuous — a pitfall the goal's explicit ∀ p is designed to
prevent.
The ground set is a Fintype with DecidableEq; is represented as
Finset (Finset V), and as a plain function type. The rank function is
-valued (matching the book's own convention for matroid rank, as opposed to the
-valued conventions used from chapter 6 onward for general M-convex functions);
RankOfFamily is implemented with Finset.sup over rather than a partial max',
so that it is a total function — its junk value at the empty family is never invoked, since
every hypothesis in this mission supplies nonemptiness explicitly, matching the book's own
phrasing.
A trivializing formalization of the goal is one that quantifies over a single fixed , or allows to be empty; both are explicitly excluded by keeping a hypothesis and universally quantified inside the theorem statement itself.
Checked against Mathlib (commit 0df444a360eaa60ab8c11dca51a86af692955474): Mathlib's
Matroid structure is axiomatized via the single-element (asymmetric) exchange property,
classically but not definitionally equivalent to Murota's simultaneous axiom (B) used
throughout this book, and Mathlib provides no constructor recovering a base family or a
Matroid from a bare rank function satisfying (R1)-(R3). Theorem 2.29 is therefore genuine,
reusable infrastructure, not a restatement of existing Mathlib API. No reference item was found
on the platform for either theorem (GET /theorems?q=matroid, q=valuated matroid return only
unrelated tropical-geometry and k-server results). Contributions to a shared
DiscreteConvex.Combinatorial definitions layer (the exchange and rank axioms) are welcome
from later chunks of this series that build on matroid or base-polyhedron structure.
Many decision problems under uncertainty take the form of a stochastic program: choose a decision from a feasible set to maximise the expected utility , where the distribution of the uncertain parameter is known only through i.i.d. samples . The standard remedy, sample average approximation, maximises instead. Its consistency (convergence of the optimal expected utility of its solutions to the true optimum) is classical, but it needs regularity assumptions of its own, for example those of King and Wets (Stochastics and Stochastic Reports, 1991), cited on p. 98 of the paper; the paper presents its construction as a route to consistency under weaker conditions.
Robust optimization (RO) takes a different route: it protects each sample by an uncertainty set and optimises against the worst point in it. Xu, Caramanis and Mannor (Math. Oper. Res. 2012) show that RO over several overlapping uncertainty sets is equivalent to a distributionally robust stochastic program (their Theorem 2.1, the subject of mission I of this series). Section 3 of the paper uses that equivalence to show that a specific robustification of the sampled problem, with boxes of shrinking radius around each sample, is consistent under only boundedness and equicontinuity of . This mission formalizes that result, Theorem 3.1.
Equip with the sup norm , its Borel -algebra and Lebesgue measure . The data are:
For a sample the boxes are , and the box-robust sample objective is
The RO solution is a maximiser of over . The equicontinuity modulus of is
The proof works with the distribution set of probability measures with for every , and with the uniform box kernel density estimator
Assume for all ; as ; and . Then for every choice of maximisers , with probability one,
Milestones 1–4 are deterministic statements about a fixed sample; milestone 5 is the only probabilistic input.
Theorem 3.1 gives consistency of a tractable robust reformulation of a sampled stochastic program under conditions the paper notes are weaker than those of King and Wets for sampled stochastic programs: need only be bounded and equicontinuous in , uniformly in , and the true distribution need only have a density. It also gives an explicit schedule for the size of the uncertainty set, with , the bandwidth condition of kernel density estimation. Section 4 of the paper applies the same distributional interpretation to regularised learning methods such as the support vector machine and the Lasso.
The result is proved in the paper, with the consistency of kernel density estimators (Devroye 1983; Devroye and Györfi 1985) cited rather than proved. No part of it is formalized in Lean or on this platform as far as a search of the platform found. A complete development would produce, besides Theorem 3.1, a machine-checked strong consistency theorem for kernel density estimators, which is a basic result of nonparametric statistics in its own right.
The deterministic part (milestones 1–4) is measure-theoretic bookkeeping: the kernel integrates to one only because the box is a sup-norm ball of volume , and every infimum and supremum must be handled with care, since need not attain them.
The obstacle is milestone 5. Almost-sure convergence of to an arbitrary density , with no continuity or support assumption, does not follow from the strong law of large numbers applied pointwise: is an average of terms whose law changes with through , and almost-sure convergence at each fixed does not give convergence of the integral along a single sample path. The theorem needs both a bias estimate valid for every integrable density and a concentration estimate for the random error. Mathlib has Lebesgue differentiation and the strong law, but no kernel density estimator and no such concentration result.
Fin m → ℝ, whose Mathlib norm is the sup norm; boxes are Metric.closedBall. The integrals are Bochner integrals against Lebesgue measure of integrable integrands.X : ℕ → Ω → Fin m → ℝ on a probability space, independent (iIndepFun) and each with law volume.withDensity h*; become X 0, X 1, …, and the -th problem uses the first . "With probability one" is ∀ᵐ ω ∂P.