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?
Combinatorial optimization problems are routinely solved by writing the convex hull of their feasible solutions as the feasible region of a linear program. When that convex hull has exponentially many facets, a classical trick is to add auxiliary variables: a polytope with many facets may be the linear projection of a higher-dimensional polyhedron with few. The spanning tree polytope, the permutahedron and the parity polytope all have compact descriptions of this kind. This raises the question of whether every polytope of an NP-hard problem might also have one, which would yield a polynomial-size linear program for that problem.
In the late 1980s several papers claimed polynomial-size linear programs for the traveling salesman problem (TSP). Yannakakis (STOC 1988; JCSS 1991) refuted all such claims at once by showing that every symmetric extended formulation of the TSP polytope has exponential size. He asked whether the symmetry assumption could be removed. Fiorini, Massar, Pokutta, Tiwary and de Wolf (STOC 2012; J. ACM 2015) answered the question: every extended formulation of the TSP polytope, symmetric or not, has inequalities.
Timeline.
Let be a finite index set. An extended formulation (EF) of a set is a linear system , in variables such that exactly when some satisfies it. Its size is the number of inequalities. The extension complexity is the least size of an EF of .
A polytope is the convex hull of finitely many points. A face of is itself or its intersection with a valid hyperplane, and a facet is a maximal proper face. A polytope is an extension of if for some linear map . Given , the slack matrix has entries . The nonnegative rank is the least with , where has columns and has rows.
For -bit strings , is the number of common ones, and is the matrix . A 1-monochromatic rectangle cover of its support is a family of products , each containing only entries with , that together contain all of them.
On the complete graph , is the characteristic vector of an edge set and is the cut of . The polytopes are
The constant is left unfixed, so the goal survives any improvement of it.
The theorem rules out every polynomial-size linear programming formulation of the TSP polytope, in any number of auxiliary variables, which settles Yannakakis's question. The cut polytope bound does the same for max-cut, and the stable set bound for the stable set problem on general graphs. The results do not depend on P vs NP: they concern one specific model of computation, linear programs whose feasible region projects onto the polytope. They started a line of work on extension complexity, including perfect matching (Rothvoss), approximate EFs and semidefinite lifts.
Formalizing the result would produce a machine-checked chain from a communication-complexity bound to a polyhedral one. The paper's results are proved; the input of Theorem 1, Razborov's bound, is only cited, and is posed here as a separate target. To our knowledge none of these statements has a formal proof in Lean or another proof assistant. The polyhedral layer (Yannakakis's theorem, faces and extensions) and the matrix layer (nonnegative rank, rectangle covers) can be reused for later extension-complexity results.
The obvious approach, bounding the number of facets of the TSP polytope, does not work: extended formulations exist precisely because a projection can have far more facets than the lifted polyhedron. Any lower bound must cover every lifting at once, which means working with the nonnegative rank of a slack matrix rather than with any concrete formulation. Ordinary rank is no help, because has rank . The step that carries the weight is Razborov's distributional bound for disjointness, a nontrivial piece of communication complexity. On the polyhedral side, Lemma 11 needs a reduction from 3SAT to a directed and then an undirected Hamiltonian cycle problem, realized as a face of with . Theorem 12 also needs a monotonicity of in that the paper only indicates.
Sym2 (Fin n)). is indexed by ordered pairs, and the Frobenius product is the dot product over ordered pairs. Bit strings are Fin n → Bool.sInf of the attainable sizes), never , so no lower bound can hold through an infinite value. The size of an EF counts inequalities only.A shop that promises delivery dates is judged by how late its orders are, not by how early. For a single machine processing jobs that are all available at time , the total tardiness of a processing order,
charges each job the amount by which its completion time exceeds its due date , and nothing for finishing early. It is one of the basic criteria of deterministic scheduling (Conway, Maxwell and Miller, Theory of Scheduling, 1967), and the single-machine problem of minimizing it is the core subproblem of many dispatching and decomposition methods.
Two contrasting rules are classical. Sequencing in order of shortest processing time (SPT) minimizes total lateness and total completion time (Smith, 1956), and it minimizes total tardiness when every job is tardy under it. Sequencing by earliest due date (EDD) minimizes total tardiness when at most one job is tardy under it. Between these extremes no simple rule is optimal, and before 1969 the proposed exact methods (Held and Karp, 1962; Lawler, 1964; Elmaghraby, 1968) searched subsets of schedules.
Timeline.
This mission formalizes Emmons's SPT side: the pairwise dominance theorem for a shorter job before a longer one, and its corollary that the SPT schedule is optimal under a condition far weaker than "every job is tardy".
A finite set of jobs is processed on one machine. Job has a processing time and a due date . A schedule of is an ordering of the jobs of ; the machine starts at time , never idles, and processes the jobs in that order, so a job's completion time is the sum of the processing times of the jobs up to and including it. Its tardiness is , and the schedule's total tardiness is . A schedule is optimal if no schedule of has smaller total tardiness.
Following Emmons, jobs are SPT-indexed: are numbered so that implies , or and . The SPT schedule processes in this order.
Emmons's notation (" precedes in an optimal schedule") means that there exists an optimal schedule having all properties already established and in which comes before . The set collects the jobs already known to precede .
The condition can be read as with the SPT completion time of , so it allows jobs to be early. It is the paper's sufficient condition for SPT optimality, and the conclusion is optimality against every schedule of .
Two further results are included as supporting statements: Corollary 1.2 (p. 705, last) and Corollary 2.3 (p. 707, the adjacent-pair rule iff after a waiting time ).
Corollary 1.4 turns an NP-hard problem into a closed-form answer on a recognizable class of instances: one pass over the SPT order checks the condition, and if it holds no search is needed. Theorem 1 is the more general tool. It orders pairs of jobs in an optimal schedule, and together with Emmons's companion theorems it underlies later exact methods for total tardiness, including Lawler's decomposition and the branch-and-bound algorithms that use Emmons's dominance rules for pruning.
The results are proved in the paper. What a formalization adds is a checked account of the step that the paper treats informally: dominance statements are existential ("some optimal schedule has before "), and the paper argues on p. 702 that such statements can be accumulated. Each statement here makes explicit which previously established properties the new optimal schedule keeps. No machine-checked proof of these results was found on Prove2Me or in Mathlib at the time of drafting.
The obvious argument is a pairwise interchange, but the interchanged jobs are not adjacent. Moving from before to 's position shifts every job in between, changes two tardiness terms in different directions, and the comparison depends on where the due dates fall relative to the start of and the end of . The hypothesis involving only controls the start time of through the information that precedes it, so the existence statement must carry that information along.
The goal is not a direct consequence of Theorem 1 applied pairwise: existential conclusions for different pairs need not hold in a common optimal schedule. Optimality of one fixed order requires all the pairwise decisions to be realized simultaneously, and the problem changes (due dates shift) once a job is fixed in place.
Jobs are elements of a type with a linear order that plays the role of the paper's index, and the job set is a Finset ι; this lets the reduction remove a job and keep the remaining labels. Schedules and completion times are the published definitions MooreLateJobs.Shared.IsSchedule and MooreLateJobs.Shared.completionTime (duplicate-free lists containing exactly the jobs of ; prefix sums of processing times from time ). Tardiness, total tardiness, optimality (against every schedule of ), "precedes" (comparison of positions), the SPT indexing convention and the SPT schedule (the jobs sorted by index) are defined in EmmonsTardiness.SPT.Model. Processing times and due dates are real.
Conventions and deviations from the page:
A formalization of the goal as "some optimal schedule starts with ", or of Theorem 1 with an arbitrary set unrelated to optimal schedules, would be a different and weaker (or false) statement; the targets above state optimality of the SPT schedule itself and tie to an optimal schedule.
Needed infrastructure: lemmas on prefix sums of lists, on the effect of a transposition on positions in a duplicate-free list, on removing the head of a schedule, and existence of an optimal schedule among the finitely many permutations of . These list-scheduling lemmas are reusable for other single-machine results (Moore 1968, and the EDD mission of this series). Proofs of the milestones, alternative arguments, and general interchange lemmas are all welcome.
A function that is bounded below need not attain its infimum: on has infimum and no minimizer. The classical "variational principle" says that at a minimizer of a differentiable functional, . Without compactness there may be no minimizer, and the principle has nothing to say. In 1974 Ivar Ekeland showed that a weaker statement survives in every complete metric space: next to any approximate minimizer lies a point that is the exact, strict minimizer of a slightly perturbed function (Ekeland 1974).
The result is now a standard tool in nonlinear analysis, optimization and the calculus of variations. It yields approximate first-order conditions () without existence of minimizers, approximate Lagrange multiplier rules, and approximate maximum principles in optimal control; Ekeland's survey (Ekeland 1979) collects many of these uses.
Timeline. Bishop and Phelps introduced the partial order on a Banach space times that underlies the proof, in their study of support functionals of convex sets (Bishop–Phelps, The support functional of a convex set, Proc. Symp. Pure Math. 7, AMS, 1963). Brøndsted and Rockafellar used it in 1965 to obtain subdifferentiability properties of convex functions on Banach spaces (Brøndsted–Rockafellar 1965), and Browder applied it to nonconvex subsets of Banach spaces (Bull. AMS 79, 1973). Ekeland's 1974 article, formalized here, isolates the device as a principle valid in every complete metric space for lower semicontinuous functions with values in , and applies it to Gâteaux-differentiable functions, constrained optimization, Plateau's problem, geodesics and optimal control.
Let be a complete metric space. Let be lower semicontinuous (for every the set is closed), not identically , and bounded from below:
For , a point is an -minimizer if
For , the Bishop–Phelps order on is
In Lean it is EkelandVP.General.bpLE α p q, read . The epigraph of is (1.15).
In §2, is a real Banach space with dual , and is Gâteaux-differentiable with derivative (EkelandVP.General.IsGateauxDiff F F'): at every with , for every (2.1).
For every satisfying (1.2) and every there is with
The parameters and are free; the trade-off between closeness to and the size of the perturbation is the content of the theorem.
The result. Theorem 1.1 replaces "a minimizer exists" by "a strict minimizer of a Lipschitz perturbation exists nearby", with explicit control of both the distance and the perturbation. With this gives a point that is -optimal, -close to , and -stationary in the metric sense. Corollary 2.3 is the form announced in the paper's abstract: a differentiable function with a finite lower bound has points where is almost minimal and is arbitrarily small. Later sections of the same paper use Theorem 1.1 for approximate Lagrange multiplier rules (§3) and an approximate Pontryagin maximum principle (§7), which are the subjects of missions II and III of this series.
Formalizing it. The theorem is proved; this mission formalizes the paper's own route (the order (1.6), Lemma 1.2, then Theorem 1.1) and its first applications in §2. The pinned Mathlib has no statement of Ekeland's principle, of the Caristi fixed point theorem, or of the Bishop–Phelps order, and the platform has none either. A machine-checked Theorem 1.1 for extended-real-valued functions would be directly reusable by every later mission that needs approximate optimality without compactness.
The obvious argument — take a minimizing sequence and pass to a limit — fails because nothing makes a minimizing sequence converge: is not compact, and a minimizing sequence of escapes to . Completeness only helps for Cauchy sequences, so one must construct a sequence that is Cauchy. The limit must moreover be maximal for the order (1.6), not merely a limit point, and that maximality is what produces the strict inequality (1.5). Lemma 1.2 is where this difficulty sits. In §2, the passage from the metric statement (1.5) to a bound on requires to be finite near along every line, which the Gâteaux hypothesis supplies.
MetricSpace with CompleteSpace; is dist u v. carries the product topology; only closedness of subsets of it is used.EReal. "Bounded from below" (1.1) is ; it also excludes the value , which the paper's codomain does not contain. "Not identically " is . Lower semicontinuity is Mathlib's LowerSemicontinuous.lam.EReal subtraction is ordinary.NormedSpace with CompleteSpace, is a function , and Gâteaux differentiability requires to be finite near before taking a real derivative; without this, EReal.toReal would let an infinite function have a junk derivative. Density of is stated for derivatives taken at points where .Contributions welcome: proofs of the milestones (the first two are short; Lemma 1.2 is the core), of Theorem 1.1, and of the §2 corollaries; a reusable Caristi fixed point theorem built on the same order would be a natural addition.
A single server shared by several classes of jobs must decide, at every moment, which class to serve. Different scheduling rules give different mean response times to the classes, and a system designer often starts from the other end: a target vector of mean response times, one per class, and the question whether any rule can meet it. Coffman and Mitrani answered this question for the multiclass M/M/1 queue in A Characterization of Waiting Time Performance Realizable by Single-Server Queues (Operations Research 28 (1980), 810–821). Their answer is a polytope with an explicit description: the response-time vectors that can be realized are exactly the convex combinations of the vectors of the preemptive priority rules, and these are exactly the vectors satisfying one equation and inequalities.
The starting point is Kleinrock's conservation law (Kleinrock, Naval Res. Logist. Quart. 12 (1965)): a weighted sum of the response times does not depend on the rule. The characterization is the first instance of what was later called the achievable region method, developed for general multiclass systems by Federgruen and Groenevelt (Oper. Res. 36 (1988)), Shanthikumar and Yao (Oper. Res. 40 (1992)) and Bertsimas and Niño-Mora (Math. Oper. Res. 21 (1996)), and used to derive priority-index policies such as the rule and Gittins indices.
There are job classes. Jobs of class arrive in a Poisson stream at rate and have exponential service times with parameter . The traffic intensity of class is , and the system is stable: . A performance vector lists the mean response times of the classes. Write , , and for a set of classes
In Lean the data are a structure Params M carrying and the three standing assumptions; Params.f, Params.Hss (), Params.prioVec, topSet and Params.H are the objects above.
The paper's Theorem 2 says a vector is achievable by a scheduling strategy iff it lies in ; its proof is the chain , where is the achievable set. The goal is the part of the chain that involves no strategies.
A further item states the paper's final remark (§4): every linear cost is minimized over at some preemptive priority vector.
The theorem turns a question about all scheduling rules into a finite check: a target vector is realizable iff it satisfies (1) and the inequalities (4), and every realizable vector is realized by randomly mixing at most priority rules. Linear costs over the realizable vectors are minimized by a priority rule, the fact behind the optimality of priority-index rules in multiclass queues. The paper also gives a linear program for finding the mixture.
The result has been proved since 1980. No machine-checked proof of it is known. The Prove2Me library holds the abstract generalized conservation law theorem of Gittins, Glazebrook and Weber (AllocationIndices.achievable_region_theorem, included as a reference item), which assumes the inequalities (4) for every policy and whose polytope also imposes nonnegativity; it does not compute the right-hand sides for the M/M/1 queue, does not prove that the priority vectors satisfy (4), and uses equality on the lowest-priority sets rather than the highest. This mission supplies the concrete polytope, the closed form of the priority vectors and the strict supermodularity of .
That the priority vectors lie in is a family of inequalities between ratios , one for each pair of a priority order and a set , and the order and need not interact in any simple way. The reverse inclusion is a statement about vertices: a vertex is determined by tight constraints, and one has to show that they form a chain. This needs strict inequalities with the right direction for every crossing pair of sets, which is where the positivity of every is used. If some , then appears in no constraint, is unbounded and the goal is false. Finally, uses only points, not all , so the goal contains a Carathéodory-type bound for the hyperplane of (1).
Classes are Fin M, numbered from . A priority order is π : Equiv.Perm (Fin M) with π r the class of rank r, rank highest. "Vertex" is an element of Set.extremePoints ℝ. The points of (3) are prioVec (σ k) for an arbitrary σ : Fin M → Equiv.Perm (Fin M), so repetitions are allowed. The priority vectors are given by their closed form, not as solutions of a system. The goal assumes ; for the set is empty.
The paper's notion "achievable by some scheduling strategy" is replaced by its analytical characterization : the strategy class of the paper (Assumptions 1–3, p. 812) is described only in prose and the steady-state means are assumed to exist, so the queueing half of the proof (Theorem 1, Lemma 1 for arbitrary strategies, the conservation law itself) is not stated. The goal is not to be stated on an abstract set satisfying hypotheses that encode Lemma 1 and (1); that form is already proved and drops the content of milestone 4. The conservation law is an equality, never the inequality (4) at the full set.
A complete development needs finite-set sums, the extreme points of a polyhedron and a Carathéodory argument in an affine hyperplane; the inequalities of milestones 2 and 3 and the vertex-chain argument are reusable for any strictly supermodular set function. Proofs of any milestone, and alternative proofs of the goal through polymatroid theory, are welcome.
When many independent users share a resource whose cost grows with use (links of a network, servers, machines), each user chooses for itself, and the outcome is a Nash equilibrium rather than a socially optimal allocation. The price of anarchy, introduced by Koutsoupias and Papadimitriou (STACS 1999), measures the cost of this decentralisation: the worst ratio between the social cost of an equilibrium and the optimal social cost. It has become a standard yardstick in algorithmic game theory, network routing and the design of distributed protocols.
Christodoulou and Koutsoupias (STOC 2005) determined the price of anarchy of finite congestion games with linear latencies, the atomic, unweighted counterpart of selfish routing. This mission formalizes the central entry of their table: pure equilibria, general (asymmetric) strategy sets, and the average social cost.
Timeline:
A congestion game has a finite set of players, a finite set of facilities, for every player a set of pure strategies (each a set of facilities), and for every facility a latency function giving the cost of to each of its users as a function of how many users it has. A pure strategy profile picks for each player. The load is the number of players with , and player pays
The profile is a pure Nash equilibrium if no player can lower its cost by switching alone: for all and all , where replaces by . The social cost is , which is times the average cost of a player. Latencies are linear: with . The game is asymmetric in the sense that each player has its own strategy set (symmetric games, where all coincide, are a special case).
The pure price of anarchy of the average social cost is
the minimum taken over pure strategy profiles. In Lean these objects are CongestionGame, load, cost, IsProfile, IsPureNash, sumCost and IsLinear in the namespace CongestionPoA.AsymSum.
The goal theorem pure_poa_sum_eq_five_halves is the conjunction of Theorems 1 and 2 of the paper:
The first part is the upper bound; the second shows that it is attained for every number of players from three on.
The value is the benchmark for atomic congestion with affine costs. It is the reference point for the later results of the paper (the symmetric case , the maximum social cost , mixed equilibria ) and for a large literature on coordination mechanisms, taxes and the price of stability, which compare their guarantees against it. The bound is also the standard example of what later became the smoothness framework, through which the same constant governs mixed and coarse correlated equilibria and hence no-regret learning outcomes.
Both theorems are proved in the paper; nothing here is open. The proofs for affine latencies, however, are only indicated: the paper displays the identity case and states that the arguments extend. The mission states the affine case and asks for complete machine-checked proofs, including the lower-bound construction, which the paper describes and declares "not hard to verify". No machine-checked proof of these results is on the platform.
The Nash conditions give one inequality per player, each mixing the equilibrium loads with the strategies of the comparison profile. Bounding the loads crudely, for instance by the number of players, gives a ratio that grows with ; the constant requires comparing the cross term with both social costs simultaneously and with the right weights. The integrality of the loads matters at that point: the natural pointwise inequality is false for real arguments, so a proof that treats loads as real numbers cannot reach .
For the lower bound, a Nash equilibrium must be verified against every unilateral deviation of every player, for all at once, in a construction with cyclic indices. The case is genuinely different (the paper states that its price of anarchy is ), so the argument has to use .
Players and facilities are finite types; a profile is a map from players to finite sets of facilities, and feasibility () is a separate predicate. Latencies are real-valued functions of the natural-number load, and "linear" means affine with nonnegative coefficients. The upper bound is stated multiplicatively, for every Nash and every feasible , which is equivalent to and avoids dividing by . The lower bound quantifies over players Fin N, , and existentially over a finite facility type, a linear game, a Nash equilibrium and an optimal feasible profile of positive social cost. The positivity rules out the trivializing witness: in the all-zero latency game every profile is a Nash equilibrium and . The Nash condition is the paper's cost form; it agrees with the payoff-form AGT.IsPureNash of agt_games for payoffs .
Trivializing formalizations are ruled out: the comparison profile must be feasible (otherwise could be by letting players use no facility), the upper bound covers all affine latencies rather than only , and the lower-bound instance must have linear latencies with nonnegative coefficients.
A complete development needs finite double counting (regrouping by facilities), monotonicity of affine latencies, and a decidable or explicit check of the lower-bound game. The congestion-game layer is reused by the other missions of this series. Proofs of individual milestones, and alternative proofs of the upper bound, are welcome.
In many statistical applications the number of unknown parameters is far larger than the number of observations : gene-expression studies with tens of samples and thousands of genes, imaging problems with fewer measurements than pixels, and nonparametric curve estimation from finitely many noisy samples. Least squares is useless in this regime, since the system is underdetermined. If the parameter is sparse (only a few of its entries are nonzero), estimation becomes possible, and the question is how accurate a computationally tractable estimator can be.
Candès and Tao (arXiv:math/0506081; Ann. Statist. 35(6), 2007, doi:10.1214/009053606000001523) introduced the Dantzig selector, an estimator computed by a linear program, and proved that its squared error is within a factor of order of the error of an oracle that knows where the nonzero entries are. The paper, with its discussion in the same issue, is one of the founding results of high-dimensional sparse regression, alongside the Lasso analysis of Bickel, Ritov and Tsybakov (arXiv:0801.1095).
Timeline. Candès and Tao (2005, arXiv:math/0502327) showed that minimization recovers a sparse vector exactly from noiseless data when the restricted isometry constants of the design satisfy . The Dantzig selector paper (first posted 2005, published 2007) carried this to Gaussian noise, with the error bound formalized here (Theorem 1.1) and an oracle inequality (Theorem 1.2). Bickel, Ritov and Tsybakov (2009) replaced the restricted isometry hypothesis by weaker restricted eigenvalue conditions and showed that the Lasso and the Dantzig selector behave alike.
Observe from the linear model
where is a deterministic design matrix with columns , each of Euclidean norm ; is an unknown deterministic parameter; and is a vector of independent random variables with . The vector is -sparse if at most of its entries are nonzero.
For let be the submatrix of the columns indexed by . The restricted isometry constant is the smallest with
for all and all coefficient vectors ; the restricted orthogonality constant (for ) is the smallest with for all disjoint with , .
Given a tuning parameter , the Dantzig selector is any solution of
Let , , -sparse, and . For every , with , with probability exceeding the program has a solution and every solution satisfies
For this is , display (1.10) of the paper. The constant is the one the paper's proof establishes (see Formalization scope).
The result. Theorem 1.1 shows that an estimator computable by linear programming reaches, up to the factor and the constant , the squared error that least squares would attain if the support of were known in advance, even when . The factor is the price of not knowing the support; the paper argues (p. 5) that, apart from this factor, (1.10) is unimprovable in general. The bound is non-asymptotic, with an explicit constant and an explicit failure probability, and it holds for every -sparse simultaneously in the sense that the good event (the noise being nearly orthogonal to every column) does not depend on . Its deterministic part, Lemma 3.1, is reused verbatim in the proof of the paper's oracle inequality (Theorem 1.2) and became a standard tool in compressed sensing.
Formalizing it. The result is proved, and to our knowledge no machine-checked proof exists. A formalization produces a checked version of the cone-and-tube argument behind most -recovery guarantees, a Lean statement of the restricted isometry machinery for noisy data, and a checked Gaussian maximal inequality usable for other high-dimensional estimators. It also settles the exact constant: the paper prints , while its proof gives in place of .
Lemma 3.1 is the main obstacle. The obvious approach bounds directly through restricted isometry, and it fails because the error is not sparse: it spreads over all coordinates, and restricted isometry controls only on vectors with at most nonzero entries. The two constraints (3.2) and (3.3) only say that is concentrated in on the coordinates of and that is small coordinatewise, and turning that into an bound on all of is where the work lies. In Lean this requires bookkeeping that is routine on paper: ordering the coordinates of off by magnitude, with ties and a possibly incomplete last group of coordinates, and working with the span of a selected set of columns. On the probabilistic side, the tail bound needs the law of (a weighted sum of independent Gaussians), a sharp Gaussian tail estimate of Mills-ratio type, and a union over events. A cruder sub-Gaussian bound would not give the stated failure probability.
Indices are Fin n and Fin p; vectors are functions into ℝ. The norms, the column and the constants , are the published definitions CandesTao_Decoding_Norms and CandesTao_Decoding_RestrictedIsometry (the smallest admissible constants, via sInf), from the formalization of Candès and Tao's Decoding by Linear Programming. The noise is a family z : Fin n → Ω → ℝ on a probability space, mutually independent (iIndepFun), each coordinate with law gaussianReal 0 σ². The constraint is coordinatewise. A Dantzig selector is any minimizer; uniqueness is not assumed. Section 3 works with ; the goal is stated for general .
Committed conventions and corrections:
A trivializing formalization is excluded: the hypothesis is on the actual least constants of , not on free parameters, and it is satisfiable (for instance by , where both constants vanish).
Needed infrastructure: sums of independent real Gaussians (Mathlib has gaussianReal and its convolution), a Mills-ratio tail bound, a sorting-based block decomposition of a Finset, and orthogonal projection onto the span of finitely many columns. The block decomposition and the tail bound are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 3.1.
A single server shared by several classes of customers is the basic model of scheduling under uncertainty: jobs of different types arrive at random, need random amounts of work, and a scheduler decides at every moment which type to serve. A classical way to optimize such a system, the achievable region approach, describes the set of all performance vectors that some scheduling policy can attain, and optimizes a linear cost over that set with linear programming. For the multiclass M/M/1 queue under preemptive, work-conserving scheduling, this set is a polyhedron described by conservation laws (Coffman and Mitrani, 1980; Gelenbe and Mitrani, 1980; Shanthikumar and Yao, 1992): it is the base of a polymatroid, its vertices are the performance vectors of the strict priority rules, and minimizing a linear cost over it is solved greedily, which recovers the rule.
That description uses one inequality for every nonempty set of classes, constraints in all. Bertsimas, Paschalidis and Tsitsiklis (working paper 1992, Annals of Applied Probability 1994) derived performance bounds for general multiclass networks from quadratic potential functions. Specialized to one station, their nonparametric method produces a different polyhedron, in variables with constraints, and they show that its projection is exactly the conservation-law polyhedron (Theorem 8.4). The paper remarks that this confirms, for this polymatroid, the belief that problems solvable in polynomial time admit polynomial-size formulations.
There are customer classes . Class has arrival rate and service rate ; its traffic intensity is , and the queue is stable: . For define
In the queue, is the steady-state mean number of class customers and their mean remaining work; is the mean work of the classes in when those classes have preemptive priority over the rest.
The performance polymatroid P1 (Theorem 8.3) is the set of with
For a permutation of , the vector is the solution of the triangular system , (Eq. (58) with ).
The extended formulation P2 (Theorem 8.4) is the set of nonnegative and satisfying
In the queue, is the steady-state mean of the number of class customers on the event that the server is busy with class . The projection of P2 is the set of for which some makes a point of P2.
Both inclusions are part of the goal. The statement fixes no constants and holds for every , every positive rate vector and every stable load.
The result. Theorem 8.4 replaces constraints by constraints in variables without changing the projected set. Any linear program over the M/M/1 performance region, including problems with side constraints where the greedy rule no longer applies, can then be solved with a polynomial-size LP. It also identifies the paper's nonparametric method as exact at a single station: the method loses nothing there, which is the baseline against which its gaps in networks are measured.
Formalizing it. The result is proved in the paper, but the reverse inclusion is argued through achievability: every point of P1 is the performance of some (randomized) policy, and every policy's performance satisfies the equations of P2. That argument rests on stochastic objects (invariant distributions under arbitrary policies, and time-0 randomizations over priority rules) that the paper does not define precisely. The paper points to a purely combinatorial derivation in Paschalidis' thesis, which we have not seen. A machine-checked proof of the polyhedral identity is therefore new content: it supplies the deterministic argument the paper delegates. The polymatroid structure of P1 (Milestone 1) is classical for supermodular set functions; this mission requires it for this specific . We know of no formalization of either result.
The inclusion only combines the equations of P2 with nonnegativity. The reverse inclusion is the hard half: for each point of P1 one must exhibit a nonnegative matrix satisfying linear equations, and the inequalities of P1 say nothing directly about the off-diagonal entries . The paper's own argument does not help here, since it produces as a steady-state expectation under a scheduling policy, an object defined through a Markov chain and given in no closed form. The sign constraints are where the inequalities of P1 are encoded, and a proof has to explain how sign conditions on auxiliary variables carry exactly the information of exponentially many inequalities in the original ones.
Classes are Fin n; rates are real functions lam mu : Fin n → ℝ with 0 < lam i, 0 < mu i and ∑ i, lam i / mu i < 1. The paper's is written x i, because n is the number of classes. A point of P2 is a pair (x, I) with I i j , including the diagonal entries. P1 is the platform definition AllocationIndices.achievablePolytope with the matrix : inequality for every , equality at , nonnegativity. The paper writes for the class set in (65) and (71); every such sum runs over all classes. The constraints (64)–(65) bound , not . is given by its closed form, , which solves (58). The standing hypothesis is presupposed by the model (Poisson arrivals at rate ); the load condition is the paper's stability condition and keeps every denominator of positive.
No statement involves a policy, a Markov chain or an expectation; the queueing meaning above is motivation only. In particular, neither "P1 is the achievable region" nor "the performance vector of each priority rule is achievable" is formalized. The goal is the full set identity: stating only , or assuming as a hypothesis of the goal, would not be Theorem 8.4.
A complete development needs: supermodularity of under the load condition; the greedy (Edmonds) description of base polytopes of supermodular functions, which is reusable well beyond this mission; and a nonnegative solution of the P2 system at each . Contributions of any of these as separate lemmas are welcome.
Many algorithms in operations research and computer science have tunable parameters: sequence-alignment weights, clustering linkage interpolations, branch-and-bound branching rules, auction reserve prices. In data-driven algorithm design the parameters are chosen by optimizing average performance over a training set of problem instances drawn from an unknown application-specific distribution. The question this mission is about is statistical: how many training instances suffice for the empirical average performance of every parameter setting to be close to its expected performance?
Classical learning theory answers this through the pseudo-dimension of the class of utility functions (Pollard, 1984): a bound on the pseudo-dimension gives a uniform convergence bound of order . The difficulty is that utility functions of combinatorial algorithms are wildly discontinuous in the parameters, so standard tools (Lipschitz arguments, linear classes) do not apply. Balcan, DeBlasio, Dick, Kingsford, Sandholm and Vitercik (arXiv:1908.02894v4, STOC 2021) observed that for a large family of algorithms the utility on each fixed instance is a piecewise-structured function of the parameters, and proved a single general theorem converting that structure into a pseudo-dimension bound. Earlier analyses (for example Gupta and Roughgarden 2017; Balcan, Nagarajan, Vitercik and White 2017) derived such bounds one algorithm family at a time; Theorem 3.3 unifies them.
Let be a set of problem instances and a class of utility functions; in the paper for a parameter space , with the performance of the algorithm with parameter on instance .
Pseudo-dimension. A class of real functions on a domain shatters points if there are targets such that every one of the patterns of "above / not above " at the points is realized by some . The pseudo-dimension is the largest for which some points are shattered. For -valued classes it is the VC-dimension .
Dual class (Definition 3.1). For , each gives an evaluation map , , and . For utility functions, : the dual function of instance records performance on as the algorithm varies.
Piecewise decomposability (Definition 3.2). Given a class of boundary functions, a class of piece functions and , a class is -piecewise decomposable if every admits and, for each bit vector , some , with where . The theorem applies this to , so and , and their duals , are classes of functions on and .
Suppose is -piecewise decomposable, , , and . With and ,
This is the explicit bound behind the printed ; it is what the paper's proof establishes.
Theorem 3.3 is the engine behind every generalization guarantee in the paper. It is instantiated for piecewise-constant and piecewise-linear duals over (Lemmas 3.8–3.10), and through them for sequence alignment, RNA folding, hierarchical clustering, integer programming (branch-and-bound), greedy algorithms and auction design. Combined with the classical uniform convergence bound, it says that training instances suffice to tune any such algorithm to within of its optimal expected performance. The matching lower bounds in the paper (Theorems 4.3 and 5.2) show that the bound is tight up to logarithmic factors.
The result is proved in the paper; to the best of available records it has not been machine-checked. The mission formalizes the known proof, including the dual-class version of Sauer's lemma and the counting argument over the partition induced by the boundary functions. The published Sauer's lemma FoundationsML.RademacherVC.sauer_lemma is included as a reference item, as it is the tool Lemma 3.4 cites.
The obvious approach, bounding the pseudo-dimension of directly from the complexity of and , fails: the piecewise structure lives on the dual side, and nothing about or themselves controls how labels instances. The bound has to pass through dual classes twice and through the dual of a dual once, and Sauer's lemma, which counts labelings of fixed points by varying functions, must be applied in the transposed direction. Formally, the counting step needs bookkeeping of label vectors under a partition indexed by boundary functions, and a conversion from a pseudo-dimension bound on to a VC-dimension bound on the thresholded class , which needs the observation that a shattered tuple of pairs has distinct first coordinates.
Shatters, PseudoDim, GrowthFunction, HasVCDim. The exact-value predicates fix finite dimensions , , which the paper's bound presupposes. "" is stated as "every shattered tuple has length at most ". is Bool.The k-server problem (Manasse, McGeoch and Sleator, 1990) is the central problem of online computation: servers sit on points of a metric space, requests arrive one at a time at points of the space, and each request must be served by moving a server to it, at a cost equal to the distance travelled. An online algorithm decides without knowing future requests; its quality is its competitive ratio, the worst-case ratio between its cost and the cost of an optimal offline schedule. Paging (caching) is the special case of a uniform metric, and weighted paging the case of a weighted star.
Timeline of the upper bounds for general metrics:
Let be a finite metric space with points and a number of servers. A configuration places server at . A deterministic online algorithm maps each prefix of the request sequence to a configuration that has a server at the last request; its cost on a sequence is the total distance travelled. is the least cost of any schedule serving from the initial configuration . A randomized algorithm is a probability distribution over deterministic online algorithms, all starting at ; it is -competitive if there is a constant such that its expected cost on every request sequence is at most .
The paper works with three auxiliary objects. A σ-HST is a rooted tree whose leaves are the points, in which all edges from a node to its children have one common length, equal to times the length of the edge above that node; the distance between two leaves is the length of the tree path. A weighted σ-HST only requires that the edge above a non-root internal node be at least times each edge below it. In the fractional k-server problem on a tree, the state is a vector of server probabilities on the leaves with and , a request at leaf forces , and moving from to costs , where is the mass below node and the length of the edge above . In the allocation problem on a weighted star with weights , requests carry a location , a monotone cost vector (the cost of serving with servers there) and a server quota .
There is a universal constant such that for all , every metric space with points and every initial configuration , some randomized online algorithm starting at is
In the order the proof uses them:
The theorem broke the exponential gap between the lower bound and the upper bound for randomized k-server, and showed that randomization helps on every finite metric, not only on uniform or specially structured ones. Its two-level method (a fractional algorithm on trees driven by per-node allocation problems, followed by an online rounding) became the template for later work, including the bound on HSTs of Bubeck, Cohen, Lee, Lee and Mądry (STOC 2018) and Lee's bound on general metrics (FOCS 2018).
The result is proved, in this paper. As far as is known it has no machine-checked proof. Formalizing it means formalizing the analysis of an online algorithm driven by a continuous-time process, a potential-function argument with exact constants, a tree contraction with a distortion bound, and an online randomized rounding against a transportation cost. The allocation, HST and rounding statements are reusable for other online problems on trees (metrical task systems, weighted paging).
For a deterministic or randomized algorithm on a tree, the natural recursion splits the servers of each node among its children. Coté, Meyerson and Poplawski showed that this works if each node solves an allocation problem with a strong guarantee: hit cost within a factor of optimal. Integral allocation algorithms cannot achieve this; the integrality gap example of the paper (p. 8) gives a factor . The fractional relaxation avoids the gap, but then the rounding step must keep a randomized state consistent with a fractional state at constant-factor cost, and the HSTs obtained from general metrics have depth growing with the aspect ratio, which a depth-dependent ratio cannot afford. Each of the three reductions (allocation to fractional k-server, deep HST to shallow weighted HST, fractional to randomized) loses only polylogarithmic or constant factors, and the main theorem needs all three at once.
The k-server model, randomized algorithms and competitiveness are the published definitions KServer_model and KServer_randomized; competitiveness carries an additive constant fixed before the request sequence. Trees are finite rooted trees with a parent map, a depth function and positive edge lengths; points of the k-server problem are the leaves, and the theorems take an arbitrary finite metric space together with a bijection to the leaves and the hypothesis that the distance equals the tree distance. Fractional k-server states have exactly units of mass, each leaf at most , and fractional algorithms are measured against the integral offline optimum. The allocation optimum is the integral optimum; cost vectors are finite, non-negative and non-increasing; the diameter of the star is . The cost of changing a randomized state is the transportation cost over couplings, with minimum-matching cost between configurations. Every is an explicit constant quantified before the instance, except that in Theorems 7 and 24 and Lemma 25 it may depend on .
Formalizations that make the targets trivial are excluded: the fractional state must place a full server on every request and stay in , the benchmark is the integral optimum (not the algorithm's own or the fractional cost), and no constant may depend on , , the metric or the tree, since otherwise Theorem 1 would follow from the bound.
The proof of Theorem 1 also uses the embedding of Fakcharoenphol, Rao and Talwar [18] of a finite metric into a distribution over σ-HSTs with expected distortion . It is an external ingredient, not a result of this paper, and is not a milestone; contributions formalizing it (or Bartal's earlier embedding) are welcome, as are formalizations of the integral optimum's properties on trees (Lemmas 21–22 of the paper), which are not stated here.
Nash equilibrium is the standard solution concept for strategic games, but it is usually justified by appeal to what players "would" do once they somehow coordinate on a profile. Correlated equilibrium, introduced by Aumann (J. Math. Econ. 1, 1974), enlarges the set of outcomes by letting players condition their actions on correlated private signals. In Correlated Equilibrium as an Expression of Bayesian Rationality (Econometrica 55, 1987), Aumann gave the concept a decision-theoretic foundation: if the players share a common prior over the states of the world and each player maximizes expected utility given his information at every state, then what they play is a correlated equilibrium — and every correlated equilibrium arises this way. The result is a standard entry point to the epistemic foundations of game theory, and correlated equilibria are central in algorithmic game theory because no-swap-regret learning dynamics converge to them (Foster–Vohra 1997; Hart–Mas-Colell 2000).
Timeline:
A game in strategic form has players , action sets , action -tuples , and payoffs .
A correlated strategy -tuple is a function on a finite probability space , with and . Its expected payoff is . For , the profile replaces player 's coordinate of by . The function is a correlated equilibrium (Definition 2.1) if
for every player and every that is a function of (i.e. ). The distribution of assigns to each the number , and a correlated equilibrium distribution (c.e.d.) is the distribution of some correlated equilibrium.
An information system consists of a finite set of states of the world, a common prior on , an information partition of for each player, and action functions with , each constant on the elements of (each player knows his own action). For a random variable , is the -average of over the element of containing . Player is Bayes rational at if
This is the two-sided statement the paper announces in its introduction (p. 2) and closes in Sect. 4d (p. 11): "under Bayesian rationality, the set of all information systems corresponds precisely to the set of all correlated equilibria."
The mission also states, as a supporting lemma without a milestone, the cell-wise step of the proof of the Main Theorem: Bayes rationality at every state gives on every cell for constant on cells.
The theorem identifies correlated equilibrium as the outcome of individual Bayesian decision making under a common prior, without any assumption that players randomize or that their choices are independent. It shows that the Nash equilibrium's independence requirement is not implied by rationality alone, and it is the template for later epistemic characterizations of solution concepts. On the computational side, correlated equilibrium distributions form a polytope described by linear inequalities (the companion mission of this series), which is why they are the tractable equilibrium notion in algorithmic game theory.
The result is proved in the paper; it has no machine-checked formalization known to this mission. Formalizing it pins down the exact role of the standing assumptions — finiteness, a common prior, measurability of each player's action with respect to his own partition, rationality at every state — and of the conditional expectation on cells of probability zero. The definitions (information systems, Bayes rationality, correlated equilibria as functions on a finite probability space) are reusable for later formalizations of the paper's Sect. 5 (subjective correlated equilibrium) and of other epistemic results.
The mathematics is short; the difficulty lies in the bookkeeping that the paper's notation hides. The hypothesis is interim (a conditional inequality at each state), while Definition 2.1 is ex ante (an unconditional inequality). Passing between them requires the law of total expectation over a partition whose cells may have probability zero, where conditional expectations are undefined. Deviations in Definition 2.1 are functions of , not arbitrary maps, and must be shown constant on cells, which uses measurability of . A tempting first idea — that rationality against every fixed action already gives rationality against every deviation — fails without measurability: a player who does not know his own action could be rational at each state against constant deviations while a deviation varies inside his cells. The converse direction needs an information system that satisfies every axiom of the goal's right-hand side, not just one that is Bayes rational.
ι with decidable equality; action sets S i are arbitrary types (the paper's finiteness of is not used); payoffs are h : ι → (∀ i, S i) → ℝ.AGT.IsLottery (from the published definition agt_games). State spaces and the witnessing probability spaces of a c.e.d. range over Type; for finite sets this loses nothing.Setoids. The Common Prior Assumption is built into the information system, which has a single prior. Measurability of each action function is a field of the structure.distr to sums over action profiles.A reproducing kernel is the function that represents point evaluation in a Hilbert space of functions: . Kernels are combined all the time. In machine learning, a kernel on pairs of objects is routinely built as the pointwise product of two simpler kernels, and in complex analysis the product of a kernel with its conjugate appears naturally. That the pointwise product of two positive matrices is again a positive matrix goes back to I. Schur (1911). What Schur's theorem does not say is which space of functions the product kernel belongs to and what its norm is.
N. Aronszajn answered this in §8 of Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404, doi:10.1090/S0002-9947-1950-0051437-7), the paper that fixed the general theory of reproducing kernel Hilbert spaces. He notes (p. 358, footnote 7) that the idea of the proof was found independently by R. Godement, who applied it only to positive definite functions. The answer has three ingredients developed in the same paper: the functional completion of an incomplete class of functions (§4), the restriction of a kernel to a subset (§5), and the direct product of two classes of functions (§8).
Let be an arbitrary set. A class with a reproducing kernel is a complex Hilbert space of functions such that every point evaluation is continuous. Its reproducing kernel is characterized by: for each , and for all , where the scalar product is linear in and conjugate-linear in .
Functional completion. Suppose is a linear class of functions on with a scalar product satisfying every Hilbert-space axiom except completeness. A functional completion of is a Hilbert space of functions on , with continuous point evaluations, that contains isometrically as a dense subset.
Restriction. For , the restriction of is , and is the class of all restrictions.
Direct product. Given classes , on with kernels , and norms , , consider on the functions
with scalar product . Their functional completion is the direct product , with norm .
In Lean, kernelFn H x y is the scalar kernel of a space H, IsFunctionalCompletion ι H says H is a functional completion of the class presented by ι, and IsDirectProduct H₁ H₂ H' says H' is .
The kernel is the reproducing kernel of the class of restrictions of the functions of to the diagonal , and
The result. Theorem II turns the Schur product theorem from a statement about matrices into a statement about function spaces: it says which functions the product kernel can represent and how their norms are computed, through a minimal decomposition. It is the standard description of the reproducing kernel Hilbert space of a product kernel, used to reason about which functions product kernels can express and with what norm, and the Remark gives a concrete series description of the same space. §5 (restriction) and §4 (functional completion) are general tools in their own right: restriction underlies every comparison of kernels on nested domains, and §4 is the criterion for when an incomplete space of functions can be completed without leaving the world of functions.
Formalizing it. All four results are classical and proved on paper. Mathlib has reproducing kernel Hilbert spaces (RKHS, RKHS.kernel, the construction RKHS.OfKernel from a positive semidefinite kernel) and Schur's product theorem (Matrix.PosSemidef.hadamard, for an arbitrary index type), but no restriction theorem, no functional completion and no tensor product of reproducing kernel Hilbert spaces. None of these statements has a machine-checked proof that the mission is aware of.
The kernel identity is the easy part: by Schur's theorem is positive, so some space with kernel exists. The content is the identification of that space and its norm. The direct product has to be constructed before anything can be said about it: the class of finite sums of products is not complete, the scalar product (2) must be shown independent of the representation and positive definite, and the completion must stay a class of functions, which is exactly the question §4 answers and which can fail (p. 349 gives a class satisfying the first condition but not the second). The norm formula is an attained minimum over an infinite-dimensional affine set of preimages, not merely an infimum.
Scalars are complex throughout ("From now on … we shall consider only complex Hilbert spaces", p. 343). The underlying set is an arbitrary type X, with no topology, measure or nonemptiness assumption. A class with a reproducing kernel is a complex Hilbert space H with Mathlib's RKHS ℂ H X ℂ structure; its functions are the coercions ⇑f. The scalar kernel is kernelFn H x y = RKHS.kernel H x y 1. Mathlib's inner product is conjugate-linear in , so Aronszajn's is .
Conventions and reading decisions:
RKHS.OfKernel K, which would make the kernel identity true by construction.IsDirectProduct); it is never defined through its kernel. With that, Theorem I is not a definitional identity and Theorem II is not a restatement of §5.IsLeast). In Theorem II and §5 it is the minimum of the norm, not its square; in the Remark it is the minimum of the sum of squared norms, as printed.HilbertBasis over an arbitrary index set, and the series converges unconditionally at each point.Results already in Mathlib are not restated: Schur's product theorem (Matrix.PosSemidef.hadamard, the first sentence of §8 and the sentence after Theorem I), positivity of a kernel (RKHS.posSemidef_kernel) and existence of a space for a positive kernel (RKHS.OfKernel, RKHS.kernel_ofKernel).
A complete development needs a Hilbert tensor product of reproducing kernel Hilbert spaces realized as functions on , the restriction construction (quotient by the subspace of functions vanishing on ), and uniqueness of a reproducing kernel Hilbert space with given kernel. The restriction theorem and the functional completion theorem are reusable well beyond this mission; contributions of either, or of a Hilbert tensor product for RKHS, are welcome.
Reproducing kernel Hilbert spaces are Hilbert spaces of functions in which evaluation at a point is a continuous linear functional. They appear wherever a space of functions carries a natural quadratic norm: Bergman and Hardy spaces of analytic functions, spaces of harmonic functions and solutions of elliptic equations, Sobolev spaces in one dimension, and, since the 1990s, the hypothesis classes of kernel methods in machine learning (support vector machines, Gaussian process regression, kernel ridge regression). In all of these settings, kernels are routinely combined: a sum of kernels is used to model a function as a sum of components, and the question is which space of functions, and which norm, the combined kernel describes.
N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404) organised the subject as a calculus of operations on kernels. Its §6 answers the question for sums.
Timeline. E. H. Moore (Bull. Amer. Math. Soc. 1916; General Analysis, 1935) introduced positive Hermitian matrices on arbitrary sets and their associated function classes. S. Bergman (1920s–1930s) studied the kernel of square-integrable analytic functions of a domain. R. Godement (C. R. Acad. Sci. Paris notes, 1945–1946) found the sum theorem for positive definite functions on a group (footnote 6 of the paper). Aronszajn (1950) proved it for arbitrary kernels on arbitrary sets, with the description of the norm as a minimum over decompositions.
Let be an arbitrary set. A class of functions on is a complex vector space of functions carrying a norm that makes it a complex Hilbert space. A function is the reproducing kernel (r.k.) of if, for every , the function belongs to and
where is the scalar product, linear in . A kernel exists exactly when every evaluation is continuous.
A function is a positive matrix if for all finite families of points and complex numbers . Every reproducing kernel is a positive matrix.
A class is a subclass of if every function of belongs to , and a subspace if moreover the two norms agree on . Two classes , with kernels , have a sum class , a set of functions; a function of it may have many decompositions , since and may share functions.
For complex Hilbert spaces , of functions on with kernels , : the kernel is the reproducing kernel of the class of all , with
the minimum taken over all decompositions , . The goal asserts that a space with kernel exists, and that every such space consists exactly of the sums and has exactly this norm, the minimum being attained.
The result itself. The sum theorem is the first operation of Aronszajn's calculus and the base of the next ones: the order between kernels and the inclusion theorem of §7 are derived from it, as are the kernel of the class of all and the characterisation of kernels of real spaces (§6, p. 354). In machine learning, it is the statement behind additive kernels and multiple-kernel learning: the hypothesis class of is the set of sums, and the regulariser is the infimal convolution of the two squared norms. In complex analysis, it describes the space attached to a sum of Bergman-type kernels.
Formalizing it. The results are classical and proved in the paper; none of them is formalized in Mathlib beyond the existence half of Moore's theorem. Mathlib (2026) has reproducing kernel Hilbert spaces with operator-valued kernels (RKHS, RKHS.kernel, RKHS.kerFun, RKHS.posSemidef_kernel) and the construction of a space from a positive semidefinite matrix (RKHS.OfKernel, RKHS.kernel_ofKernel). This mission adds uniqueness, the sum theorem, kernels of closed subspaces, the finite-dimensional case and the conjugate class.
The kernel is the kernel of some space by Moore's existence theorem, so the content is the identification of that space. The obvious candidate, the external direct sum mapped to functions by , is not injective as soon as and share a nonzero function; the class of sums is the image of a quotient, and its norm is the norm of a minimal representative, which has to be shown to exist and to make the class complete. Proving that the resulting space has kernel and that every other space with this kernel coincides with it requires the uniqueness half of Moore's theorem, which is not in Mathlib. The disjoint case needs, in addition, that an isometric image of a complete space is closed, and the converse direction of its "only in this case".
X with no topology, measure, or nonemptiness assumption.RKHS ℂ H X ℂ on a complex Hilbert space H; its functions are Set.range (⇑ : H → X → ℂ).kernelFn H x y is RKHS.kernel H x y 1.⟪g, f⟫_ℂ.(Matrix.of K).PosSemidef, and "positive definite" is Matrix.PosDef.IsLeast), never an infimum.Reading decisions, recorded in the item notes:
Trivialization ruled out. The goal does not define the sum class as RKHS.OfKernel (K₁ + K₂) and assert that its kernel is , which is Mathlib's kernel_ofKernel. Its content is the description of the functions (exactly the sums) and of the norm (the attained minimum) for every space with that kernel.
Infrastructure. A complete development needs:
Submodule.starProjection);Milestone 1 and the RKHS structure on a closed subspace are reusable beyond this mission and are natural Mathlib contributions. Independent proofs of any milestone are welcome.
Expander graphs are sparse graphs in which every set of vertices has many neighbours. Families of them with bounded degree and expansion bounded away from zero are a basic tool of theoretical computer science: they are the main component of the sorting network of Ajtai, Komlós and Szemerédi (AKS 1983), the building block of superconcentrators and other graphs with strong connectivity properties, and an ingredient of many later constructions in coding theory, derandomization and complexity.
Expansion is hard to certify. Checking that every set of vertices has many neighbours means looking at exponentially many sets, and computing the exact expansion of a graph is coNP-complete. A spectral quantity, by contrast, is computable in polynomial time. N. Alon's paper Eigenvalues and expanders (Combinatorica 6 (1986) 83–96) proves that for regular bipartite graphs the two notions are equivalent: a graph is a strong expander if and only if the second-smallest eigenvalue of its Laplacian is bounded away from 0, with explicit constants in both directions. This is a discrete counterpart of Cheeger's inequality for Riemannian manifolds.
Timeline.
All graphs are finite and simple. For a graph and a set , is the set of neighbours of ; it may meet .
The Laplacian of is , where is the 0–1 adjacency matrix and the degree of . It is symmetric with eigenvalues , counted with multiplicity, and is its second-smallest eigenvalue. It is positive exactly when is connected.
Let be a -regular bipartite graph with and .
Part (1) of the goal combines Lemmas 3.1 and 2.4; part (2) follows from Lemma 3.3.
The result. Theorem 3.4 makes expansion of regular bipartite graphs checkable in polynomial time up to a constant-factor loss. A random regular bipartite graph can be generated and its expansion certified by computing one eigenvalue. Lemma 2.4 is one of the first discrete Cheeger inequalities. Together with Corollary 2.3 it shows that magnifiers and enlargers are the same graphs up to the constants, and it underlies the later theory of spectral expanders, including the Alon–Boppana bound and Ramanujan graphs.
The formalization. The results are proved in the paper. The work is to formalize the known proofs. That includes Tanner's eigenvalue bound, which the paper only cites, and a max-flow min-cut argument, for which Mathlib has no general theorem. No machine-checked version of Lemma 2.4, Lemma 3.1, Lemma 3.3 or Theorem 3.4 is known to exist. Lemma 2.2 is already stated and proved on the platform as part of the Alon–Milman mission.
The direction "eigenvalue gap implies expansion" is a variational argument on the spectrum of . The converse is the hard one. A first attempt bounds from below by testing the Rayleigh quotient on indicator vectors of sets. That only gives upper bounds on : any one test vector does. A lower bound has to control every vector orthogonal to the constants at once. The paper first reduces to the positive part of an eigenvector (Eq. (2.1)). It then turns the combinatorial expansion of the graph into an analytic inequality for that function, using a network flow whose existence comes from the max-flow min-cut theorem. Step (ii) of the flow conditions printed on p. 87 is false as stated: the arcs of the network absorb part of the flow. The flow argument has to be repaired before it can be formalized.
Lemma 3.1 has its own obstacle: one-sided expansion of inputs must be converted into expansion of arbitrary vertex sets that mix inputs and outputs. This needs the strong form of expansion; for ordinary expanders the lemma is false.
Graphs are SimpleGraph V on a Fintype. A bipartite graph lives on the sum type I ⊕ O, and IsIOBipartite forbids edges inside I and inside O. Cardinalities are Set.ncard. "Maximal degree " is read as G.maxDegree ≤ d; every statement is monotone in or fixes by regularity (G.IsRegularOfDegree d). The condition is written in . All constants are real, and every subtraction and division is taken in .
Reused published items:
AlonMilman.Diameter.lambda1, the second-smallest eigenvalue of G.lapMatrix ℝ, which is by convention on fewer than two vertices.AKSSorting.Core.neighbours.AlonMilman.Diameter.theorem_2_5, which carries Alon–Milman's standing hypotheses that is connected and ; outside them the inequality is trivial.The page omits a few degenerate cases, and the following hypotheses are added for them. Each is necessary, with a counterexample recorded in the item's statement:
Eq. (2.1) is stated in multiplied form, so no quotient by appears.
The closing sentences of Theorem 2.5 and Theorem 3.4 ("Thus … one can prove efficiently …") are not formalized. Read as implications between expanders they reduce to monotonicity in , because ; their content is algorithmic.
Several encodings would trivialize the mission and are excluded:
Contributions are welcome:
Uzan's review Varying Constants, Gravitation and Cosmology (Living Rev. Relativity 14 (2011) 2) is about testing whether the fundamental constants of physics change in space or time. Before any experiment can be read, §2.1 of the review settles which constants it even makes sense to ask about. Two claims from that section carry the whole programme:
Both claims are informal statements of a classical result of dimensional analysis, the Buckingham theorem (E. Buckingham, Phys. Rev. 4 (1914) 345). This mission states them precisely and asks for formal proofs.
Fix base units (for mechanics : ) and dimensional constants. The dimension matrix says that constant has dimension ; real exponents are allowed, because Gaussian units give the charge the dimension (Uzan, p. 15). A configuration lists the numerical values of the constants in some system of units.
Goal (Buckingham ). Put . There are linearly independent such that every unit-invariant factors as
Milestones, in order:
The result. Milestones 6–7 justify the review's working convention of quoting all bounds as bounds on dimensionless numbers (, , , …). Milestone 2 counts how many independent numbers there are. Milestones 3–5 say that natural units are well defined.
Formalizing it. The mathematics is classical and the proofs are known. What remains is to formalize it: a reusable, general dimensional-analysis layer (unit actions, dimensionless monomials, natural units) that later missions on Uzan's review can build on.
Taking logarithms turns the multiplicative problem into linear algebra: changes of units act on by translations through the column space of , and is the annihilator of that space. Two steps carry the content. The first is the duality step (annihilator of the annihilator) behind milestone 6 and the goal. The second is the bookkeeping with real powers (Real.rpow), which only behaves well on positive bases. The goal also needs a choice of with no regularity, defined through the quotient .
VaryingConstants; all definitions are in one definition file. Indices are Fin n and Fin d, and exponents are real.IsPositive), not a subtype. Unit invariance constrains only on positive configurations.Matrix.rank over .e : Fin d → Fin n. The independence hypothesis is .Contributions such as general lemmas on Real.rpow products and on annihilators of matrix column spaces are reusable beyond this mission.
Every linear program comes with a second linear program, its dual, and most of what is known about linear programming is a statement about how the two interact. Weak duality gives certificates of optimality; strong duality says those certificates always exist; complementary slackness turns optimality into a system of equations. These three facts are the core of any first course in optimization and of every correctness argument for the simplex method.
Strict complementarity is the sharpest statement of the same kind. Complementary slackness says that in each pair (a primal variable and its dual slack, a dual variable and its primal slack) at least one member vanishes at optimality. Strict complementarity says that some optimal pair can be chosen so that exactly one member vanishes in each pair. The result is due to Goldman and Tucker (1956). It is what identifies the optimal face of a linear program and its partition of the variables into those that can be positive at an optimum and those that cannot, and it is a standing ingredient in the analysis of interior-point methods, which approach this strictly complementary optimum rather than a vertex.
This mission formalizes the chain from duality to strict complementarity as it is developed in Chapters 5 and 10 of Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014, doi:10.1007/978-1-4614-7630-6). It is the second mission of a series on that book.
Timeline:
Fix integers , a real matrix , a vector and a vector . The primal problem is
where is the primal slack. The dual problem is
where is the dual slack. A vector is primal feasible if and ; it is primal optimal if it is feasible and for every feasible . Dual feasibility and dual optimality are defined in the same way, with minimization. Inequalities between vectors are componentwise, and means that every component of is strictly positive.
A halfspace of is a set with ; a polyhedron is a set for some , and .
In the Lean development these objects live in the namespace VanderbeiLP.StrictComp: primalSlack A b x, dualSlack A c y, PrimalFeasible, DualFeasible, PrimalOptimal, DualOptimal, IsHalfspace, IsPolyhedron.
If the primal (10.9) has an optimal solution, then there exist a primal optimal and a dual optimal , with slacks and , such that
The only hypothesis is primal optimality; the existence of a dual optimum is part of the conclusion.
Theorem 10.6 is the feasible-solution version of the goal; Theorem 10.4 is a further consequence of Farkas' Lemma in the same chapter.
Strict complementarity determines the optimal partition: the set of indices for which some optimal has is exactly the complement of the set for which some optimal dual slack is positive. This partition describes the optimal faces of both problems, is the object that interior-point methods recover in the limit, and is the starting point of sensitivity analysis beyond a single optimal basis. Farkas' Lemma and the separation theorem are the linear-algebraic form of convex separation and are reused across optimization, game theory and polyhedral combinatorics.
All results of this mission are classical and proved in the literature. What the mission adds is a machine-checked version of them in one fixed linear-programming form, the inequality form with explicit slacks used throughout Vanderbei's book. Weak duality, strong duality and complementary slackness are already formalized on this platform for other forms (Bertsimas–Tsitsiklis's general form, a minimization, and a covering pair with the roles of primal and dual exchanged). Those statements are equivalent to the ones here only after a transformation (negating the objective, swapping primal and dual), so they are not the same theorems. The Farkas variant for inequality systems, the separation theorem for two polyhedra, and both strict complementarity theorems have no formal counterpart on the platform.
Weak duality and the converse direction of complementary slackness are short computations. The substance lies elsewhere. Strong duality and Farkas' Lemma require a genuine existence argument; the book obtains them from the simplex method, whose termination is itself a nontrivial fact, and any other route needs an independent theorem of the alternative.
For strict complementarity the obvious attempt fails. Complementary slackness gives, for each optimal pair, only that one member of each complementary pair vanishes; nothing in a single optimal basic solution forces the other member to be positive, and in degenerate problems every basic optimal pair can fail strictness. A strictly complementary pair is in general not a vertex of either optimal face, so it cannot be found by inspecting basic solutions. The goal also asks for more than Theorem 10.6: the positivity must be achieved within the optimal sets, which are faces cut out by an additional objective-level constraint, so the feasible-solution argument does not transfer verbatim.
Vectors are Fin n → ℝ and Fin m → ℝ; the constraint matrix is Matrix (Fin m) (Fin n) ℝ; m and n are arbitrary natural numbers, including zero. The slacks are functions of the solution (primalSlack A b x = b - A *ᵥ x, dualSlack A c y = Aᵀ *ᵥ y - c), never free variables, so a "solution " of the book is the vector with the slack it determines. Optimality is attainment of the maximum (minimum) over the feasible set; no supremum, value function or extended reals are involved. The strict inequality is written componentwise as ∀ j, 0 < x j + dualSlack A c y j and ∀ i, 0 < y i + primalSlack A b x i.
A halfspace carries a nonzero normal vector. Without that requirement the empty set would be a halfspace and the separation theorem would be trivial; the formal definition rules this out.
The book states every result in this mission with its hypotheses explicit, and none of them asserts the existence of an unspecified constant, so no explicit-constant instantiation was needed. The remark after Theorem 10.7 refers to "the complementary slackness theorem (Theorem 5.1)"; the complementary slackness theorem is Theorem 5.3, and the milestones follow the theorem numbering.
A complete development needs a theorem of the alternative for real linear inequality systems (Mathlib has Farkas-type results for cones and the geometric Hahn–Banach theorem, but no ready-made matrix version of Lemma 10.5) and elementary convex-combination arguments on feasible sets. The definitions of this mission are self-contained and reusable for any later chapter that works in Vanderbei's inequality form. Proofs of any milestone are welcome, as are proofs that avoid the simplex method.
Large convex programs often have a block structure: a small set of "complicating" variables couples otherwise separate subproblems in the remaining variables . Decomposition with respect to variables fixes , solves the subproblem in , and treats the optimal subproblem value as a function of alone. The outer problem in is then small but nonsmooth, because the optimal value of a constrained program is generally not differentiable in its parameters. Shor's Chapter 4 (Shor 1985, Ch. 4) presents this reduction as a principal application of subgradient methods: once a subgradient of the outer function can be read off from the subproblem, the methods of Chapters 2–3 apply directly. The same construction underlies Benders decomposition (Benders 1962) and its convex generalization (Geoffrion 1972), and parametric decomposition schemes for linear programs.
The chapter's other numbered results serve the same programme from the dual side: the Lagrangian dual function of a program over a compact set gives a lower bound usable in branch and bound (Theorem 4.3), exact nonsmooth penalty functions turn a constrained convex program into one unconstrained nonsmooth minimization (Theorem 4.2; nonsmooth penalties were first studied systematically by I. I. Eremin, 1967), and a stochastic transportation model is shown to be a convex program before being solved through its dual (Lemma 4.3).
The variables split into and (Euclidean spaces, inner product ). The problem is
with convex functions of (jointly convex), finite everywhere. For a fixed , the subproblem (4.3)–(4.4) is with . Where it has a solution , the value function is
The Slater condition at asks for a with for all . The Lagrange function is , and are Kuhn–Tucker multipliers at when . A subgradient of a function of is written through its projections on the two blocks; a subgradient of at is a with .
If is a convex set of -values at which the subproblem has a solution, then is convex on ; and if satisfies the Slater condition, then for every optimal , multipliers exist, has a subgradient at with vanishing -projection, and the -projection of any such subgradient satisfies
The result itself. Theorem 4.1 is what makes decomposition with respect to variables an instance of convex nonsmooth minimization: the outer problem is convex, and one subproblem solve returns both and a subgradient. The algorithm on p. 96 — solve the subproblem at , form by (4.6) or (4.7), take a subgradient step — is exactly this, and the step-size theory of Chapter 2 then gives convergence. The Corollary is the version used in practice for linear and quadratic subproblems, where multipliers and partial subgradients are computed directly. Theorem 4.2 justifies replacing constraints by nonsmooth penalties of finite slope, and Theorem 4.3 is the weak-duality bound behind Lagrangian relaxation in branch and bound.
Formalizing it. All results are classical and proved in the book; none is formalized as stated here. The platform already has related statements with different shapes: convexity of the perturbation value function in the constraint right-hand side (VectorSpaceOpt.perturbationValue_convex, Luenberger), Slater strong duality over the whole space (ConvexOptimization.slater_strong_duality), weak duality with an unconstrained domain (ConvexOptimization.weak_duality), weak Lagrangean duality for integer programs (LinearOptimization.integer_program_weak_lagrangean_duality), and the LP special case of convexity of the optimal cost (LinearOptimization.lp_optimal_cost_convex_in_rhs). This mission adds the partial-minimization form in which one block of variables is minimized out under joint convexity, its subgradient calculus, exact nonsmooth penalties, and weak duality over a compact domain.
Convexity of is elementary once the minimum is attained. The subgradient formula is where the obvious argument fails: an arbitrary subgradient of at does not project to a subgradient of , because its -projection contributes a term of unknown sign. The theorem needs a subgradient whose -projection vanishes, and its existence is a separate fact about partial minimization of a jointly convex, everywhere-finite function. The multipliers come from the Kuhn–Tucker theorem for the subproblem, which requires the Slater condition. In the Corollary, the difficulty is to show that differentiability in forces the -projection of any combination to vanish. In Theorem 4.2 the necessity part needs a subdifferential chain rule for .
EuclideanSpace ℝ (Fin l), EuclideanSpace ℝ (Fin m), EuclideanSpace ℝ (Fin N); constraints are indexed by Fin n (or Fin m). All functions are real-valued and finite everywhere; joint convexity is convexity on the product .Useful infrastructure beyond this mission: partial minimization of jointly convex functions, subgradients on product spaces, and a Kuhn–Tucker saddle-point theorem for convex programs with inequality constraints. Proofs of any milestone, and reusable lemmas for these, are welcome.
The ellipsoid method is the algorithm that settled the polynomial-time solvability of linear programming (Khachiyan, 1979) and that underlies the equivalence of separation and optimization in combinatorial optimization (Grötschel, Lovász and Schrijver, 1981). Its origin is in nonsmooth convex optimization. In 1976 Yudin and Nemirovskii proposed a modified method of centered sections that localizes an optimum inside a sequence of ellipsoids, and in 1977 N. Z. Shor observed independently that the same scheme is a subgradient method with space dilation along the gradient, the family of methods he had developed since 1969. Section 3.8 of Shor's monograph Minimization Methods for Non-Differentiable Functions (Springer 1985) presents the method in this second form and proves its basic localization property.
Timeline:
Let be -dimensional Euclidean space with inner product , and . For a unit vector and a number , the operator of space dilation along with coefficient is : it multiplies the component of a vector along by and leaves the orthogonal component unchanged.
Let be a vector field, not necessarily continuous. The problem is to find a point with
where it is known that such an exists in the closed ball of radius about a given point . Put and . The algorithm (3.57)–(3.60) starts from , , , and at iteration stops if , and otherwise sets
With , the localizing ellipsoid is , and the dimension-dependent ratio is
Three problems produce such a field: minimizing a convex on a ball (the field (3.62), a subgradient inside the ball and the outward radial direction outside); the convex program s.t. (the field (3.65), a subgradient of the objective at feasible points and of a most violated constraint otherwise); and a convex–concave saddle point problem (the field ).
For every ,
that is, . The statement holds for every field satisfying the monotonicity condition at ; nothing about continuity or convexity is assumed.
The result. Theorem 3.14 with the volume identity says that after steps the solution is confined to an ellipsoid of volume times that of the initial ball, for any field of the above kind. Milestones 4–6 turn this into localization guarantees for constrained convex minimization, general convex programming and convex–concave saddle points, with a rate that depends only on the dimension. The same localization underlies the complexity bounds of the ellipsoid method for linear programming and the polynomial equivalence of separation and optimization.
Formalizing it. The results are classical and proved in the book. No machine-checked proof of the space-dilation form of the method is known to exist. The platform already contains a proved version of the Bertsimas–Tsitsiklis form (LinearOptimization.ellipsoid_update_halfspace_subset, LinearOptimization.ellipsoid_update_volume_lt: a half-ellipsoid is covered by an updated ellipsoid whose volume is smaller by a factor below ), and Khachiyan's feasibility algorithm (SmaleNinth.khachiyan_ellipsoid_decides). Those statements are about a center/shape-matrix update and give a volume inequality; this mission is about the iterates of Shor's matrix recursion and the exact ratio . Relating the two parametrizations () is a welcome side result.
The obvious approach, tracking the ellipsoid through the center and shape matrix and invoking a minimum-volume covering argument, is not what the algorithm computes: here the iterate is updated through the factor and the stepsize is fixed in advance, independent of the field, so the induction must be carried out in the transformed coordinates in which the ellipsoid is a ball. The difficulty is that the monotonicity condition gives only the sign of one inner product, , while the norm of depends on both and ; the constants and are exactly those for which the resulting quadratic estimate closes. For the volume identity, the main technical step is computing and the Lebesgue measure of a linear image of a ball in EuclideanSpace.
EuclideanSpace ℝ (Fin n); matrices act through Matrix.toEuclideanLin; is the transpose. is the matrix (the book's property 10); for unit this is the operator of the book's definition.ellipsoidMethod g R x₀ : ℕ → EllState n, with state , , . If the state is repeated from then on (the book stops); the normalization in (3.57) is only performed when . is the matrix inverse of , which is nonsingular.ℝ≥0∞. The ellipsoid is given for an arbitrary center (the book writes in one place and in another; the volume is the same). The volume formula requires the first iterations to have been performed (, ); the ratio requires iteration to be performed.MeasureTheory.Measure.addHaar_image_linearMap), and elementary real inequalities for . The space-dilation lemmas are reusable in the other Shor missions on SDG methods and the -algorithm.Many optimization problems of operations research have objectives that are convex but not differentiable: Lagrangian duals of integer and combinatorial programs, maxima of finitely many affine or smooth functions, penalty functions for systems of inequalities, and the value functions produced by decomposition. For such functions the gradient method and steepest descent fail. Constant steps cannot work because the subgradients need not tend to zero at a nondifferentiable minimum, and exact line search along the negative gradient can converge to a point that is not a minimizer (the example on pp. 22–23 of the source).
The subgradient method replaces the gradient by an arbitrary subgradient and gives up monotone decrease of the objective. Its convergence theory is the foundation of nondifferentiable optimization and of Lagrangian relaxation in integer programming.
Timeline. N. Z. Shor proposed the method with normalized steps in 1962 (Kiev). Yu. M. Ermoliev proved convergence in finite dimensions with divergent-series stepsizes (Kibernetika, 1966), and B. T. Polyak proved it for constrained problems in Hilbert space (Doklady Akad. Nauk SSSR, 1967). Held, Wolfe and Crowder (Mathematical Programming, 1974) brought the method to large combinatorial problems through Lagrangian relaxation. This mission formalizes the exposition of Section 2.1–2.2 of Shor's monograph (Springer, 1985), which gives self-contained proofs of these results.
Let be the -dimensional Euclidean space with inner product and norm . Let be a convex function finite everywhere. A vector is a subgradient of at if
Every convex has at least one subgradient at every point. Let be the set of minimum points and, when it is nonempty, .
A subgradient selection assigns to each some subgradient of at . No particular choice is made: every result holds for every selection. Given stepsizes and a starting point , the normalized subgradient method is
If , then is a minimizer and the computation stops. The unnormalized method is (2.5), and the method with restarts takes that step when and returns to otherwise.
If is nonempty and bounded, , and , then for every and every subgradient selection, the method (2.4) either reaches at some index or
Theorem 2.2 is the basic convergence guarantee for first-order methods on general nonsmooth convex functions. It needs no Lipschitz constant, no bound on the subgradients and no smoothness: normalizing the step makes the step length independent of the size of the subgradient. The divergent-series rule , is the standard stepsize condition of stochastic approximation and of Lagrangian relaxation codes. Theorems 2.3–2.5 mark its boundaries. The unnormalized method needs bounded subgradients (Theorem 2.3), restarts remove that need (Theorem 2.4), and a solution set with nonempty interior gives finite termination (Theorem 2.5). The last result is the basis of the finite methods for systems of convex inequalities and for the dual of an assignment problem with a unique solution (pp. 28–29).
All of these results are classical and proved in the source. None of them is formalized in Lean's Mathlib. The platform has neighbouring results that are not the same statements: Poljak's divergent-series theorem for concave piecewise-linear maximization (in Validation of Subgradient Optimization I), and rate bounds for Lipschitz objectives (First-Order and Stochastic Optimization Methods for ML II, Understanding Machine Learning X). This mission adds the general convex case with normalized steps, the dichotomy for unnormalized steps, and finite termination.
The standard rate analysis of the subgradient method bounds by . It then needs a uniform bound on , which is exactly what is not assumed here. Nothing a priori keeps the iterates in a bounded set, and the subgradients of a general convex function (for instance , the source's example on p. 26) grow without bound away from ; with unnormalized steps this makes the method diverge. Even with normalized steps, the distance to a minimizer decreases only outside a neighbourhood of whose size is of the order of the current step, so a monotone decrease argument gives at best a subsequence with small function values. Convergence of the whole sequence to zero is a stronger statement, and boundedness of is essential to it.
EuclideanSpace ℝ (Fin n); is real-valued (finite everywhere) with ConvexOn ℝ Set.univ f.g is arbitrary, with the hypothesis ∀ x, IsSubgradient f x (g x). The starting point is arbitrary.normalizedIter, plainIter, resetIter); the stepsize sequence is h : ℕ → ℝ with h (k+1) used at step . In (2.4), a zero subgradient is handled by an explicit branch that repeats the current iterate (which is then in ). No statement relies on Lean's convention .Metric.infDist, and is ⨅ y, f y.Tendsto (fun N => ∑ k ∈ Finset.range N, h (k+1)) atTop atTop. is "for some , eventually ", so it cannot hold vacuously for an unbounded sequence.Needed infrastructure: continuity of convex functions on (in Mathlib), compactness of sublevel sets when is bounded, and the geometry of level surfaces relative to supporting hyperplanes. The one-step inequality (2.3) and the level-set compactness lemma are reusable by the later missions of this series (linear rate, Polyak's stepsize, stochastic subgradient). Contributions that prove Eq. (2.3) or Theorem 2.1 first are welcome.
Gradient methods assume a continuous gradient; subgradient methods assume convexity. Many objective functions met in practice satisfy neither. Shor's example is economic planning, where components of the objective are piecewise-smooth, not necessarily convex functions of a parameter describing the productivity of a unit, and where minimax formulations produce kinks as a rule (Shor, Minimization Methods for Non-Differentiable Functions, Springer 1985, §1.4, p. 17, DOI 10.1007/978-3-642-82118-9). Such problems need a class of functions wide enough to contain piecewise-smooth and minimax functions and narrow enough to carry a usable replacement for the gradient.
Shor's answer is the class of almost differentiable functions, introduced in his 1972 work and presented in §1.4 of the book, together with the almost-gradient, a limit of gradients taken at nearby points of differentiability. The capstone of the section, Theorem 1.15, connects this class with convex analysis: every convex function on is almost differentiable, and its almost-gradients are subgradients. This is what lets the later chapters treat convex minimization and almost-differentiable minimization with one set of tools. Clarke's generalized gradient of locally Lipschitz functions (Clarke 1975) is the closest relative; Shor's definition differs in requiring the gradient to be continuous on its domain (p. 19).
Let denote -dimensional Euclidean space with inner product and norm . For , write and for the gradient at .
A function is almost differentiable if
An almost-gradient of at is a vector that is an accumulation point of a sequence with and . The set of almost-gradients is . A generalized almost-gradient is a point of the closure of the convex hull of .
A vector is a subgradient of at if for all ; for convex the set of subgradients is the subdifferential .
In Lean these objects are AlmostDifferentiable f, almostGradients f x₀ and IsSubgradient f x₀ g in the namespace ShorNonsmooth.AlmostDiff, with = EuclideanSpace ℝ (Fin n).
For convex ,
The printed statement says the almost-gradients "coincide with" the subgradients. As a set equality this is false (for on , while ), and the book's proof establishes the inclusion. The goal is the inclusion.
The result. Theorem 1.15 embeds convex functions into the almost differentiable class and identifies each almost-gradient of a convex function as a subgradient. Consequently any method that only needs almost-gradients (limits of gradients at nearby differentiable points, which is what a numerical procedure can actually compute) produces valid subgradients when applied to a convex function. Theorem 1.14 supplies the compactness that makes usable as a set-valued substitute for the gradient.
Formalizing it. All results here are classical and proved on paper. Mathlib contains Rademacher's theorem for Lipschitz functions (LipschitzWith.ae_differentiableAt) and local Lipschitz continuity of convex functions on open sets; it does not contain the continuity of the gradient of a convex function on its domain of differentiability, nor any notion of almost-gradient. The mission produces those, together with a formal record that the printed "coincide" is an inclusion. A formal proof of the true equality would be a welcome further contribution.
Two parts of the goal carry real content. The first is condition (c): the gradient of a convex function, restricted to the set where it exists, is continuous. The book cites this from the literature; it is not a consequence of Rademacher's theorem, which gives differentiability almost everywhere and says nothing about how gradients at nearby points relate. The second is condition (b) in a form Lean accepts: Rademacher's theorem in Mathlib is stated for globally Lipschitz functions, while a convex function on is only Lipschitz on bounded sets, so the almost-everywhere statement has to be assembled from local pieces. The passage from gradients to subgradients in the second conjunct is comparatively routine.
The analogous closure properties claimed on the same pages for sums, products and maxima of almost differentiable functions (Theorems 1.16 and 1.17) are false as printed and are not targets; see the formalization scope.
EuclideanSpace ℝ (Fin n); is allowed and harmless. Functions are total and real-valued; convexity is ConvexOn ℝ Set.univ f.gradient f x; condition (c) is ContinuousOn (gradient f) {x | DifferentiableAt ℝ f x}, continuity of the restriction in the subspace topology.∀ S, Bornology.IsBounded S → ∃ L, LipschitzOnWith L f S. Condition (b) is ∀ᵐ x ∂volume, DifferentiableAt ℝ f x.MapClusterPt) of the gradient sequence, not its limit; the points may equal .Infrastructure that is reusable beyond this mission: continuity of the gradient of a convex function on its domain; Rademacher's theorem for locally Lipschitz functions on ; the almost-gradient set and its compactness. Contributions that prove these as standalone lemmas are welcome.
Average cost control of queues rests on a small amount of Markov chain theory: when does a chain with costs have a well defined long-run average cost, and how can that be checked for a concrete model with an unbounded state space? Appendix C of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, doi:10.1002/9780470317037) collects this material for countable state spaces and packages it in one hypothesis, the standard chain. Chapters 7–10 of the book verify this hypothesis for the Markov chains induced by stationary policies in admission, routing and service-rate control models, and use its consequences to prove existence of average cost optimal policies.
The tools are Lyapunov functions in the sense of Foster (1953): a nonnegative function on the states whose expected one-step change is negative away from a finite set. Foster's criterion for positive recurrence, and its refinements bounding expected first passage times and costs, are the standard way to verify stability of queueing networks (Meyn and Tweedie, Markov Chains and Stochastic Stability, 1993/2009).
A Markov chain on a countable set is given by transition probabilities with . is the state at time and the -step transition probability (). State leads to if for some ; states that lead to each other communicate, which partitions into communicating classes.
For a nonempty the first passage time from is given , and ; is the case and the expected return time. The taboo probability is the probability of going from to in steps without visiting at the intermediate times, and is the expected number of visits to at times . A state is transient if and positive recurrent if ; a positive recurrent class is a communicating class of positive recurrent states. The steady state probability is (zero when ).
Each state carries a finite cost . The expected average cost over from is
is the expected cost of a first passage (defined when ), and is the average cost on a positive recurrent class . The chain is standard (Definition C.2.5) if for a distinguished state
If is standard, then is the union of a positive recurrent class and a set of transient states, , and
The statement fixes no constants: it asserts that the average cost exists, is finite, and does not depend on the initial state.
Proposition C.2.6 is what makes the standard hypothesis useful: an average cost criterion that is a genuine limit, finite, and independent of the initial state, even for chains with transient states and unbounded state spaces. Every average cost optimality result of the book that works with a stationary policy's induced chain (the (SEN) and (BOR) assumption sets, the approximating-sequence method, the continuous-time chapter) calls on this proposition or on the Lyapunov criteria of Remark C.2.7 to establish its hypotheses for queueing models.
All results of the mission are classical and proved in the literature; parts are stated in the book without proof and referred to Chung (1967), Grassmann et al. (1985) and renewal theory. None of them has been machine-checked in this form as far as the platform and Mathlib show: Mathlib has kernels and Ionescu-Tulcea trajectories but no countable-state Markov chain classification, no first passage calculus, and no Foster–Lyapunov criterion. Existing platform results on countable chains (the Levin–Peres–Wilmer series) treat irreducible chains without costs. A complete development here produces a reusable library of first passage identities, Foster–Lyapunov bounds for times and costs, and average cost limits on reducible chains.
The Lyapunov bounds (C.1.5, C.2.3) are telescoping arguments, but they require a clean handling of truncated passages and of sums that may be infinite: (C.7) is an inequality between possibly divergent series, and the step "iterate times and let " must be made rigorous for -valued expectations.
The central difficulty is part (iii) of the goal for transient initial states. On the class , the limit of is a renewal reward theorem over successive returns to ; from a transient state the first cycle has a different law, so a delayed renewal reward argument is needed, and it has to cover the case where costs are unbounded. The obvious approach, bounding between and the average over the first steps of the chain started in , fails because need not converge (periodic classes) and because finite does not bound individual cost terms. Proposition C.1.2's uniqueness and the Kac-type identity of C.1.4(iv) likewise need the full cycle decomposition of a positive recurrent class.
The chain is a structure MC S with P : S → S → ℝ≥0∞ and ∑' j, P i j = 1, over a countable type S; costs are C : S → ℝ≥0. Probabilities and expectations are ℝ≥0∞-valued sums over finite paths Fin (t+1) → S, so every quantity is defined without summability side conditions and may be . The first passage time is ; is the expectation of from its law (and when ), not defined by the recursion (C.4), so that (C.4) is a theorem. counts visits at times . is computed over first passage paths and is used only when , as in the book. is , which the book states equals the Cesàro limit . is meaningful for , and limits are taken in . The drift conditions and are written in the equivalent additive form , which is equivalent for finite and makes the case fail, as it does in the book.
A trivializing formalization, such as defining or by the equations (C.4) or (C.13), defining as the limit of , or allowing a standard chain whose return time or return cost to is infinite, is ruled out: standard requires and for every including , and each quantity is defined from path probabilities.
Needed infrastructure: path-sum manipulation in (first-step and last-step decompositions), the ratio limit / renewal reward theorem for a positive recurrent class, and the delayed version for transient starts. The first passage calculus and the Lyapunov bounds are reusable by the book's other chapters on average cost, which state the standard property for policy-induced chains. Contributions of lemmas on path sums and of an independent renewal reward library are welcome.
In the theory of Markov decision chains two cost criteria dominate: the discounted cost, in which a cost incurred at time is weighted by for a discount factor , and the average cost, the long-run cost per unit time. A standard route to average cost optimal policies is to solve the discounted problem and let . That route needs a precise link between the two criteria for a single sequence of expected costs : the discounted cost multiplied by on one side, the running average on the other. Appendix A.4 of Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) supplies this link as Theorem A.4.2, and the book invokes it whenever it passes from discounted to average cost (for instance in Chapter 6, where it is applied to ).
The result belongs to classical summability theory.
Let be nonnegative terms with . For the power series
always has a sum, possibly , because its partial sums increase. Its radius of convergence is . The partial sums are for . Two ways of averaging the sequence are compared:
For the constant sequence both equal . In the Lean development these are U, radius, w, cesaroMean and abelMean in the namespace SennottDP.Tauberian, all valued in ℝ≥0∞. The proof also uses the function of Fig. A.1, equal to on and to on .
and the following are equivalent: (i) all terms in (A.28) are equal and finite; (ii) exists and is finite; (iii) exists and is finite.
No growth or boundedness condition on is assumed: nonnegativity is the only Tauberian condition.
The result itself. Theorem A.4.2 lets every statement about for a discounted value be read as a statement about long-run average cost, and conversely. The strict cases of Example A.5.1 show why the book must work with and rather than limits: average costs of policies need not exist as limits, even for bounded costs.
Formalizing it. Mathlib contains Abel's theorem for convergent series (Mathlib/Analysis/Complex/AbelLimit.lean) and Cesàro convergence of convergent sequences, but no Tauberian theorem. The pinned checkout has no file mentioning "Tauberian", and neither does the platform. The mathematics has been proved since 1914. Formalizing it here adds:
The Abelian inequalities (A.28) follow from rearranging the series. The converse (iii) ⇒ (ii) does not: the first idea, recovering from at , fails, because knowing near controls only weighted averages of all the , not a sharp truncation. Some positivity argument is unavoidable, since the converse fails for signed sequences (for example ). The sharp truncation at corresponds to the discontinuous weight . Passing from polynomial weights to the jump function requires uniform approximation together with the nonnegativity of the at every step.
The infinite values add bookkeeping. A single makes every term of (A.28) infinite, and forces on .
Conventions the statements commit to:
ℝ≥0∞) with . , the Abel means, and the Cesàro means are ℝ≥0∞-valued, with ℝ≥0∞ sums (no summability side conditions).liminf. "Exists and is finite" means convergence in to some .𝓝[<] 1.atTop on ; the value is irrelevant.List.TFAE.A trivializing formalization is ruled out. Real-valued / would make (A.28) hold by junk values on unbounded sequences; hypotheses such as boundedness of would replace the theorem by an easier special case; and a definition of "exists and is finite" allowing would make (ii) hold for . None of these is used. As sanity checks: for all four terms of (A.28) equal , and for all equal and (i)–(iii) all fail.
A complete development needs:
polynomialFunctions.topologicalClosure);𝓝[<] 1.Reusable beyond this mission: the ℝ≥0∞ power-series toolkit and the Karamata argument for general continuous weights (milestone 8). Contributions welcome: proofs of any milestone, and alternative proofs of (iii) ⇒ (ii).
Linn Sennott's Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) studies Markov decision chains with countably many states, finite action sets and unbounded nonnegative costs. Its main computational device, the approximating sequence method (Definition 2.5.1, p. 28), replaces the countable state space by an increasing sequence of state spaces and the transition law out of each state by distributions on that converge pointwise to the original law. Every convergence argument of that method has the same shape: a sum , an expected cost or value under the -th approximating model, must be shown to converge to , or at least to satisfy a one-sided bound in the limit.
Appendix A, Sections A.1–A.2 (pp. 270–278), collects the analysis results used for this. The author proves them for sums over countable sets rather than general integrals, so they need no measure theory, and the proofs of the discounted-cost and average-cost approximation theorems (Chapters 4 and 8) cite them. This mission formalizes that appendix section as a self-contained unit.
Let be a countable set and a probability distribution on : and . Values of functions are extended reals in , with the convention . For , the weighted sum is
which is well defined, in , whenever the negative parts have finite weighted sum. In Lean this is wsum P u.
A family of approximating distributions for consists of
Since the sets increase to , a fixed state lies in for every large , so and make sense for a function defined only for . In Lean these three conditions are the structure ApproxDist P SN Q, with Q N j .
Under the approximating-distribution hypotheses, let and be finite with for , let and for every , and assume
Then
The results. Proposition A.2.5 and Theorem A.2.6 are the two limit interchanges the approximating sequence method needs. The generalized Fatou inequality gives the lower bound on limits of value functions of the approximating models, and the generalized dominated convergence theorem identifies the limit of expected costs when a dominating function is available. Corollary A.2.7 gives the bounded case, and Proposition A.1.3 moves limits inside the minimization of an optimality equation. Proposition A.1.10 compares Cesàro averages with the sequence itself, which the average-cost chapters use.
Formalizing them. All statements are classical and proved in the book. A.1.7, A.2.1, A.2.3 and A.2.4 are, after translation, instances of Mathlib's Fatou lemma (MeasureTheory.lintegral_liminf_le) and dominated convergence theorem for a discrete measure. The mission states them in the book's discrete, extended-real form so later chapters can cite them by number. The versions in which the distribution and its support change with (A.2.5–A.2.7) are not in Mathlib in this form; the generalized dominated convergence theorem appears in the measure-theoretic literature (Royden, Real Analysis, Ch. 4) but has no Lean formalization. None of these statements has been formalized for this book.
For the generalized results, Mathlib's Fatou lemma and dominated convergence theorem do not apply directly: they fix one measure, while here both the weights and the support change with . The dominating function also changes with and is not integrable uniformly in ; only the convergence of its expectations is assumed. For small , may even be infinite, and then has no value.
A second difficulty is bookkeeping in the extended reals. Lower limits may be , products use , and a sum with a term and a term is undefined. The inequality of Proposition A.1.5 holds only when that indeterminate form is excluded. The bound in A.2.1 and A.2.5 cannot be dropped: Examples A.1.9 and A.2.2 of the book show the inequalities fail without it.
[Countable S]. Probabilities are ℝ≥0∞-valued with ∑' j, P j = 1, and is Q N j. Extended-real values are EReal, and nonnegative extended values (A.1.7, A.1.8) are ℝ≥0∞. Limits and lower and upper limits are along atTop in ℕ. The book's convention (Remark A.1.2) needs nothing extra, since only large matter.(SN N).indicator (Q N) times the function. Values of and for never enter any statement, and the hypotheses on (, ) are imposed only on , as in the book.wsum, the difference of the weighted positive and negative parts, each in [0,∞]. When both are infinite the book's sum is undefined and wsum returns . Every sum used in a hypothesis or conclusion is defined, except possibly for finitely many in limit statements, where it does not matter.EReal, since the book allows extended-real limits (p. 271). The hypotheses force them to be finite wherever .wsum returns its junk value could make an inequality trivial. Every left-hand side here is a lower limit of sums whose negative parts are bounded, or a limit of eventually defined sums, so no statement holds only because of that junk value. Real-valued tsum with its junk value is not used anywhere.lintegral_liminf_le for the counting measure, and lemmas relating wsum to Mathlib's tsum and to integrals against Measure.sum (fun j => P j • dirac j), can be reused by the other missions of this series.MeasureTheory.lintegral_liminf_le, MeasureTheory.tendsto_integral_of_dominated_convergence).Many queueing systems evolve in continuous time: customers arrive according to a Poisson process, services take exponentially distributed times, and a controller may change the service rate, admit or reject customers, or route them whenever the state changes. Minimizing the long-run average cost of such a system is a standard problem in the control of queues (Lippman 1975; Puterman 1994, Ch. 11; Sennott 1999, Ch. 10). The continuous time model does not fit directly into the discrete time theory of Markov decision chains developed in the earlier chapters of Sennott's book, because time spent in a state now matters and the natural average cost is a ratio of expected cost to expected elapsed time.
This mission formalizes Sections 10.1–10.4 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999): the elementary properties of the exponential distribution, the continuous time Markov decision chain and its average cost, a reduction of the continuous time problem to an auxiliary discrete time Markov decision chain, and the theorem stating that finite state approximating sequences of the auxiliary chain compute optimal average costs and optimal stationary policies of the continuous time chain. The chapter closes with an explicit average cost computation for the M/M/1 queue with service rate control.
A random variable has the exponential distribution with rate if for . A function is if as .
A continuous time Markov decision chain (CTMDC) has a countable state space and, for each , a finite nonempty action set . Choosing in state incurs an instantaneous cost and a cost rate in effect until the next transition. The time until the next transition is exponential with rate , so its mean is ; the next state is with probability , where . A policy chooses, at each transition, an action (possibly at random) from the history of past states, actions and sojourn times; a stationary policy chooses in state . With the cost and the time of the first transition periods, the average cost and the minimum average cost are
Assumption (CTB) requires constants and with . The auxiliary MDC has the same states and actions, costs , and transition probabilities for , . Its average cost and minimum average cost are those of Chapter 2. Assumption (CTAC) is .
An approximating sequence for uses finite state spaces increasing to and transition probabilities on converging to . The (AC) assumptions ask for constants and functions on solving
with , for a constant , and , .
Under (CTB), (CTAC) and the (AC) assumptions for an approximating sequence of :
and every limit point of a sequence of stationary policies realizing the minimum in (10.21) satisfies and . The goal leaves the chain, the approximating sequence and the constants of (CTB) arbitrary.
The goal theorem turns the average cost control of a continuous time chain on an infinite state space into a finite computation: solve the optimality equation (10.21) of a finite truncation of the auxiliary chain, let the truncation grow, and read off the optimal average cost and an optimal stationary policy of the original continuous time chain. The auxiliary chain is the book's form of uniformization, and the result is what licenses the numerical study of the M/M/1 service rate control problem in Section 10.4 and of the M/M/K and polling models in Sections 10.5–10.6. Proposition 10.4.1 gives the closed-form benchmark against which the computed optimal policy is compared.
The results are proved in the book, some with details left to the reader (Lemma 10.3.2(ii), Problem 10.10), and the goal rests on Theorem 8.1.1 and Lemma 7.2.1 of the same book. None of them has, as far as a search of Mathlib and the Prove2Me catalogue shows, a machine-checked proof: Mathlib provides the exponential law (ProbabilityTheory.expMeasure) and its distribution function, but not memorylessness or the minimum of independent exponentials, and no continuous time Markov decision model. A formalization would supply these, together with a checked average cost comparison between a continuous time chain and its discrete time auxiliary chain.
The obvious argument compares the two chains policy by policy, but the policy classes differ: a policy for may change action in every time slot, including slots where the state does not change, while a policy for acts only at transitions and may use the observed sojourn times. Only the stationary policies coincide. The lower bound therefore cannot be obtained by transferring policies, and it is exactly what Assumption (CTAC) supplies. The upper bound requires passing from the discrete time inequality (10.20) for the limit point to a bound on a ratio of expected cost to expected time in continuous time, where the denominator depends on the policy; the uniform bounds of (CTB) on the mean sojourn times are what control it. Inside Lemma 10.3.1 the function is only bounded below, so the telescoping of expectations must be justified without integrability of from above.
The state space is a countable type S, actions a type Act, and action sets A i : Finset Act; the CTMDC and MDC structures hold data, and their axioms (nonempty action sets, nonnegative costs, positive rates, stochastic transition rows with ) are separate predicates. Transition probabilities are ℝ≥0∞-valued; costs, rates and the functions are real. Expected costs, expected times and all average costs are ℝ≥0∞-valued, so is a legitimate value, and they are compared with real constants in EReal; the limits superior and inferior of (AC) are taken in EReal. The expected cost of transition periods under a general policy is a recursion over the periods in which the sojourn time is integrated against expMeasure ν(i,a) and the next state is drawn independently from ; policies are measurable in the past sojourn times. In (10.15) and (10.20) the convergence of the series is part of the inequality. The strict inequality of (CTB) is kept strict (as a positive margin); weakening it to would make vanish or turn negative.
The average cost is a ratio of expectations, not the expectation of a ratio, and the infimum ranges over history dependent randomized policies that may use sojourn times; replacing either by a stationary-only class, or dropping (CTAC), gives a different theorem.
A complete development needs: expected rewards of a chain with exponential holding times, the average cost theory of Chapter 8 for the auxiliary chain (Theorem 8.1.1 and Lemma 7.2.1, restated here as needed), and renewal-reward reasoning for Proposition 10.4.1. The exponential-distribution lemmas are reusable beyond this mission and are welcome as independent contributions.
In a discrete-time queue the service of a customer lasts a random number of slots. When such a system is modelled as a Markov decision chain (Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, DOI 10.1002/9780470317037, Chapter 9), the state must record how much service is still owed, and the controller only observes that a service has lasted slots and is not yet finished. The relevant random quantity is then the residual life : the remaining service time given that slots have elapsed without completion. Verifying the book's average cost assumptions for such a model requires bounds on expected first passage times and costs, and these reduce to moment bounds on and on the residual lives .
Section 9.2 isolates a single condition that makes those bounds available: the expected remaining service time is bounded uniformly in the elapsed time. The concept of mean residual life comes from reliability theory, where is the lifetime of a component and is its expected remaining lifetime at age . This mission formalizes Section 9.2 of the book, together with the moment computation for batch arrivals (Lemma 9.5.2) that the same verification uses.
Let be a random variable with values in and distribution , . Write and for , so and . The -th moment is
For with , the residual life has distribution
with ; its tail is , and is the mean residual lifetime.
The distribution of has bounded mean residual lifetimes (BMRL-, Definition 9.2.4) if there is a finite constant with
and it is BMRL if it is BMRL- for some .
Three families appear by name: the geometric distribution of the number of Bernoulli() trials to the first success, ; the negative binomial of the number of trials to the -th success, for ; and the truncated Poisson , for .
For Lemma 9.5.2, batches of customers arrive in each slot; the batch sizes are independent with common distribution , mean and second moment , and is the number of arrivals in slots.
If the distribution of is BMRL, then
The goal fixes no constant: it asserts only that a uniform first-moment bound on the residual lives forces every moment of to be finite.
The result itself. Proposition 9.2.5 turns a condition that is easy to check for concrete service distributions, and natural for services (a service whose expected remaining duration grows without bound as it goes on is undesirable), into the moment bounds that the average cost analysis consumes. With Proposition 9.2.6 it shows that the most common unbounded service distributions on have finite moments of all orders; with Lemma 9.5.2 it supplies the linear and quadratic growth of expected arrivals and their second moments that the verification of the (WAC) assumptions for the batch-arrival queue of Example 9.3.1 needs (Section 9.5). Every bounded distribution is BMRL as well (the book's Problem 9.3).
Formalizing it. All results here are proved in the book; none has a machine-checked proof on the platform or in Mathlib, which has geometric and Poisson distributions but no residual lives, negative binomial or truncated Poisson laws. A complete development gives a reusable tail-sum calculus for moments of -valued random variables in , a residual-life construction for discrete distributions, and the BMRL property of three standard families. The platform's mean residual life order (the "Stochastic Orders II" mission, Shaked–Shanthikumar) compares two variables; BMRL is a uniform bound on one variable's residual lives and is not an order, so none of that material states these results.
BMRL controls only first moments, of the conditional laws ; the goal asks for moments of every order of itself. Bounding by expanding for each fixed gives nothing, because each single bound is compatible with a heavy tail: the uniformity in is essential. The residual lives are also only defined where , so every argument must handle distributions with bounded support separately. Proposition 9.2.6 requires explicit control of ratios of tail sums for three families; for the negative binomial and truncated Poisson the tails have no closed form.
IsDistOnPos). , moments and residual-life moments are ℝ≥0∞-valued series; an infinite moment is and "finite" means . No Bochner integral is used, so a finite-moment conclusion cannot hold vacuously through an integrability default.geometricPMF does.iIndepFun) batch sizes of common law , expectations as lower Lebesgue integrals, and only assumption (BA1), , which is the part of the book's (BA) that concerns arrivals.Controlled queues, inventories and communication links are run for a long time, and the quantity an operator usually cares about is the long-run average cost per period rather than a discounted total. The average cost criterion is harder to work with than the discounted one: its value is a of Cesàro means, it is not given by a contraction, and for general (history dependent, randomized) policies the limit need not exist. Chapter 6 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) treats the case of a finite state space, where the strongest results hold: an average cost optimal policy exists, can be taken stationary, and can be obtained as a limit of discount optimal policies as the discount factor tends to one.
The results go back to D. Blackwell, "Discrete dynamic programming", Ann. Math. Statist. 33 (1962), who showed that for finite states and actions some stationary policy is discount optimal for all discount factors close to one. Such a policy is now called Blackwell optimal. Sennott's Chapter 6 derives average cost optimality of this policy and the multichain average cost optimality equation from it, in the notation used throughout the book.
A Markov decision chain (MDC) has a countable state space , a finite nonempty action set in each state , nonnegative finite costs , and transition probabilities with . A policy chooses the action at time from a distribution on that may depend on the whole history . A stationary policy always chooses a fixed action in state .
With the state and action at time and , define
All infima range over all general policies, and every quantity may equal . A policy is discount optimal if , and average cost optimal if .
For a stationary policy on a finite state space, the induced Markov chain splits into positive recurrent classes and transient states. With the probability of reaching from , distinguished states , and , the relative value function is .
For an MDC with a finite state space there are and one stationary policy such that is discount optimal for every , is average cost optimal, and
with three equivalent conditions for equality. 3. Proposition 6.2.2. For finite and stationary , . 4. Proposition 4.5.1, Proposition 4.5.4, Corollary 4.5.5. The power series structure of in ; monotonicity and left continuity of ; continuity under bounded costs. 5. Theorem 6.3.1. For the policy of the goal, exists, and
together with the limit identities (i)–(iii) and the optimality criterion (v). 6. Proposition 6.3.3. with as .
The goal says that on a finite state space nothing is gained by randomizing or by remembering the past when minimizing average cost, and that the minimum average cost is the vanishing-discount limit of the discounted value function. This justifies computing average cost optimal policies through discounted problems and value iteration, the route taken in the rest of Chapter 6 and, via approximating sequences, for countable state spaces in Chapters 7 and 8. Theorem 6.3.1 supplies an optimality equation without any unichain or communication assumption. The book's Example 6.3.2 shows that the inequality in that equation can be strict, and that a stationary policy attaining the minimum need not be optimal.
The results are classical and proved in the book. No machine-checked version of them is known to exist. The platform has average-reward results for unichain finite MDPs with Markov policies (the Puterman series) and an average-cost optimality equation under recurrence assumptions (the Bertsekas series). Neither covers existence of a Blackwell optimal policy against the class of all history dependent randomized policies, or the multichain equation. A formal development also yields reusable infrastructure: the law of a controlled process under a general policy, first passage quantities of finite chains, and the Abelian inequality between Abel and Cesàro means of a nonnegative sequence.
The obvious argument picks, for each , a stationary discount optimal policy and lets . Finiteness of the set of stationary policies gives one policy that is optimal along some sequence , but not on an interval. Excluding infinite switching between two policies requires the analytic structure of (Proposition 4.5.3), which in turn rests on matrix inversion of . Passing from the discounted criterion to the average one requires an Abelian inequality for nonnegative series whose terms may be infinite (Proposition 6.1.1), and comparison against general policies rules out any argument that works only within stationary or Markov policies. For Theorem 6.3.1 the difficulty is the multichain structure: the relative value function has to be assembled class by class from first passage times and costs, and its limit must be identified.
S; [Countable S] for Section 4.5 and Proposition 6.1.1, [Fintype S] from Section 6.2 on, as in the book. Actions form a type Act with A i : Finset Act nonempty. Costs are in ℝ≥0, transition probabilities in ℝ≥0∞.A i. Stationary policies embed as degenerate policies. The law of the process is built from this data, and every infimum ranges over all general policies.ℝ≥0∞, so is represented. is the filter 𝓝[<] 1. On a finite state space these quantities are finite. The real valued objects of Section 6.3 (, , , equation (6.6)) are therefore formed with toReal, and this switch from ℝ≥0∞ to ℝ happens only in Theorem 6.3.1 and Proposition 6.3.3.p/q without requiring . Each is excluded here: and are infima over all general policies, one pair is quantified before all , and the denominator is required to be nonzero on .Useful infrastructure includes rational functions of one real variable and their finitely many sign changes, the resolvent of a stochastic matrix, the Abelian inequality for -valued sequences, and renewal-reward identities for finite chains. Contributions of general lemmas on these topics are welcome, as are proofs of individual milestones.