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?
A Markov decision problem models a system that is observed once per period and controlled by choosing an action: the action earns an immediate income and determines the probabilities of the next state. Inventory control, machine replacement, queue admission and many reinforcement-learning benchmarks are of this form. With future income discounted by a factor , Howard (Dynamic Programming and Markov Processes, 1960) showed how to compute an optimal policy by policy improvement. The undiscounted problem () is harder, because total income is typically infinite.
David Blackwell's Discrete Dynamic Programming (Ann. Math. Statist. 33 (1962) 719–726) treats as a limit of . Its Theorem 5 shows that some stationary policy is optimal simultaneously for all discount factors sufficiently close to . Such policies are now called Blackwell optimal, and the result is the base of sensitive discount optimality (Veinott, 1969) and of the standard textbook treatment of average-reward problems (Puterman, Markov Decision Processes, 1994, Ch. 10).
Timeline. Howard (1960): policy iteration for discounted and average-reward finite problems. Blackwell (1962): Theorem 5 (Blackwell optimal stationary policies exist) and the characterization of nearly optimal stationary policies (Theorem 4, the subject of the companion mission). Miller and Veinott (Ann. Math. Statist. 40 (1969) 366–370), Veinott (Ann. Math. Statist. 40 (1969) 1635–1660): Laurent expansions of in and -discount optimality.
There are finitely many states and a finite set of actions, every action available in every state. In state , action yields income (any sign) and moves the system to state with probability ; each is a probability vector.
A decision rule is a function from states to actions; is the finite set of decision rules. A policy is a sequence in : on day , in state , action is used. Policies are deterministic and Markov but may change with time. The policy uses on day and then follows ; uses every day and is called stationary.
For , is the vector and the Markov matrix . With and , the return of at discount factor is
a vector indexed by the initial state. Vectors are compared coordinatewise; means and .
A policy is -optimal if for every policy . Following §4 of the paper, a policy is optimal if it is -optimal for all sufficiently near .
There exist a decision rule and such that
One and one serve every competing policy and every .
The result. Theorem 5 shows that the infinitely many discounted problems near share a common optimal stationary policy. Such a policy is also optimal for the long-run average criterion, which settles the existence of average-optimal stationary policies in finite models without any recurrence assumption. It also justifies computing undiscounted solutions as limits of discounted ones, and it is the first case of the sensitive optimality criteria developed later.
Formalizing it. The theorem is classical and proved in the paper and in the textbooks; there is no machine-checked proof of it in Blackwell's model on the platform. A related open item, SennottDP.AvgFinite.prop_6_2_3_blackwell_optimal, states the textbook version for nonnegative costs and randomized history-dependent policies; the present mission is Blackwell's own formulation with incomes of either sign and deterministic Markov policies. A complete development also yields a verified policy improvement theorem (Theorem 3) and the rationality of discounted values in , both reusable for any finite-state discounted model.
The Corollary gives, for each , some optimal stationary policy, and is finite, so one is -optimal for infinitely many accumulating at . The obvious argument stops there: optimality on a sequence of 's says nothing about the 's in between, and a pointwise limit argument cannot produce a whole interval . The step that fails is passing from "frequently" to "eventually", and it needs structural information about how depends on , not just continuity. A second difficulty is the comparison class: optimality must hold against all time-dependent policies, not only the finitely many stationary ones, so the final step has to bring the Corollary back in for every near .
States and actions are finite nonempty Lean types St, Act; decision rules are functions St → Act and policies are sequences ℕ → St → Act, indexed from (π 0 is Blackwell's ). Incomes are real-valued with no sign restriction. The law of motion law s a s' satisfies the published predicate IsTransitionKernel. is the ordered matrix product and is the tsum of the series, which converges absolutely for ; every statement at a fixed assumes , and nothing is stated for . Vector inequalities are coordinatewise, and the strict order is " and ", not coordinatewise strict. " sufficiently near " is "there is such that for every ". The paper's §4 phrase is encoded as -optimality, so no supremum over policies appears.
The word "optimal" has two meanings in the paper: at one fixed (§3, the Corollary) and for all near (§4, Theorem 5). The Lean development keeps them apart as IsBetaOptimal β and IsOptimal. A statement of Theorem 5 at a single , with "there exists ", for a set of 's accumulating at , or against stationary policies only would be a different and weaker theorem; the goal rules all of these out.
Needed infrastructure: summation and shifting of the discounted series, Neumann series for stochastic , Cramer's rule to express as a ratio of polynomials in , and the fact that a nonzero polynomial has finitely many roots. The policy improvement theorem and the rationality lemma are reusable beyond this mission. Proofs of individual milestones are welcome independently.
Selfish routing and resource sharing are modelled by congestion games: each player picks a set of shared resources, and the cost of a resource grows with the number of players using it. The price of anarchy, introduced by Koutsoupias and Papadimitriou (STACS 1999), measures how much worse the social cost of a worst Nash equilibrium is than the optimum. For non-atomic (infinitesimal) traffic with linear latencies, Roughgarden and Tardos (J. ACM 2002) showed the ratio is . Christodoulou and Koutsoupias (STOC 2005) turned to finite (atomic, unweighted) congestion games, where each of players controls one indivisible unit of load, and determined the pure price of anarchy for linear latencies in four settings: asymmetric or symmetric strategy sets, and average or maximum social cost. Awerbuch, Azar and Epstein (STOC 2005) obtained the value for the asymmetric average case independently.
This mission covers the symmetric average-cost entry of that table (Sect. 3.2 of the paper). It shows that when all players share one strategy set, the ratio is not but , which depends on the number of players and tends to only as .
A congestion game has a finite set of players (in Lean, Fin N), a finite set of facilities , for each player a collection of pure strategies , and for each facility a latency . A profile picks for each player (IsProfile). The load is the number of players whose strategy contains (load), the cost of player is
(cost), and the social cost is (sumCost), times the average cost. A profile is a pure Nash equilibrium (IsPureNash) if for every player and every , where replaces by .
Latencies are linear (IsLinear) when with . The game is symmetric (IsSymmetric) when all players have the same strategy set, . The pure price of anarchy of a class of games is the supremum, over games in the class and pure Nash equilibria , of , with .
For every : every pure Nash equilibrium of every symmetric linear congestion game with players satisfies
and some symmetric linear game with players has a pure Nash equilibrium and a profile with and equality. Together these state that the pure price of anarchy of the class is exactly .
The result separates symmetric from asymmetric games for every finite number of players: for the symmetric bound is , for it is , against for asymmetric games with players. Theorem 4 shows the bound is tight, so the function is the exact answer, not an artefact of the proof. The asymptotic value coincides with the asymmetric one, which says that symmetry helps only by a vanishing amount for large populations. Later work on smoothness arguments (Roughgarden, STOC 2009) takes the bound of this paper as its central example.
The theorems are proved in the paper; the authors print the proofs for identity latencies and state that they extend to . No machine-checked proof of these bounds is known to exist. This mission produces a statement for general affine latencies with nonnegative coefficients, the affine forms of the intermediate inequalities, and an explicit family of instances for every , all of which are reusable for the other entries of the paper's table.
The upper bound requires combining the deviation inequalities (player against the strategy of each player in the comparison profile) and then bounding cross terms facility by facility; the step that needs care is that the bound of Lemma 1 holds for integer loads only and fails for real numbers, so any argument that relaxes loads to reals loses the constant. The asymmetric argument, which compares player only with its own optimal strategy , gives and cannot see the dependence on .
For the lower bound, the instance must be a Nash equilibrium against every strategy in the common strategy set, which contains the equilibrium strategies of all other players as well as the optimal ones. Exact equality of the ratio requires the block sizes to be tuned to ; verifying the equilibrium condition involves counting facilities shared by pairs and triples of players.
Players are Fin N with ; facilities are an arbitrary finite type with decidable equality; strategies and profiles are Finsets of facilities, with feasibility a separate predicate. Latencies are real-valued functions of the natural-number load. Linear latencies are affine with nonnegative coefficients, as in Sect. 2 of the paper; the milestone inequalities carry the coefficients explicitly and reduce to the printed displays when , . The Nash condition is in cost form. Upper bounds are stated against every feasible profile , which is equivalent to the bound on without dividing by . All constants are computed in .
The lower bound requires : without it the statement is satisfied by zero latencies or empty strategies, where both sides vanish. Symmetry is a hypothesis of the upper bound and a property of the instance; without it the upper bound is false, since asymmetric instances reach .
A complete development needs finite-sum manipulations (double counting ), the integer inequality of Lemma 1, and an explicit facility type for the instance. The model layer is shared with the other missions of this series. Proofs of the milestones and alternative proofs of the bound are welcome.
The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the cutoff-90 mission already covers every , the new work is the range from 89 to 90.
The argument for was reached by tightening its estimates step by step, starting from 256. With its current choices those estimates stop working below 90, and nobody has yet found a way past that point. It is not known whether 90 is a real limit of the method or only of the choices made so far, so this mission is the smallest test of whether the cutoff can move at all. The accepted proof for and its research note are the natural starting point. The goal theorem below gives the exact statement.
This is an open entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 89 or lower also settles this mission.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryA matching in a graph is a set of edges no two of which share a node. Given a real weight on every edge, the maximum-weight matching problem asks for a matching of largest total weight. It is one of the basic problems of combinatorial optimization: assignment, pairing and scheduling problems reduce to it, and it is the standard example of a combinatorial problem that is solvable in polynomial time although it is not obviously a linear program.
For bipartite graphs the problem is a linear program in disguise: the polytope cut out by nonnegativity and the node-degree inequalities has only 0–1 vertices (the Birkhoff–von Neumann theorem in the square case; Mathlib has it as extremePoints_doublyStochastic). For general graphs this fails already on a triangle, where the vector with every coordinate satisfies all degree inequalities but is not a combination of matchings. Edmonds' 1965 paper (DOI 10.6028/jres.069b.013) adds one family of inequalities, one for each odd set of nodes, and proves that the resulting polyhedron has exactly the matching vectors as its vertices. The companion paper Paths, trees, and flowers gives the cardinality algorithm on which the weighted algorithm of §7 is built.
Timeline:
Let be a finite graph with node set and edge set ; each edge meets two different nodes, its ends. Real variables correspond to the edges . The polyhedron is the set of vectors satisfying
The matching vectors are the vectors with every component or that satisfy (2); they are the incidence vectors of matchings. For edge weights , the linear form (4) is .
The dual program has a variable for each node and for each odd set (, ). Its objective is (5) , subject to (6) and (7) for every edge with ends . For a matching , conditions (8)–(10) are the complementary slackness conditions: at nodes not covered by , equality in (7) on , and every odd set with contains exactly edges of .
A blossom sequence (Theorem (M)) starts from with matching and repeatedly shrinks an odd circuit (a blossom, edges of which are matched) to a single node, carrying node weights and edge weights that obey conditions (a)–(k) of p. 127.
In the Lean development these are Graph, IsMatching, incidence, matchingPolyhedron (), matchingVectors (), W, U, DualFeasible ((6)–(7)), CompSlack ((8)–(10)) and BlossomSequence, all in the namespace EdmondsMatching65.Polyhedron.
The vertices (extreme points) of are exactly the matching vectors of . Hence the maximum weight of a matching equals for every .
The result. Theorem (P) turns maximum-weight matching in general graphs into a linear program over an explicitly described polyhedron, and Theorem (M) with the §5 translation gives a short certificate of optimality for every maximum matching. Together they established the template of polyhedral combinatorics: describe the convex hull of the combinatorial objects by inequalities, and prove the description through linear programming duality and an algorithm. The matching polytope underlies the analysis of the weighted blossom algorithm, separation over odd-set inequalities (Padberg–Rao), and many later integrality results; Edmonds' own §8 states the extension to degree-constrained subgraphs.
Formalizing it. The theorem has been proved since 1965 and appears in every text on combinatorial optimization; this mission asks for a machine-checked proof of the polytope statement for general finite graphs, including parallel edges, together with the duality certificate and the blossom-sequence characterization. The prove2me platform has a proved form of Edmonds' perfect matching polytope theorem on complete graphs in convex-decomposition form (MetricTSP.pm_polytope_decomposition), a different polytope with a different conclusion; nothing states Theorem (P) or Theorem (M).
The inclusion and weak duality are routine. The difficulty is the reverse inclusion: showing that no fractional point of is a vertex. The bipartite argument (a fractional point has a cycle of fractional edges along which it can be perturbed both ways) breaks on odd cycles: perturbing along an odd circuit violates a degree inequality, and the odd-set inequalities that cut off the half-integral points are exponentially many and overlap. The paper's route needs, for every weight vector, an optimal matching together with a dual solution satisfying (6)–(10), and the existence of that certificate is the substance of the weighted matching algorithm: the blossom sequence of Theorem (M) must be constructed, and the translation (11)–(16) from node and edge weights of the contracted graphs to must be verified through the whole shrinking history.
V, a finite edge type E and an end map ends : E → Sym2 V with no loops. Parallel edges are allowed: the contracted graphs of Theorem (M) have them, and Theorem (P) holds for multigraphs; simple graphs are the case of an injective end map.E → ℝ, one coordinate per edge. Vertices are Mathlib's Set.extremePoints ℝ. Odd sets carry an explicit r : ℕ with 1 ≤ r and |S| = 2r + 1; even sets and singletons carry no inequality.|V|.z is a function on all node sets of which only odd sets are read.Gᵢ is a partition of V into blocks; an edge of G is an edge of Gᵢ when its ends lie in different blocks. Each Mᵢ must be a matching of Gᵢ, and all of (a)–(k) appear as fields of BlossomSequence; a sequence missing any of them would make milestone 6 trivial or milestone 5 false.Sym2 V → ℝ) leave non-edge coordinates free and give a polyhedron with no extreme points, and the goal is stated as equality of extreme points, not as a convex-hull identity or as the existence of a dual certificate.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.
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.
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.
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.
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.
Control problems for queueing systems (admission control, routing, service rate selection, inventory replenishment) are naturally modelled as Markov decision chains with a countable state space, such as the number of customers in a buffer, and with costs that grow without bound in the state, such as holding costs proportional to queue length. The expected discounted cost criterion is the first infinite horizon criterion applied to such models, and it is also the tool through which the average cost criterion is treated later in the same book (Chapters 6–8 of Sennott's text reach average cost optimal policies through limits of discounted problems as the discount factor tends to one).
Classical treatments of discounted dynamic programming assume bounded costs, under which the dynamic programming operator is a contraction and has a unique bounded fixed point. That assumption fails for queueing models. This mission formalizes Chapter 4, Sections 4.1–4.4, of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999), which develops the discounted theory for nonnegative, possibly unbounded costs, where value functions may be infinite.
Timeline of the underlying theory:
A Markov decision chain has a countable state space ; for each state a finite nonempty action set ; for each a nonnegative finite cost and a probability distribution of the next state. A policy chooses the action at time at random from a distribution on that may depend on the entire history . A stationary policy always chooses in state ; for it one writes and .
Fix a discount factor . For an initial state and a policy , the -horizon cost with terminal cost zero and the infinite horizon discounted cost are
and the value functions are and , infima over all policies. All of these lie in . A policy is discount optimal if . The discount optimality equation is
With , denotes the set of actions attaining the minimum at .
solves (4.9); every solving (4.9) satisfies ; and every stationary policy with
is discount optimal. No boundedness of costs and no finiteness of is assumed.
In attack order: Lemma 4.1.1 (); Proposition 4.1.2 (a supersolution of the one-policy equation dominates and ); Corollary 4.1.3 (a supersolution of the optimality inequality dominates ); then, beyond the goal, Corollary 4.1.5 ( where ), Proposition 4.2.2 and Corollary 4.2.4 (conditions under which a solution of (4.9) equals ), Proposition 4.3.1 (, and limit points of finite horizon optimal stationary policies are discount optimal) and Proposition 4.4.1 (optimal policies are exactly those concentrated on the sets along histories of positive probability).
Theorem 4.1.4 is the foundation for everything in the book that concerns discounted costs: it produces an optimal stationary deterministic policy, identifies among the many solutions of (4.9) (Example 4.2.1 of the book gives a one-parameter family of finite solutions), and underlies value iteration (Proposition 4.3.1) and the approximating-sequence method of Sections 4.6–4.7. The average cost results of Chapters 6–8 are proved from it by letting . Proposition 4.4.1 describes the full set of optimal policies, including randomized and history-dependent ones.
These are known results with published proofs. The contribution of this mission is a machine-checked development of the discounted theory for countable state spaces with unbounded costs and infinite values, over the general policy class. Related statements on the platform (the monotone-mapping propositions of Bertsekas 1977 in the MonotoneDP missions, and bounded-cost or finite-state discounted results) use different models and are open; no machine-checked proof of the present statements is known to this mission.
The contraction argument that settles the bounded case is unavailable: with unbounded costs the operator in (4.9) has many fixed points, and can equal at some states, so neither uniqueness of fixed points nor subtraction of values is available. The optimality equation compares the infimum over all history-dependent randomized policies with a one-step minimum, so the general policy class and the law of the process under it must be handled directly; restricting attention to Markov or stationary policies begs the question. Every limit exchange (monotone limits of finite horizon costs, the passage to limit points of policies in Proposition 4.3.1) takes place in , where finite-valued arguments do not transfer verbatim.
The Lean development lives in the namespace SennottDP.Discounted. Conventions:
S with [Countable S]; actions form a type Act and A i : Finset Act is nonempty. Costs are ℝ≥0; transition probabilities are ℝ≥0∞ with ∑' j, P i a j = 1 for a ∈ A i.Fin (n+1) → S, Fin n → Act; a policy assigns to every history a distribution on the action set of its last state. The probability of a history is the product of the policy and transition probabilities; expectations are ℝ≥0∞ sums over histories, so no integrability conditions arise.ℝ≥0∞-valued; . The discount factor is α : ℝ≥0 with 0 < α and α < 1. Terminal costs are zero.Useful infrastructure, reusable by the later missions of this series (approximating sequences, average cost): the shift of a general policy after its first step, the Chapman–Kolmogorov identity for the history law, and the computation for stationary policies. Contributions of such lemmas, and proofs of any milestone, are welcome.
Controlled queueing systems (admission control, routing, service-rate selection) are naturally modelled as Markov decision chains whose state is a buffer content and therefore ranges over a countably infinite set. Linn Sennott's Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999, DOI 10.1002/9780470317037) develops the dynamic programming theory for exactly this setting: countable state space, finite action sets, nonnegative and possibly unbounded costs, and value functions that are allowed to be infinite. The book's computational method, the approximating sequence method (ASM), replaces the infinite chain by a sequence of finite truncations and asks when optimal values and policies of the truncations converge to those of the original chain.
This mission is the first of a series on the book. It covers Chapter 3, finite horizon optimization, together with the model of Chapter 2 and three results from Appendices A and B that the chapter uses. The finite horizon theory is the entry point: it is where the book's general policy class, its extended-valued cost criteria and its approximating sequences are first used together.
A Markov decision chain has a countable state space ; for each a finite nonempty action set ; a finite cost ; and for each a transition distribution . A history at time is , and a general policy chooses the action at time from a distribution on : it may use the whole history and may randomize. Stationary policies () and deterministic Markov policies (a stationary policy for each time) are special cases.
Fix a finite terminal cost and a discount factor ( is the undiscounted case). The horizon expected discounted cost of from initial state is
and the value function is over all general policies. Both may be . A policy is optimal for the horizon if it attains at every . For put and let be the set of minimizing it.
An approximating sequence has finite nonempty state spaces increasing to , the same actions and costs, and transition distributions on converging to as . Its value functions are . In an augmentation type approximating sequence, the probability of leaving to is redistributed over by an augmentation distribution . Assumption FH(, ) requires to be finite and at most for every . A stationary policy is a limit point of stationary policies if, along a subsequence, eventually for each .
For fixed ,
and under either condition every limit point of stationary policies with satisfies for all .
Theorem 3.1.2 is the finite horizon dynamic programming equation in the generality the rest of the book needs: the value function is an infimum over history-dependent randomized policies, and the equation holds with infinite values allowed. Its characterization of optimal policies is Bellman's principle of optimality in necessary-and-sufficient form. Corollary 3.1.4 shows that deterministic Markov policies suffice. The discounted chapter builds on these results, since its value function is the limit of finite horizon ones, and so does the value iteration algorithm of the average cost chapters.
Theorem 3.2.3 is the finite horizon case of the approximating sequence method. It says exactly when finite truncations give the right answer, and it reduces the question to Assumption FH, for which Section 3.3 gives checkable conditions. The same structure (a lim inf inequality, a lim sup assumption, a limit point of optimal truncated policies) recurs for the discounted and the average cost criteria in later chapters.
The results are proved in the book. None of them is formalized: the platform has finite horizon dynamic programming only for Markov policies, abstract monotone mappings or finite reward-maximizing MDPs, and nothing on approximating sequences. A formalization contributes a Lean model of Markov decision chains with general policies and extended-valued criteria, which the later missions of the series restate and can merge with this one.
The obvious proof of the optimality equation conditions on the first action and state and then applies the induction hypothesis to the rest of the trajectory. With general policies the rest of the trajectory is governed by a continuation policy that depends on the first state and action, and the decomposition of the path law into a first step and a continuation must be proved from the definition of the process, not assumed. Infinite values also make the "only if" direction delicate: a strict inequality between expected costs becomes an equality once both sides are infinite.
For approximating sequences, the natural idea is to pass to the limit in the optimality equation of . This fails in general. Example 3.2.1 of the book has , because truncation moves probability onto states of high cost and dominated convergence is not available. Only the lim inf inequality holds for free, through a generalized Fatou lemma for approximating distributions. The lim sup side is exactly what Assumption FH supplies. The limit point argument then needs the compactness statement of Appendix B and the fact that a lim inf can be passed through a minimum over a finite set.
The state space is a type S with [Countable S], the actions a type Act, and A i : Finset Act is nonempty. Costs are ℝ≥0, transition probabilities ℝ≥0∞ summing to 1 over S, and all values and expectations are in ℝ≥0∞, so infima over policies are lattice infima and +∞ is a genuine value. A history is the list of past state–action pairs, most recent first, with the current state, and a policy gives a distribution on A i for every history. Expectations are sums over histories of the path probabilities , which is the book's (2.6) and (2.9), not the dynamic programming recursion. The discount factor satisfies in every statement. An approximating sequence is indexed by with a start level ; its value functions are set to for the finitely many at which a given state is not yet in , which does not affect limits.
The optimality equation must not be made definitional by defining or through the recursion (3.2). The policy class must not be restricted to deterministic Markov policies either, since that would make the characterization in Theorem 3.1.2 a different statement. Theorem 3.1.2(ii)(2) is stated with the guard ; the book omits it, and without it the "only if" direction is false (see the item's note).
A complete development needs the first-step decomposition of the path law under a general policy, the generalized Fatou lemma for approximating distributions (Proposition A.2.5, a milestone of the Appendix A mission of this series), and lim inf / lim sup manipulations in ℝ≥0∞. The model definitions are reusable by every later mission of the series. Contributions are welcome at every milestone, including proofs of the definitional sanity facts (for instance ).