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.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
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?
Temporal-difference learning estimates the value of a policy from observed state transitions and rewards. In a finite Markov decision process, fixing a policy produces a Markov chain, so policy evaluation becomes the task of estimating the expected return from each state. Bradtke and Barto's 1996 paper introduced a least-squares temporal-difference method, LS TD, that uses each observed transition in a linear system instead of selecting a learning-rate schedule. Their Theorem 1 states probability-one convergence for trials that end at absorbing states under explicit conditions on state access, rewards, and features. This mission formalizes that result and the statements the authors use to reach it. Bradtke and Barto, 1996.
The result matters for episodic policy evaluation: a learner may collect many short trajectories, each begun from a prescribed start distribution, and update the same estimate as data accumulate. The theorem identifies conditions under which the limit is the true value parameter even when the discount factor is one. That endpoint is useful for undiscounted tasks ending in an absorbing goal state; it also makes the convergence claim more delicate than the standard discounted case. The paper proves the result mathematically. The Lean statements in this mission are targets for machine-checked proofs, not claims of proofs already present in Mathlib. Bradtke and Barto, Theorem 1, pp. 43–44.
Let be a finite, nonempty set of states. After a policy is fixed, is the probability of a transition from to , so each row of is nonnegative and sums to one. A transition earns a deterministic real reward . A state is absorbing when ; let be the absorbing states and the others. The chain is absorbing when some absorbing state can be reached with positive probability from every state. A start distribution gives the state at the beginning of each trial. No state is inaccessible when every state can be reached from the positive support of .
For a discount , the expected immediate reward is . The true value function is defined by the expected return
A feature vector represents state . The matrix has row equal to . The target parameter is a vector for which at every state; it is something the theorem must establish, not an input chosen by a formula. Equation (11) forms an LS TD estimate from the observed feature differences and rewards. Bradtke and Barto, §2, Table 1, Eq. (11).
Figure 2 collects trials. Each starts from , follows while the current state is non-absorbing, and ends upon entry into . The next trial starts with a fresh draw from . The estimator includes transitions taken within trials; a draw that starts the next trial is not an observed transition for Eq. (11). Bradtke and Barto, Figure 2, p. 42.
If every state is accessible from , rewards between absorbing states vanish, the feature vectors on are linearly independent, features on are zero, , and , then the expected-return series converges and there is a parameter satisfying
The theorem keeps the paper's endpoint . The return series' convergence is explicit because a real infinite sum in Lean has a default value when it diverges. Bradtke and Barto, Theorem 1, p. 43.
The milestone list follows the statements used in the paper: almost-sure visits and departure proportions for the trials; invertibility of the non-absorbing block of ; invertibility of for positive non-absorbing weights; Lemma 5's probability-one limit ; and Eq. (12), , together with finiteness of the true parameter. Here . Bradtke and Barto, Lemma 5, p. 43; Proof of Theorem 1, p. 44.
Theorem 1 identifies the target of the asymptotic LS TD estimate: the value function defined from rewards, rather than merely a vector satisfying a sampled linear system. It covers an undiscounted absorbing chain, where a general fixed-point equation for values would fail to determine the values of absorbing states. The zero-reward and zero-feature conditions determine that boundary correctly. The result also explains the dimension condition: one independent feature vector for each non-absorbing state permits exact representation of the return. Bradtke and Barto, pp. 43–44.
A complete formal development would connect finite-state stochastic-process laws, visit frequencies, matrix limits, and the return-defined value function in one checked statement. The reusable parts include a finite row-stochastic chain model, a path-law description of restarts, a filtered least-squares estimator, and results about transient blocks of stochastic matrices. The paper's mathematical proof exists; this mission asks for formal proofs of its Lean targets. It also leaves room for alternative proofs and sharper, separately stated variants without weakening Theorem 1.
Ordinary matrix convergence cannot be applied until the observed transition frequencies are known to converge and the limiting matrix is invertible. A trial has random length, and the process resets after absorption, so a sequence indexed by all restart-process steps does not have the same raw state proportions as a count indexed by trials. The proof must account for both clocks while retaining the in-trial data of Eq. (11). At , a direct geometric-series argument for the value function is unavailable; its finiteness depends on absorption and the reward convention. The matrix itself is singular at the undiscounted endpoint because of absorbing states, while its non-absorbing block is the relevant invertible matrix. Bradtke and Barto, Proof of Theorem 1, p. 44.
The Lean state type is finite and nonempty. The paper evaluates one fixed policy, so is a real row-stochastic matrix and is a deterministic real reward on transitions; there is no action type in the formal statement. Absorbing states are exactly those with , and “absorbing chain” means that an absorbing state is reachable from every state. The paper does not define “inaccessible”; the formalization reads it as unreachable from the positive support of . The state space carries the discrete measurable structure. Theorem 1's restart process and Lemma 5's ordinary Markov chain are each constrained by their finite-dimensional cylinder probabilities, not by assumed transition frequencies.
The feature space is , and equals the cardinality of the subtype . LS TD uses only departures from . Index counts restart-process steps, so the estimate repeats at a restart draw; the paper counts in-trial transitions. These indices have the same asymptotic estimate when transitions continue. The factors in Eq. (11) cancel, and early singular inverses take Lean's total-inverse default. The value function is the return series, and the goal explicitly asserts its summability. The true parameter is existential, never defined by the formula whose convergence the theorem is meant to prove.
The paper defines for absorbing chains as expected departures from per trial. The Theorem 1 visit-frequency milestone normalizes by restart-process steps, which rescales all weights by one positive common factor; Lemma 5's matrix expression is invariant under that rescaling. Lemma 5 itself counts every ordinary-chain transition and carries the paper's “any Markov chain” scope. The milestone on invertibility allows arbitrary weights at absorbing states because their feature rows are zero. These conventions are recorded with each Lean item. Contributions toward the path-law frequency theorem, transient-matrix invertibility, return-series summability, and the matrix limit are all within scope. A vacuous path law or a value function defined from the desired linear equation would not establish the stated goal.
A call center has to decide how many agents to staff. In practice the decision is often posed as a service-level constraint rather than a cost trade-off: use the fewest agents for which the expected waiting cost, or the fraction of customers who wait, stays below a target. Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; journal version in Operations Research 52(1), 2004, doi:10.1287/opre.1030.0081) treat this constraint problem in Section 8 of their paper, alongside the cost-minimization problem of Sections 5–7, and show that a simple square-root staffing rule solves it asymptotically as the arrival rate grows.
The rule matters because it is what practitioners use. Under the classical Erlang-C model, the exact optimum requires evaluating the Erlang-C formula over many staffing levels. The asymptotic rule replaces this with a single equation in the Halfin–Whitt function : when the target is a delay probability (Example 8.5 of the paper), it reduces to staffing servers.
Timeline. Erlang's formula for the M/M/N delay probability dates from 1917. Halfin and Whitt (Operations Research 29, 1981) identified the limit of the delay probability under square-root staffing with integer . Jagers and Van Doorn (Operations Research Letters 5, 1986; SIAM Review 33, 1991) studied the continued Erlang loss and delay functions at non-integer numbers of servers, including their convexity, which is what lets the staffing problem be relaxed to a continuous one. Borst, Mandelbaum and Reiman (2000/2004) used these to prove asymptotic optimality of square-root rules for both the cost and the constraint formulations.
Customers arrive at rate to identical servers, each with service rate ; is fixed while . Stability requires . A customer who waits time units costs , where , is strictly increasing on and for all .
The Erlang-C probability of waiting is
and the conditional waiting cost is . The waiting cost per unit time with servers is
Given a target , the optimal staffing level is the least integer with ; call it .
In the continuous parametrization , define , the continuous Erlang-C function with , and . The Halfin–Whitt function is with the standard normal hazard rate. A staffing function is judged by the rounding gap
It is asymptotically optimal when as .
Suppose that for some and , , i.e. the waiting cost is comparable to the target. Let solve . Then
If for every and solves , then .
The theorem certifies the staffing rule used in workforce-management practice: the excess staffing is determined by one scalar equation involving the Gaussian function and the scaled waiting cost, and rounding the resulting staffing level misses the constraint by a vanishing fraction of the target. Lemma 8.1 is a reusable framework: any approximation that is asymptotically exact at the proposed staffing level yields an asymptotically optimal rule, and the paper instantiates it in three regimes (Theorems 8.2, 8.6, 8.9).
The results are proved on paper. To the best of current knowledge none of them, nor the Halfin–Whitt limit for the continuous Erlang-C extension, has a machine-checked proof. A formalization would produce the first verified heavy-traffic limit of the Erlang-C delay probability, a verified continuous Erlang-C extension with its integer identity, and the convexity facts about and that many staffing papers cite without proof.
The obvious argument is to quote Halfin and Whitt: the delay probability converges to under square-root staffing, so can replace the Erlang-C formula. That limit, as published in 1981, is about integer server counts along sequences with a convergent excess-staffing parameter. The paper needs it for the continuous function at non-integer server counts and for staffing functions that are merely bounded, and it also needs the identity at integers and the monotonicity of in , both cited from Jagers and Van Doorn rather than proved. None of these is in Mathlib. A second obstacle is that the staffing function is defined only implicitly by an equation involving , which depends on the arbitrary cost functions ; nothing a priori prevents it from escaping to infinity, outside the range where the Halfin–Whitt approximation applies. Finally, compares integer-level costs given by the Erlang-C formula with a continuous approximation, so both representations of the delay probability are in play at once.
The queue itself is not formalized: there is no Markov chain and no waiting-time distribution. Every statement is about the closed-form waiting cost with given by the Erlang-C formula, exactly as the paper's analysis is. Conventions, all in the namespace DimCallCenters.Constraint:
lam : ℝ is the arrival rate (λ is a Lean keyword); limits are Filter.atTop in lam, with μ fixed. Objects indexed by λ (, , ) are functions of lam constrained only for lam > 0.WaitModel packages μ > 0 and with , strict monotonicity on , and integrability of on for θ > 0 (the paper's finiteness of ; integrability is required because Lean's integral of a non-integrable function is 0).Nstar : ℝ → ℕ given with its two defining properties (feasible; below every feasible integer level above λ/μ). and are any positive solutions of their equations; existence and uniqueness are not hypotheses.∃ᶠ ("frequently"), as eventual boundedness.A trivializing formalization is ruled out: keeps all of the paper's terms and is never replaced by a smaller quantity, and the hypotheses are jointly satisfiable — with satisfies (33) for every with .
Infrastructure needed: the continuous Erlang-C function and its integer identity; the Halfin–Whitt limit (a Gaussian approximation of Poisson/gamma tails); calculus facts about the normal hazard rate. These are reusable beyond this mission, notably by the sibling missions on the cost-minimization problem. Example 8.5 (delay-probability target with ) motivates the rule but violates the strict monotonicity of , so it is not an instance of the theorem as stated. Contributions on any milestone, and on Theorem 8.9 (quality-driven regime, which needs Lemma 4.2), are welcome.
Impulse control models an agent who acts on a random system through discrete interventions, each with a fixed cost: inventory replenishment, cash management, exchange-rate interventions by a central bank. With two agents whose objectives conflict, the problem becomes a nonzero-sum stochastic differential game with impulse controls. Before the work of Aïd, Basei, Callegaro, Campi and Vargiolu (Math. Oper. Res. 45(1), 2020; preprint arXiv:1605.00039), such games had no general verification theorem and few explicit equilibria; the paper supplies both. Its main application, formalized in this mission, is a game between two central banks with different targets for an exchange rate, a two-player version of the exchange-rate control models of Bertola, Runggaldier and Yasuda and of Cadenillas and Zapatero (references [10], [12] of the paper). The paper proves that this game has an explicit one-parameter family of Nash equilibria of threshold type, with closed-form payoffs.
The state is a real process. Without interventions it is , where is a standard real Brownian motion and . Player 1 may shift it up by impulses , player 2 down by impulses :
Player 1 earns the running payoff , player 2 earns , with . An impulse costs its author and pays the opponent . Payoffs are discounted at rate . The standing assumptions are , , and .
A strategy of player is a pair : an open continuation region and a continuous impulse map . Player intervenes when the state leaves , applying the impulse ; player 1 has priority when both want to act. This rule defines the controlled process and the interventions inductively. Player 's payoff is
A pair is -admissible, , when these random variables are integrable, has all moments, and neither player's interventions accumulate in finite time. A Nash equilibrium is an admissible pair from which no player gains by deviating to any strategy that keeps the pair admissible.
The explicit objects are , and
From the zero of and a free parameter , the formulas (4.20)–(4.21) give thresholds , targets , coefficients , the functions and the piecewise candidates of (4.6). These are linear outside and equal inside.
For every and every initial state , the threshold strategies
form an -admissible Nash equilibrium, and
Milestones 1–3 are deterministic real analysis; milestone 4 and the goal are probabilistic.
The result gives explicit equilibria, with explicit thresholds and payoffs, for a nonzero-sum stochastic game with impulse controls. Such games rarely have closed-form solutions. The equilibria form a continuum indexed by : equilibrium payoffs are not unique, and every equilibrium in the family is a translate of a fixed interval policy. The explicit formulas also support the comparative statics of Section 4.4, where the continuation region widens as the fixed cost grows.
Proposition 4.7 is proved in the paper by applying its verification theorem (Theorem 3.3) to . The admissibility estimate (4.26) is written out only for initial states ; the general case is said to be similar. As far as is known, none of these results has a machine-checked proof. A formal proof would check every regularity, pasting and admissibility condition. It would also yield a reusable pathwise construction of impulse-controlled Brownian motion.
The deterministic milestones need careful algebra with nested logarithms and square roots. Proving Lemma 4.6 requires the global shape of , which needs the sign pattern of from Proposition 4.2, not only local conditions at the thresholds.
The goal is harder. The Nash inequality must hold against every admissible deviation: any open continuation region and any continuous impulse map, not only threshold strategies. Comparing payoffs therefore needs a verification argument, namely Itô's formula for a function that is only piecewise and across the thresholds, applied along a process with an unbounded number of jumps, plus a localisation that uses the moment condition (2.8). Admissibility needs a renewal-type bound on the discounted number of interventions, built from i.i.d. exit times of Brownian motion from an interval.
The Lean development lives in the namespace ImpulseGames.LinearGame.
Model with the proposition Model.Standing. The added hypothesis appears in every statement that uses : with , which the standing assumptions allow, has no zero in and the family (4.20) does not exist.IsBrownianReal W P on a probability space, with time in . Definition 2.2 is formalized pathwise: exit times in with , the tie rule favouring player 1, and for the tail of each impulse control. No SDE or stochastic integral appears in any statement; the uncontrolled dynamics are .Two slips of the page are corrected. First, the paper's impulse maps are not -valued on all of ; they are replaced by and , which agree with them wherever each player acts. Second, in Lemma 4.6 the maximiser (4.23) is not unique when , in the opponent's intervention region (all impulses tie there). The statement asserts maximality everywhere and uniqueness outside that region.
A complete development needs: elementary real analysis for milestones 1–3; a pathwise theory of piecewise-defined processes; an Itô formula for Brownian motion with , piecewise- functions; and exit-time estimates for Brownian motion. The last two are reusable well beyond this mission. Proofs of the deterministic milestones are welcome independently of the stochastic part.
Sequential decisions often change the distribution of future states. A planner choosing an action today must account for both its immediate reward and the later rewards made possible by the resulting state. The mathematical question is whether an optimal rule can be chosen once and reused at every stage, even when a competing plan may randomize and use the entire observed history. In Discounted Dynamic Programming, Blackwell studies this question on general Borel state and action spaces, beyond the finite models in which a direct comparison of actions is available.
The paper distinguishes several strengths of optimality. For each distribution of the initial state, an approximately optimal stationary plan exists, but a single plan that is approximately optimal at every initial state need not exist in a general Borel problem. Essential countability of the actions restores uniform approximate stationary optimality; essential finiteness yields exact stationary optimality. These are different mathematical claims, and the mission keeps their different quantifiers visible. Blackwell 1965, pp. 227, 229, 232–234.
A state is an element of a nonempty standard Borel space , and an action is an element of a nonempty standard Borel space . The transition kernel gives a probability distribution for the next state after action in state . The reward may depend on that next state ; it is bounded and Borel measurable. Future rewards are discounted by with . These are the objects of Blackwell’s Sections 2–3. Blackwell 1965, pp. 227–228.
A plan assigns a probability distribution of actions to each possible history before a decision. At stage , that history contains completed state-action pairs and the current state. Thus plans may randomize and depend on earlier states and actions. A Markov plan instead uses a Borel function at each stage; a stationary plan uses the same function at every stage and is denoted . Starting from state , the plan has discounted expected return
Here and are the state and action at stage . The comparison class for an optimal plan is all such plans, including randomized and history-dependent ones. Blackwell 1965, pp. 228–229.
Two actions are equivalent at state when they have the same reward for every next state and the same transition measure . An action set is essentially countable by a Markov plan if, for every , one of the actions is equivalent to at . It is essentially finite by that plan if has a countable Borel partition such that, for , one of is equivalent to every action at . A finite action set is a special case. Blackwell 1965, pp. 233–234.
For a probability distribution on and , -optimality asks for a stationary with
Theorem 6(b) asserts that such an always exists. Under essential countability, Theorem 7(a) obtains a stronger, uniform -optimality statement: for every there is a stationary with for all . Its other targets identify the optimal return with the fixed point of the operator and with the unique bounded solution of the optimality equation . Blackwell 1965, pp. 232–234.
The mission’s goal is Theorem 7(b). Under essential finiteness, it asks for a stationary with exact optimality:
The milestone list also includes the paper’s operator identity, approximate selection result, contraction criterion, generated-plan comparison, and upper-bound criterion. Each has its own source index and statement. Blackwell 1965, pp. 231–234.
The exact result says that, under a condition weaker than a globally finite action set, repeated use of one measurable state-based rule matches or exceeds the return of every adaptive randomized plan. It is a structural result about what information and randomization can add to discounted control. The preceding approximate results specify what can still be guaranteed when that condition is relaxed; Blackwell’s examples show that the distinctions cannot simply be ignored. Blackwell 1965, pp. 229–230, 234.
Blackwell proved these statements in 1965. The formalization work here is to give machine-checked proofs for the Borel-space model and its full comparison class, together with reusable definitions of history-dependent kernels, returns, stationary rules, and Bellman operators. The draft theorem statements compile as Lean declarations, but their proofs remain open. The milestone results are intended to make both the final theorem and its supporting measure-theoretic objects independently usable.
On an uncountable Borel action space, the pointwise supremum of available action values does not automatically come with a Borel action selector. Choosing a maximizing action separately at each state may fail to define a measurable rule, and a supremum need not be attained. Also, a Markov or stationary comparison cannot by itself certify optimality against plans that depend on full histories. These issues are real in the paper’s examples: general Borel problems may lack an -optimal plan, and a given plan need not be uniformly approximated by a Markov plan. Blackwell 1965, pp. 229–230.
The Lean model uses nonempty StandardBorelSpace types for and . “Baire function” is read as Borel measurable on these metrizable spaces. The problem stores a Markov transition kernel, a bounded measurable real reward on , and ; is included. A plan contains a probability kernel on each finite history, and the return is the actual absolutely convergent series of expected one-stage rewards. The first decision is indexed by in Lean, corresponding to the paper’s index . The finite history law is assembled through kernel composition products, and a stationary rule is represented by deterministic kernels. The integrals and series therefore express the paper’s expected return, including the cases where the reward depends on the next state.
For the operator results, means bounded and measurable real functions. The suprema defining and the optimal return are real suprema over nonempty families bounded by the reward and discount; they are used only in that setting. The abstract operator in Theorem 5 maps into itself. The action equivalence predicate uses the paper’s explicit equality of reward functions and transition laws; the later “i.e.” phrasing on p. 234 is weaker when interpreted as equality of operators alone. A partition piece may be empty, and Lean’s piece corresponds to the paper’s , with rules .
An optimality claim here always compares with every randomized history-dependent plan. Restricting that quantifier to Markov or stationary plans would trivialize the target. A complete development needs measure-theoretic facts about history laws and their bounded integrals, the discounted series, measurable partitions and selections, and the sup-norm contraction of bounded Borel functions. The history-law and bounded-function infrastructure can be reused outside this mission. Contributions to those foundations and to the numbered milestone theorems are welcome.
In network design games, selfish users build a shared network and split the cost of every edge among the users of that edge. Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 38 (2008), DOI 10.1137/070680096) studied the fair connection game, in which the cost of an edge is shared equally (the Shapley value) among its users. In this game the worst equilibrium can cost times the optimum, so the relevant measure is the price of stability: the ratio between the cheapest pure Nash equilibrium and the optimal centralized design. Their Theorem 2.1 bounds it by the harmonic number in every directed graph, and that bound is tight for directed graphs.
For undirected graphs the paper notes that is not tight and calls the correct bound "an interesting open problem". Its Section 4 settles the smallest case: two players with a common terminal. The general theorem gives there; Claim 4.1 improves this to , and a three-node example shows that is the right value.
Timeline. Rosenthal (1973) showed that congestion games have pure Nash equilibria through a potential function. Anshelevich et al. (FOCS 2004; journal version 2008) introduced the price of stability for the fair connection game, proved the bound and the two-player undirected bound treated here. Subsequent work studied the undirected multi-player case, which remains without a matching upper and lower bound in general.
Let be a finite undirected simple graph, with a cost on every edge . There are two players, a common terminal and personal terminals . A strategy of player is a set of edges that connects with : in the graph , and lie in the same connected component. A profile is a pair of strategies.
Under fair cost sharing each edge is paid for equally by the players using it. With the number of players whose strategy contains , player pays
A pure Nash equilibrium is a profile in which no player can lower its payment by switching to another strategy while the other player's strategy stays fixed. The total cost of a profile is the cost of the network it builds,
For a set of edges write . For a profile , the quantities , and split the total cost into the private and the shared parts.
The game is an instance of a congestion game, with per-user latency on edge ; the mission builds on the published congestion-game layer CongestionPoA.AsymSum.Model.
If the game has a profile, then some pure Nash equilibrium satisfies
Moreover, in the three-node example (nodes , edges of cost , edge of cost , with ) the cheapest pure Nash equilibrium costs exactly and the optimum costs exactly , so the ratio approaches .
The result shows that the price of stability of fair cost sharing depends on the network: the bound, tight for directed graphs, is not tight for undirected ones even with two players. It is the first undirected bound below and the starting point for the later study of undirected fair network design, where the question for many players is still open.
The theorem is proved in the paper; this mission formalizes it. A search of the Prove2Me library found no formalization of the price of stability of fair connection games. Beyond the theorem itself, the mission produces a reusable undirected layer over the congestion-game library: connectivity strategies stated with Mathlib's graph reachability, fair cost sharing as a congestion game, and the total-cost functional. A checked proof of the potential inequality (4.1) is the two-player case of the potential argument behind Theorem 2.1.
The obvious argument starts from an optimal solution, follows improving moves to an equilibrium and compares potentials. For two players this only yields the factor : the potential counts shared edges with weight , so a potential inequality alone cannot rule out an equilibrium in which both players share expensive edges. The improvement to needs a second inequality, (4.2), obtained from a specific deviation of each player in the equilibrium, and that deviation is valid only because of the undirected structure: the private parts of the two optimal paths together connect with , and the deviating player can then follow the other player's equilibrium route to . Making this connectivity claim precise for edge sets rather than drawn paths is where the formal work lies. It holds when the optimal strategies are inclusion-minimal, which is why the deviation milestones carry that hypothesis.
Fintype with decidable equality; edges are unordered pairs Sym2 V; the graph is a SimpleGraph V. Edge costs are a real function c with 0 ≤ c e for every e.i : Fin 2 (the paper's players 1 and 2 are 0 and 1) is a Finset of edges contained in G.edgeSet such that t i and s are Reachable in SimpleGraph.fromEdgeSet. Strategies are not restricted to paths.CongestionGame from CongestionPoA.AsymSum.Model with latency ; profiles, player costs and pure Nash equilibria are that library's IsProfile, cost and IsPureNash.Contributions welcome: a proof of the potential inequality (finite improvement paths in the two-player fair game), the graph-theoretic lemma that the symmetric difference of two simple paths with a common endpoint connects their other endpoints, and a computation of the three-node example.
A classifier built from a neural network produces a real score and predicts a binary label from its sign. A network can have many hidden units, so a guarantee based only on the number of parameters can be uninformative even when its output weights are small. Bartlett's 1998 paper asks whether a classifier's margin on training examples and the total magnitude of its weights can control its probability of error without fixing the number of units. Its Theorem 28 gives such a statement for two-layer networks whose activation is bounded and nondecreasing. The paper also discusses why this parameter-magnitude view supports weight decay and early stopping as learning heuristics, while leaving their algorithmic behavior outside the theorem's scope (Bartlett 1998, pp. 526, 534–535).
The theorem combines two results in the same paper. Theorem 2 turns the fat-shattering dimension of a real-valued function class into a margin generalization bound. Corollary 24 controls that dimension for finite combinations of affine-input units when the sum of the absolute combination weights is bounded. Lemmas 19, 22, and 23 supply covering estimates along that path. These are the milestones of this mission, with the source statements preserved in the milestone record (Bartlett 1998, pp. 527, 532–534).
An input is a vector , represented in Lean as Fin n → ℝ. A label is ; Lean's Bool is converted by pm, where true means . A probability distribution lives on labeled inputs. From an independent sample , the empirical margin error at scale is the fraction of indices with . The population error is the probability that , where . The inequality in the empirical error is strict, as in the paper's definition (Bartlett 1998, p. 526).
Fix a bounded nondecreasing activation . The first-layer class contains every , with an arbitrary weight vector and bias. The network class contains all finite sums with and . Thus bounds the output layer's total weight magnitude, while can vary without an imposed width limit. The bias is part of every unit. For a class , records the largest length of an input sequence whose every sign pattern can be realized with separation at least around one vector of thresholds (Bartlett 1998, pp. 526, 533–534).
For , , , and an independent sample of length , the goal is one universal such that, with probability at least , every satisfies
The paper prints in this display. That term vanishes at , although the class can then contain halfspace classifiers with nonzero sample complexity. The proof obtains a positive factor at that corner through Corollary 24 at scale , giving . The goal states this correction and records the printed statement separately in the moderation notes. The constant precedes all network, distribution, margin, confidence, and sample parameters in Lean; it cannot be selected after observing the instance (Bartlett 1998, pp. 533–534).
Corollary 24 bounds by a constant multiple of when the activation has range . Theorem 2 then converts a finite fat dimension at scale into a simultaneous bound on population error for all members of . The three covering lemmas track how shattering, pseudodimension, and an weight budget affect covers in sample , , and distances. Each bound retains the scale and explicit constants printed by the paper, subject to the stated corrections to undefined or false boundary cases (Bartlett 1998, pp. 527, 532–533).
The goal gives a width-independent generalization guarantee for a chosen network when its empirical margin error and total output weight are small. It applies to the entire class at once, so choosing a network after inspecting the sample does not turn the bound into a claim about only one fixed predictor. It does not assert that a learning algorithm finds such a network or that the displayed constants are optimal. Bartlett notes that later work had improved a logarithmic factor, and that empirical agreement with neural-network performance remained an open experimental question at the time (Bartlett 1998, pp. 534–535).
The paper proves the mathematical result. This mission asks for a machine-checked proof of its corrected formal statement and the stated supporting results; the draft theorem files currently contain proof obligations. A completed development would also make the fat dimension and strict external sample-cover definitions available for other margin analyses. Those objects differ from the platform's fixed-architecture neural networks and closed-ball covering numbers, so they are defined here with the conventions of this paper.
Counting hidden units gives no finite width-independent capacity bound, because permits arbitrarily many terms. Bounding each unit separately also does not control the full combination class: different small contributions can produce distinct values on a sample. The challenging step is relating covers of the base class to covers of all finite combinations under the total absolute-weight constraint, and then relating those covers back to fat-shattering. Even once a finite capacity estimate is available, the probability statement must hold simultaneously for every , including a network selected after sampling (Bartlett 1998, pp. 532–534).
Lean uses for fat dimensions and covering numbers, so an unbounded class cannot acquire a spurious dimension zero. Covers are external finite sets of real functions and use the strict distance of Definition 3. Sample and distances are normalized by . Pseudodimension is the supremum of positive-scale fat dimensions, matching the paper's right limit. Theorems assume , and sample indices are zero-based. The network class is generated from its weights rather than supplied as an arbitrary set satisfying the desired bound.
The paper says it ignores measurability issues and assumes all sets considered are measurable (Bartlett 1998, p. 526). The goal makes the event of a violating network measurable. Its individual network functions are measurable from monotonicity of and finite sums; the restated Theorem 2 has explicit hypotheses for measurable class members, the violating event, and the double-sample event in its proof. Theorem 2 additionally restricts to , where its printed logarithmic bound remains valid. Corollary 24 uses because a zero-dimensional input still permits a biased constant unit. Lemma 23 uses and in place of the printed : at or , or for , the printed strict inequality fails, while on the rest of the printed range it is kept. These are recorded as corrections rather than attributed to the printed wording.
The deeper-network part of Theorem 28 is outside this proposal. Its printed chain through Corollary 27 has an unresolved range issue when the input box bound is smaller than the activation range, and the displayed factor also vanishes at . This mission's goal is Part 1 and uses none of those claims. Contributions that establish the corrected covering lemmas, the capacity corollary, or the simultaneous margin bound fit the present proof frontier (Bartlett 1998, pp. 533–534).
Dynamic programming (DP) solves sequential decision problems by backward recursion: compute the optimal cost of the last stage, then of the last two stages, and so on. For problems with finitely many states and controls and real-valued costs, the recursion obviously gives the optimal cost. Applications are rarely like that. Control spaces are continuous, costs can be unbounded or infinite, the criterion can be multiplicative (risk-sensitive exponential cost) or worst-case (minimax), and the set of policies is an infinite product of function spaces. In this setting the DP recursion can fail to produce the optimal cost.
Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996), Part I, separates the order-theoretic content of DP from the measure theory. It works with an abstract monotone mapping that covers deterministic, stochastic, multiplicative-cost and minimax problems at once, following Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15 (1977). Chapter 3 answers the finite-horizon questions: when does the DP algorithm give the -stage optimal cost, and when do optimal or nearly optimal policies exist? This mission is the first of a series formalizing the book. Later chapters (contraction models, monotone increase and decrease models, the Borel models of Part II) are built on the model fixed here.
Let (states) and (controls) be sets, and for each let be a nonempty control constraint set. Write and let be the set of all functions , ordered pointwise. A mapping is given, subject to the Monotonicity Assumption: implies for all , .
A selector is a function with for all . A policy is a sequence of selectors. Define
and let be the -fold composition of . A terminal function with for all is fixed. The -stage cost of and the -stage optimal cost are
A policy is uniformly -stage optimal if each tail is -stage optimal, and -stage -optimal if where and where .
The three conditions on used in the chapter are F.1 (continuity of along nonincreasing sequences with ), F.2 (there is with for all ), and F.3 (a quantitative selection property with a constant ).
Under F.1, if for all and ; or under F.2, if for all and :
and under F.2, for every there is with .
The identity says that an infimum over an infinite-dimensional policy space equals nested one-dimensional infima. Every numerical use of finite-horizon DP depends on it, and so do the infinite-horizon results of later chapters, which pass to the limit in . Corollary 3.3.1 and Proposition 3.4 give the existence of optimal policies, and Propositions 3.6 and 3.7 verify the abstract hypotheses for two models outside standard expected additive cost.
These results are proved in the book; none of them is formalized. Mathlib has no abstract DP model, and the platform's finite-horizon results (Bertsekas, Dynamic Programming and Optimal Control, Prop. 1.3.1 and the minimax DP algorithm) assume finite disturbance and constraint sets and real costs. They are special cases, not this theory. The finite-horizon results of the 1977 paper (Lemma 3.1 here, on compact sublevel sets, and Corollary 3.1.1, the F.1′ case) are already posed on the platform and are not posed again.
The obvious argument interchanges the infimum over policies with the composition of operators: . The inequality follows from monotonicity alone. The reverse inequality is the content. Taking a near-minimizing selector at each stage requires either passing a limit inside (F.1) or bounding how errors at later stages propagate through (F.2, F.3). Both steps break at infinite values. With there may be no -optimal policy at all (Counterexample 4 of the book). Without F.1 or F.2 the identity itself fails (Counterexamples 1–3). A proof must therefore track separately the states where the optimal cost is , which is why F.3 and the definition of -optimality have two cases.
The model is a structure Model S C with fields U, U_nonempty, H : S → C → (S → EReal) → EReal and the monotonicity proof. Policies are ℕ → Selector, with selectors as a subtype of S → C. is m.T^[N], and is a recursion that applies first. All values lie in EReal. The book's convention never arises in Propositions 3.1–3.4, which only add real numbers to extended reals. The minimax and multiplicative mappings implement it explicitly (badd, and an expectation that returns when the positive part diverges). Every theorem assumes and . Assumptions F.1–F.3 are predicates on the model. F.2 is also available with a named constant (F2With) so that Propositions 3.6 and 3.7 can carry the book's constants and .
is defined as an infimum over policies of the composed operators, never through , so the goal is not true by definition. A formalization in which already contains an infimum over controls would make Proposition 3.1 hold by rfl, and this one rules that out.
Proving the goal needs elementary EReal order arithmetic, iterated infima over subtypes, and pointwise selection of near-minimizers via choice. Proposition 3.6 additionally needs monotone and dominated convergence for countable sums in ℝ≥0∞. The model and operator definitions are reusable by the later missions of the series (contraction, monotone increase and decrease models). Proofs of any milestone, and reusable EReal lemmas about shifting by real constants, are welcome.
How many agents should a call center staff? Telephone call centers employ millions of people, and staffing is their largest cost, so the question is asked every half hour of every day (Gans, Koole & Mandelbaum, 2003). The classical model is the M/M/N (Erlang-C) queue: calls arrive at rate , service times are exponential with mean , and agents serve in parallel. Practitioners use the square-root safety staffing rule , which Halfin and Whitt (1981) justified in the regime where the probability of waiting stays bounded away from and .
Borst, Mandelbaum and Reiman (CWI Report PNA-R0015, 2000; published as Operations Research 52(1), 2004) asked when such a rule is actually optimal: given a staffing cost and a waiting cost, which staffing level minimizes total cost as the arrival rate grows? They identified three regimes according to how the two costs compare. This mission formalizes their third case, the quality-driven regime, in which waiting is so expensive relative to staffing that the optimal number of agents exceeds the offered load by more than any fixed multiple of its square root.
Fix a service rate . For every arrival rate a waiting-cost function assigns cost to a wait of time units; it satisfies , is strictly increasing, and is integrable on for every . A staffing cost , defined for real , is convex and strictly increasing.
For an integer the probability of waiting is the Erlang-C formula
the expected waiting cost of a delayed customer is , and the total cost per unit time is . An optimal staffing level minimizes over the integers .
Write , and for put , , and , where extends the Erlang-C formula to real . The normalized cost is , and a surrogate cost is . Rounding is measured by .
Two special functions appear. The Halfin–Whitt delay function is with the standard normal hazard rate. The Stirling-type approximation is
Asymptotic relations are limits of ratios as : means , and means .
Assume the regime is quality-driven, display (27): for every . Let minimize over . Then
The statement fixes no constants and no rate; it asserts only that rounding the surrogate optimum loses a vanishing fraction of the excess cost.
In attack order: Lemma C.1 ( strictly convex decreasing); the identity at integer (Section 3, p. 12); Lemma 3.1 and Lemma 3.2; Corollary 3.3 (the asymptotic optimality criterion); Lemma B.1 ( strictly convex decreasing); display (15); Lemma 4.1 (Halfin and Whitt); and the first statement of Lemma 4.2, whenever .
Theorem 7.1 completes the paper's picture of optimal staffing. In the rationalized regime the square-root rule with the Halfin–Whitt function is optimal; in the efficiency-driven regime staffing barely exceeds the load; in the quality-driven regime the staffing excess outgrows and must be replaced by the Stirling-type expression . The theorem gives a one-dimensional minimization whose solution is asymptotically optimal, which turns a discrete optimization over into a smooth problem, and it marks the boundary of validity of square-root staffing.
The result is proved in the paper; it is not formalized anywhere to our knowledge. A complete development formalizes the Section 3 framework (shared with the other regimes of the same paper), the convexity of and of , the Halfin–Whitt limit for the continuous extension , and the Stirling-type asymptotics of the Erlang-C formula. Each of these is a reusable piece of queueing theory in Lean.
The regime theorem itself is short once the framework is in place; the weight lies in the analytic lemmas. Lemma 4.2 requires uniform asymptotics of at a staffing excess that may grow at any rate, from barely faster than a constant to faster than , where neither the central-limit picture of Halfin and Whitt nor a single Stirling expansion covers all cases. Lemma 4.1 concerns the continuous extension at non-integer server counts, whereas Halfin and Whitt's theorem is about integer ones. The natural first idea, that the goal follows from Corollary 3.3 by plugging in Lemma 4.2, does not apply directly: Lemma 4.2 only covers staffing excesses that tend to infinity, and nothing in the definition of the true optimum or the surrogate optimum says that they do.
Lean represents as a positive real, and is the filter atTop on with fixed. The standing assumptions on and are the structure WaitModel; is a function argument with hypotheses ConvexOn and StrictMonoOn on . Staffing levels are natural numbers. Minimizers (, , , ) are function arguments with minimality hypotheses at every , so every statement holds for every choice among ties. Liminf and limsup relations are stated through Filter.Frequently, avoiding boundedness side conditions.
The queue itself (Poisson arrivals, waiting-time law) is not formalized: the paper's analysis and all its theorems concern the closed-form cost with the Erlang-C formula.
Conventions committed to: (i) the goal adds the hypothesis as , which the paper asserts on p. 12 to show the continuous optimum exists but which does not follow from its standing assumptions (it holds exactly when is unbounded); (ii) in the floor term is omitted when , since the cost is undefined at unstable levels; (iii) the integrability of is explicit, because a Lean integral of a non-integrable function is ; (iv) , the value of formula (11) at ; (v) display (15) is stated for , since the ratio is undefined at . The instance , , (Section 9) satisfies every hypothesis of the goal, so the goal is not vacuous; taking or at Lean default values is ruled out by these explicit domain conditions.
Only the first statement of Lemma 4.2 is a milestone: the second, under , fails as printed at . Contributions on the Erlang-C asymptotics, the normal hazard rate, and Laplace transforms of increasing functions are welcome and reusable beyond this mission.
Many large convex programs have the form "minimize a strictly convex function subject to linear equations ". Examples are entropy maximization under moment constraints, the estimation of a matrix with prescribed row and column sums (the matrix-scaling or RAS problem of transportation and input–output analysis), and least-norm solutions of linear systems. When is large and sparse, methods that touch one equation at a time are attractive: each step needs only one row of .
L. M. Bregman's 1967 paper (doi:10.1016/0041-5553(67)90040-7) introduced such a method. §1 defines a "relaxation" for finding a common point of closed convex sets , in which each step replaces the current point by its -projection onto one set: the minimizer of a distance-like function over that set. §2 chooses from the objective itself, with the gradient of ; this function is now called the Bregman divergence. Theorem 3 of the paper, the target of this mission, shows that with this choice the relaxation does more than find a feasible point: started at a suitable point, its limit minimizes over the feasible set. The resulting row-action methods underlie later work on entropy optimization and matrix balancing (Censor and Zenios, Parallel Optimization, 1997) and the Bregman-projection techniques of modern optimization.
Work in the Euclidean space with inner product . Let be a convex set with closure and interior . Let be strictly convex and continuously differentiable over , with gradient at , and continuous over . Let be an matrix with nonzero rows and . The problem (2.1)–(2.3) is
with feasible set , assumed nonempty. A point of minimizing over is a solution.
The function (1.4) is
and also denotes the hyperplane . The paper assumes that satisfies its conditions I–VI of §1 with respect to these hyperplanes; among them, condition II provides, for every , a -projection minimizing over . It also assumes condition (2): if and , then .
A relaxation sequence with control starts at and sets . The control is any sequence of row indices. Finally,
is the set of points of at which the gradient lies in the row space of .
Assume that the -projection of every point of onto every lies in . For every control and every relaxation sequence with that converges to a point ,
Convergence of the sequence is a hypothesis; the theorem says what the limit is, whichever control produced it.
An additional item states Note 2: the point and the multiplier in (2.7)–(2.8) are unique.
Theorem 3 converts a feasibility algorithm into an optimization algorithm for equality-constrained convex programs. Each step solves a one-dimensional problem (the multiplier of a single equation), so the method scales to systems with very many equations, and with the controls of Theorems 1–2 of the same paper it gives a complete algorithm. Specializations include iterative proportional fitting for entropy objectives and Kaczmarz-type projections for .
The theorem and its proof are classical and have been reproved many times, but no machine-checked proof is known to exist. A formalization produces a verified bridge between three standard pieces of convex analysis: first-order optimality on an affine set, the supporting-hyperplane inequality for a differentiable convex function extended to the closure of its domain, and the passage of a Lagrange condition to a limit. Each is reusable in other row-action and mirror-descent developments.
The obvious argument says: the limit is feasible, and the gradient at every iterate lies in the row space of , so the limit satisfies the Karush–Kuhn–Tucker conditions. Two steps of this argument fail as stated. First, the gradient is only known on , the limit may lie on the boundary of (or outside , in ), and need not extend continuously there, so the multipliers need not converge and no Lagrange condition holds at the limit. Lemma 3 must therefore reach optimality without a gradient at . Second, the Lagrange condition (2.7) at an iterate requires the projection to be an interior minimizer, which is why the theorem carries the hypothesis that preserves ; on the boundary of a minimizer over need not satisfy (2.7).
The space is EuclideanSpace ℝ (Fin p), rows are vectors a i, and is the real inner product. The gradient is explicit data tied to by HasGradientWithinAt f (g x) S x for and continuous on ; is not assumed open, and Mathlib's gradient is not used. The relevant explicit choices are:
lam.The goal does not conclude that the relaxation converges; a statement asserting convergence is a different, unproved theorem. Equally, it must not be weakened to a fixed control, to an open , or to a limit assumed to lie in : any of these would trivialize the passage to the limit that the theorem is about.
A complete development needs the first-order condition for a local minimum on an affine hyperplane, the gradient inequality for , , and an induction along the relaxation sequence. Proofs of the milestones and of Note 2 are welcome independently.
A reproducing kernel Hilbert space is a Hilbert space of functions on a set in which every point evaluation is continuous; the function that represents evaluation at is its reproducing kernel. N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404, DOI 10.1090/S0002-9947-1950-0051437-7) gave the general theory of these spaces, which today underlies kernel methods in statistics and machine learning, Gaussian-process regression, and the Bergman and Szegő kernels of complex analysis.
Part I of the paper studies how kernels behave under the basic operations on classes of functions: sums, inclusions, products, restrictions, and limits. §9 treats limits. Its case A concerns a decreasing sequence of classes with increasing norms, defined on an increasing sequence of sets. The application in the paper's Part II is the computation of kernels of a domain by approximation from simpler domains: when a domain is exhausted by an increasing sequence of subdomains, the kernels of the subdomains converge to the kernel of the whole domain. This mission formalizes §9, Theorem I and the steps of its proof.
Let be an arbitrary set and subsets with union . For each let be a complex Hilbert space of functions on , with norm , in which point evaluations are continuous; , for , is its reproducing kernel, characterized by and
with the scalar product linear in . For and , denotes the restriction of to . The standing assumptions of §9 A (p. 362) are:
together with the existence of every kernel . For two kernels on a set , means that is a positive matrix: for all finite families , . is the restriction of to .
The limit class is the set of functions on such that (1°) every restriction belongs to and (2°) .
Under the standing assumptions there is such that, whenever ,
and is the reproducing kernel of with the norm
The result. Theorem I turns a monotone family of function spaces into a single space and identifies its kernel as the pointwise limit of the kernels. It reduces the computation of a kernel on a large set to kernels on an exhausting sequence of subsets, the method Aronszajn uses in Part II for Bergman-type kernels of plane domains. With for all (explicitly allowed on p. 362) it gives the limit of a decreasing sequence of kernels on one set as the kernel of the intersection class with the limit norm. The milestones (4)–(6) are quantitative: (5) bounds the distance between restricted kernel sections by the decrease of the diagonal values, which yields strong convergence of in every .
Formalizing it. The theorem is classical and proved in the paper; to our knowledge no machine-checked proof exists. Mathlib has the RKHS class, the operator-valued kernel, the positive semidefiniteness of kernels and the Moore–Aronszajn construction RKHS.OfKernel, but nothing about restrictions of an RKHS to a subset, the order between kernels, or limits of sequences of reproducing kernel spaces. This mission produces those statements on Mathlib's RKHS vocabulary over , with kernels on varying domains.
The kernels live on different sets , so convergence is not convergence of a sequence of functions on one set: a pair enters the sequence only from the first containing both. The identification of the limit class needs three separate facts: that with the limit norm is a Hilbert space (the limit of norms must be shown to come from a scalar product, and completeness requires passing to the limit in two indices), that , and that reproduces. The natural first idea, to embed all in one space and take an intersection, fails: the are spaces of functions on different sets, and their norms differ, so there is no common ambient Hilbert space; the comparison goes only through restriction and the inequalities (3). Eq. (4) itself uses §7, Theorem II (a contractively included Hilbert subclass has a dominated kernel) and the restriction theorem of §5, neither of which is in Mathlib.
H n with [InnerProductSpace ℂ (H n)] [CompleteSpace (H n)] [RKHS ℂ (H n) (E n) ℂ], a space of functions on the subtype E n; the set is a type X with no topology, measure or nonemptiness assumption.kernelFn H x y is Mathlib's RKHS.kernel H x y 1. Mathlib's inner product is conjugate-linear in the first slot, so Aronszajn's is ⟪g, f⟫_ℂ.IsDecreasingRKSequence; every statement takes it as a hypothesis. Restriction is pointwise agreement on . Indexing starts at .KernelLE K₁ K := (Matrix.of K - Matrix.of K₁).PosSemidef, with Mathlib's positive semidefiniteness over an arbitrary index type (finitely supported vectors).ComplexOrder, which also asserts that these values are real.Tendsto).RKHS.OfKernel K₀ and then asserts that its kernel is would be a tautology (RKHS.kernel_ofKernel); the goal instead characterizes the space by its functions and norm, as the paper does.Needed infrastructure, reusable beyond this mission: restriction of an RKHS to a subset (§5), the dominated-kernel theorem for contractive inclusions (§7, Theorem II), and the passage from a convergent sequence of norms to a convergent sequence of scalar products. Proofs of any milestone, and of these general facts as separate lemmas, are welcome.
Mathlib/Analysis/InnerProductSpace/Reproducing.lean (the RKHS class, RKHS.kernel, RKHS.OfKernel). https://github.com/leanprover-community/mathlib4A call center must choose enough servers to limit waiting while paying for every server it staffs. When arrivals are heavy, small changes in the number of servers can change the probability of delay substantially. Borst, Mandelbaum, and Reiman study how to make this choice when the arrival rate grows and the costs of staffing and waiting need not grow at the same rate. Their CWI report treats several regimes within one queueing model. This mission concerns the efficiency-driven regime, where the incremental staffing cost eventually dominates the conditional waiting cost at every fixed positive square-root staffing offset. The resulting rule chooses an offset by optimizing a simpler cost that treats the probability of waiting as one.
The result is useful when the staffing-cost and waiting-cost primitives change with system scale. It says that the simplified choice still attains the optimal total cost asymptotically, even though the actual staffing decision is an integer and the simplified problem uses a real variable. The report states this as Theorem 6.1 on printed page 19, with its interpretation of asymptotic optimality supplied by Corollary 3.3 on printed page 14.
Customers arrive at rate and receive exponential service at rate per server. The service rate is fixed as grows. For an integer number of servers , the Erlang-C delay probability is the explicit finite-sum expression in Section 2 of the report. A customer who waits has an exponential waiting time with rate . Let be the cost of a wait of length . It is strictly increasing on , satisfies , and has finite exponential expectation at every positive rate. The resulting conditional waiting cost is
The staffing cost is one fixed, convex, strictly increasing function of the server count. Its continuous extension is evaluated at real . Total cost per unit of time at a stable integer level is
Write for any minimizing stable integer level. Ties are permitted. For a positive real offset , define , , and . The report extends Erlang-C continuously to and writes the incremental continuous objective as . These definitions and the integer-extension identity are from Section 3, printed pages 11–12.
The report defines the efficiency-driven regime by
For each , choose to minimize over . Let be the smaller cost of the stable integer levels immediately below and above ; if the lower one is unstable, use the upper one. The goal, Theorem 6.1 together with Corollary 3.3, is
The milestone path includes the convexity of the conditional waiting cost (Lemma C.1), the agreement of the continuous Erlang-C extension with its integer formula, the two approximation lemmas and their corollary (Lemmas 3.1–3.2 and Corollary 3.3), the convex staffing-cost comparison of equation (13), and all three clauses of the Halfin–Whitt limit in Lemma 4.1. This ordering follows the objects each later statement uses.
The theorem certifies a staffing rule defined by a one-variable surrogate rather than the exact Erlang-C probability in the objective. Its guarantee concerns the incremental total cost above the unavoidable baseline , which is the economically relevant quantity when comparing two near-minimal stable staffing levels. The ratio tends to one, so the theorem is stronger than a claim that the two costs merely have the same growth order. The source also presents other regimes with different surrogates; their conclusions are separate targets in this series.
The paper proves the mathematical theorem. This mission asks for a Lean proof of its closed-form model and the surrounding lemmas. The complete development would make the report's approximation framework reusable for later results that combine a continuous queueing approximation, a surrogate minimizer, and integer rounding. It would also expose the exact assumptions needed to pass between real and integer staffing levels. No machine-checked proof of this report's Theorem 6.1 is claimed here.
The simple objective replaces the delay probability by one. That replacement is accurate near zero offset, but the minimizing offset itself changes with . Pointwise asymptotics at a fixed positive offset do not directly control the value of an objective at its moving minimizer. The proof therefore has to relate the regime assumption to the location of the relevant minimizers before using the Halfin–Whitt limit. Integer rounding introduces another boundary issue: when is just above , its floor need not be stable, so evaluating the ordinary Erlang-C formula there would compare the target against a meaningless cost. These difficulties are visible already in the statements of Theorem 6.1 and Lemma 3.2.
Lean represents , , offsets, and costs as real numbers; arrival-rate limits use the real filter at . Staffing counts are natural numbers. The service rate is positive and fixed. A WaitModel packages strict increase and normalization of on nonnegative waits together with integrability against every positive exponential rate. This integrability expresses the report's finiteness assumption for and prevents a nonintegrable real integral from silently evaluating to zero. The hypotheses on are convexity and strict increase on positive real staffing levels; does not depend on .
The report asserts that diverges as decreases to , although the stated assumptions permit bounded increasing waiting penalties for which that assertion fails. The goal therefore includes this explicit divergence hypothesis, which also supports existence of the continuous minimizer used in the report's argument. The integer optimum and the surrogate optimum are functions constrained to be minimizers at every positive arrival rate. They cannot be arbitrary choices that make the conclusion vacuous. The continuous optimum appears only in the framework milestones; it is not a hypothesis of Theorem 6.1.
All formulas are total Lean functions. Their values at , unstable integer counts, nonpositive offsets, or invalid parameters to the continuous Erlang-C integral have no queueing interpretation. Every theorem using them constrains its relevant inputs. The definition of ignores an unstable floor and uses the stable ceiling. At a positive offset and arrival rate this ceiling is above offered load. The Gaussian density, its cumulative integral, the hazard rate, and the delay function use the explicit formulas of Section 4; the value of the delay function at zero is the continuous extension needed by Lemma 4.1.
The queue's stochastic construction is outside this mission. The formal objects are the report's cost formulas and asymptotic comparisons, not a continuous-time Markov chain. Useful contributions include proofs of the special-function limit, convexity of conditional waiting cost, the integer-extension identity, and the reusable approximation lemmas. The regime condition is the full limit in equation (23); weakening it to an unrelated boundedness condition would change the theorem.
Reproducing kernel Hilbert spaces are the function spaces of kernel methods in statistics and machine learning (Gaussian-process regression, support vector machines, kernel mean embeddings), of the Bergman and Szegő spaces of complex analysis, and of the theory of positive-definite functions. In all of these, bounded operators on the space (covariance operators, integral operators, projections onto subspaces, multiplication operators) are handled through functions of two points rather than through abstract operators. N. Aronszajn's Theory of Reproducing Kernels (Trans. Amer. Math. Soc. 68 (1950), 337–404) gives, in its §11, the dictionary between bounded operators on a space with a reproducing kernel and their kernels, and characterizes the kernels of bounded symmetric operators with prescribed bounds. Aronszajn credits the ideas of the section to E. H. Moore.
Let be an arbitrary set and let be a class of complex-valued functions on that forms a complex Hilbert space with scalar product , linear in and conjugate-linear in . A reproducing kernel of is a function such that, for every , the function belongs to and
Such a kernel exists exactly when every point evaluation is continuous.
For a bounded linear operator on , with adjoint defined by , the kernel of is
the value at of the element of . By the reproducing property, for every and , so is determined by .
A function is a positive matrix if for every finite family of points and complex numbers . For two arbitrary functions on , one writes if is a positive matrix. A bounded operator is symmetric if , and positive if for every . A symmetric has lower bound and upper bound if
A kernel is hermitian symmetric if .
For an arbitrary hermitian symmetric function and real numbers :
The function is not assumed to have ; that membership is part of what the condition yields.
Theorem I identifies, by finite quadratic-form inequalities alone, which functions of two points are kernels of bounded symmetric operators and with which spectral bounds. It reduces statements about operators (boundedness, positivity, operator inequalities ) to statements about finitely many evaluations of kernels, the form in which they are checked in practice, for instance when a covariance or integral operator is shown to be bounded and positive from its kernel. The milestones make the correspondence a usable calculus: adjoints become conjugate transposes, composition becomes a scalar product in the middle variable, and limits of operators become limits of kernels.
All of these results are proved in the paper. None is formalized: Mathlib has reproducing kernel Hilbert spaces (RKHS), adjoints, positive operators and positive semidefinite matrices over arbitrary index types, but no kernel of an operator and none of the statements above. The mission produces machine-checked proofs of the §11 dictionary and of Theorem I.
The necessity half of Theorem I and milestones (3), (6), (4) follow from the reproducing property. The sufficiency half is where the work is: is an arbitrary function, and the hypothesis is only about finite families of points. One has to produce an operator on all of . The obvious attempt, defining on the dense span of the functions by the kernel and extending by continuity, needs the bound on that span, which does not follow directly from the two one-sided inequalities on the diagonal forms. The positivity of and does not by itself give the membership , which the definition of the kernel of an operator requires. In milestone (7), positivity of an operator is a statement about all of , while positivity of the kernel only sees finite combinations of kernel functions; the passage between them uses density of these combinations.
RKHS ℂ H X ℂ: a complex Hilbert space H whose elements are functions X → ℂ on an arbitrary type X (no topology, no measure, not assumed nonempty), with continuous evaluations. The scalar kernel is the series' shared definition AronszajnRK.Sum.kernelFn H x y := RKHS.kernel H x y 1; the function is the element RKHS.kerFun H y 1.L : H →L[ℂ] H is opKernel L x y := (adjoint L) (kerFun H y 1) x. Mathlib's ⟪u, v⟫_ℂ is conjugate-linear in u, so the paper's is ⟪g, f⟫_ℂ, and every formula with a scalar product or a bar has been rewritten in that order. On a one-point with , and , the kernel is .Matrix.PosSemidef of Matrix.of Λ over the index type X (finitely supported test vectors, ComplexOrder on ℂ); no finiteness of X is assumed.IsSelfAdjoint L. "Positive" in (7) is ∀ f, 0 ≤ ⟪f, L f⟫_ℂ in ComplexOrder (real and nonnegative), without assuming self-adjointness, as in the paper. The bounds in Theorem I are bounds of the quadratic form, m‖f‖² ≤ Re⟪f, L f⟫ ≤ M‖f‖², not of the operator norm. The paper does not assume and neither does the statement: for both sides hold exactly when and .H, and that the kernel of L₁ ∘L L₂ is their scalar product.⟪v, Lₙ u⟫ → ⟪v, L u⟫ for all u, v; uniform convergence is ‖Lₙ − L‖ → 0 in operator norm.HilbertBasis with arbitrary index types, and the double limit is taken along growing finite sets of indices in both variables. For systems indexed by this contains the paper's over ; the general form also covers finite-dimensional spaces. The second sentence of Theorem III (kernels in correspond to operators of finite norm) needs the direct product and is not stated.RKHS, RKHS.kerFun_inner, RKHS.kerFun_dense, RKHS.posSemidef_kernel, ContinuousLinearMap.adjoint, ContinuousLinearMap.IsPositive and isPositive_iff_complex, HilbertBasis, Matrix.PosSemidef. Contributions welcome: a general lemma that a function with is the kernel of an operator , and the inclusion theorem , both reusable beyond this mission.A stochastic approximation algorithm is a recursion
in , where is a vector field, are small step sizes and is noise. Such recursions go back to Robbins and Monro's root-finding scheme (Robbins–Monro 1951) and underlie stochastic gradient descent, temporal-difference learning, adaptive control and learning in games. The ODE method studies them by comparing the iterates with the trajectories of .
Benaïm's lecture notes (Benaïm 1999) organize the ODE method in two steps. A deterministic step, Proposition 4.1, shows that whenever the noise satisfies a condition called A1 (together with a boundedness condition on the iterates), the interpolated process is an asymptotic pseudotrajectory of the flow of . A probabilistic step then verifies A1 for concrete noise models. Proposition 4.2 does this for martingale difference noise with bounded -th moments, at the price of step sizes with . This mission formalizes the second verification, Proposition 4.4: when the noise is subgaussian, A1 holds almost surely under the much weaker requirement that for every , which allows step sizes decaying only slightly faster than . The notes attribute the result to Duflo (1997), see also Kushner and Yin (1997) and Benaïm and Hirsch (1996).
Let be a deterministic sequence with , and (a step sequence). Put , , and let
be the index of the step that contains time . For a sequence define the piecewise constant processes and , so that step occupies the time interval of length .
Assumption A1 asks that for every
or, in the form the notes call equivalent, for every , where
Let be a probability space with a nondecreasing sequence of sub--algebras, and continuous. A sequence given by the recursion above is a Robbins–Monro algorithm if is deterministic, is -measurable, and . The noise is subgaussian if there is a number such that for all and all
Bounded noise, , is an example.
For a Robbins–Monro algorithm with subgaussian noise and a deterministic step sequence such that
with probability one the realised noise sequence satisfies A1, in both of its forms, simultaneously for all .
is a supermartingale. 2. Directional maximal tail bound. For every unit vector , , and ,
Proposition 4.4 is the sufficient condition for the ODE method when the noise has Gaussian-type tails. Its step-size condition holds whenever , so it admits steps that decrease far more slowly than the of the classical theory; slowly decreasing steps are what practitioners use to keep algorithms responsive. Combined with Proposition 4.1 it shows that the interpolated process of such an algorithm, with bounded iterates, is almost surely an asymptotic pseudotrajectory of the flow of , and the limit set theorems of the notes then locate the limit points of the algorithm.
The result is proved in the notes and in the cited literature; it has not, to our knowledge, been machine-checked. A formal proof would add reusable pieces: an exponential supermartingale and maximal inequality for vector-valued martingale differences with a conditional subgaussian bound (Mathlib's conditional subgaussian notion is scalar), a Borel–Cantelli argument along the grid , and the continuous-time bookkeeping of , and shared with the other missions of this series.
The moment method of Proposition 4.2 does not reach this regime: any fixed polynomial moment of the window sums decays only polynomially in the window's step sizes, and under alone polynomial bounds are not summable over windows. Exponential tail bounds are needed, and they must be maximal (uniform over the window) and must hold for the norm of a vector, not only for a scalar. The continuous-time deviation involves partial steps at both ends of , so the bound must be stated in terms of rather than a sum over whole steps, with constants that do not depend on , or . Finally, A1 quantifies over all : the almost-sure statement must hold on a single event of full probability for every .
The space is as EuclideanSpace ℝ (Fin d) (the paper writes ); time is real. The sequences and are indexed by , and their values at are unused, as the paper indexes them from . The filtration is a Mathlib Filtration ℕ; is -strongly measurable and integrable, and almost surely. The subgaussian condition requires to be integrable for every and . The summand is taken to be when , its limiting value. The suprema in A1 and are taken in ; the supremum over an empty range of is . In Eq. (18) the constants are chosen before the probability space, the algorithm and .
The following readings are excluded and are not acceptable formalizations: a subgaussian condition that holds vacuously because the exponential is not integrable (Lean's conditional expectation of a non-integrable function is ); a summability condition made trivial or false by the convention ; and the conclusion "for each , A1 holds almost surely" in place of "almost surely, A1 holds for all ". The second sentence of Proposition 4.4 (the asymptotic pseudotrajectory conclusion) is outside this mission.
All hypotheses are satisfiable: , , , and satisfy every one of them.
Contributions welcome: a maximal inequality for nonnegative supermartingales in the form needed here, vector subgaussian tail bounds for martingale transforms with deterministic weights (reusable well beyond this mission), lemmas on the step processes and (measurability, local integrability, additivity), and the proofs of the milestones.
Dynamic programming over uncountable state and control spaces needs two things at every stage: the optimal cost-to-go, obtained by minimizing over the control, must be a function that can be integrated against the next stage's transition probabilities, and a policy that nearly attains the minimum must be measurable, so that it defines a stochastic process. With Borel-measurable costs and Borel-measurable policies both requirements fail. Minimizing a Borel function of over produces a function whose level sets are projections of Borel sets, and such projections need not be Borel (Suslin, 1917). The repair, developed by Blackwell, Freedman and Orkin (1974), Shreve and Bertsekas, and set out in Chapter 7 of Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978), is to enlarge the class of costs to the lower semianalytic functions and the class of policies to the analytically or universally measurable ones. Sections 7.6–7.7 of the book establish that this class is closed under partial minimization and admits measurable ε-optimal selectors. Chapters 8–10 of the book, and much of the later literature on Borel-space Markov decision processes (Hernández-Lerma and Lasserre; Feinberg and coauthors), build on these results.
Timeline:
A Borel space is a topological space homeomorphic to a Borel subset of a complete separable metric space (Definition 7.7); its Borel σ-algebra is . The Baire space is with the product topology. A set is analytic if it is empty or the image of under a continuous map; by Proposition 7.41 this is the book's Definition 7.16 (the Suslin operation applied to closed sets). Every Borel set is analytic, and the converse fails when is uncountable.
Three σ-algebras on are in play. The analytic σ-algebra is generated by the analytic sets (Definition 7.19). The universal σ-algebra is , the intersection over all probability measures on of the -completions of (Definition 7.18). For a function from into a Borel space , is analytically measurable if and for every , and universally measurable if the same holds with (Definition 7.20).
Let . A function is lower semianalytic if is analytic and is analytic for every real (Definition 7.21). For write , , and define the partial infimum
A selector is a function whose graph lies in .
Let be Borel spaces, analytic, and lower semianalytic.
(a) For every there is an analytically measurable selector with
(b) The set of points where the infimum is attained is universally measurable, and for every there is a universally measurable selector with on and the bounds of (a) off .
The goal fixes no constant beyond the book's and .
In attack order: Proposition 7.40 (Borel images and preimages of analytic sets are analytic), Corollary 7.42.1 (), Corollary 7.44.2 (composites of analytically measurable maps are universally measurable), and Proposition 7.49, the Jankov–von Neumann theorem:
Further items of the mission, on the same definitions: Proposition 7.39 (projections of analytic sets are analytic, and every analytic set is a projection of a Borel set), Lemma 7.30(1) (strict and non-strict, real and extended level sets give the same class) and Proposition 7.47 (lower semianalytic functions are exactly partial infima of Borel functions).
Proposition 7.50 is the selection theorem behind the existence of ε-optimal policies in Borel-space dynamic programming. In the finite-horizon model of Chapter 8 the optimal cost-to-go at each stage is lower semianalytic, by Propositions 7.47 and 7.48. Proposition 7.50 then turns the one-stage minimization into a measurable policy, analytically measurable when only ε-optimality is required and universally measurable when the minimum is attained. Chapters 8–9 of the book (the finite-horizon recursion and the optimality equation under (P), (N), (D)) use it at every step. Downstream catalog papers on average-cost and stochastic shortest-path problems over Borel spaces cite these results.
All results here are proved in the book and in the descriptive set theory literature (Kechris, Classical Descriptive Set Theory, §18 and §29). None is formalized on Prove2Me. Mathlib has analytic sets in Polish-type settings, the Lusin separation theorem and Suslin's theorem, but it has no universal σ-algebra, no analytic σ-algebra, no lower semianalytic functions and no Jankov–von Neumann uniformization. The definitions in this mission are reusable by the later missions of the series (Chapters 8–10), which restate them locally until these are published.
The obvious route to a selector is to choose, for each , a minimizing or near-minimizing . The axiom of choice provides such a function, but nothing makes it measurable, and the conclusion of the theorem is exactly that measurability. The Borel route fails too: the set is a projection of a Borel set, which is analytic but in general not Borel, so no Borel-measurable selector exists in general. The Jankov–von Neumann theorem needs a lexicographically least branch of a continuous parametrization of by , and an argument that the resulting map is measurable with respect to , which is generated by sets that are not closed under complementation. Part (b) adds a further obstacle: the composite of two analytically measurable maps need not be analytically measurable, so the exact selector is only universally measurable. Proving that requires Lusin's theorem that analytic sets are measurable for every completed probability measure.
IsBorelSpace (Definition 7.7, the ambient complete separable metric space taken in the same universe), together with Mathlib's [MeasurableSpace X] [BorelSpace X], so measurable sets are exactly the Borel sets. On the product σ-algebra is used; it coincides with for separable metrizable spaces (Proposition 7.13).MeasureTheory.AnalyticSet (empty or a continuous image of ℕ → ℕ).EReal. The book uses , and Mathlib's EReal uses . No statement of this mission adds infinities of opposite sign; adds a real number.NullMeasurableSet E p for every probability measure p.Not included: Lusin's theorem in Suslin-scheme form (Proposition 7.42, which needs the Suslin operation as a definition), Proposition 7.43 on , the integration results of Propositions 7.46 and 7.48, and Lemma 7.30(2)–(4). None is used in the proof of the goal. Contributions welcome: the bridge between IsBorelSpace and Mathlib's StandardBorelSpace, the universal σ-algebra API, and the Jankov–von Neumann theorem itself.
In a network design game each player must connect its terminals in a graph whose edges carry fixed costs, and the cost of an edge is split among the players that use it. Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 38 (2008)) studied the fair (Shapley) split, in which the users of an edge pay equal shares. That game is a congestion game in the sense of Rosenthal (Int. J. Game Theory 2 (1973)), so it has an exact potential and pure Nash equilibria always exist.
Section 6 of the same paper turns to weighted players: player has a weight (a traffic volume, a bandwidth demand, a share of ownership) and pays for each edge it uses a share proportional to its weight. The equal-split potential is then lost, and the paper notes that weighted games with three or more players need not have a pure Nash equilibrium at all (Chen and Roughgarden, Network design with weighted players, SPAA 2006). Theorem 6.3 identifies a natural class in which equilibria survive: all players share one source and one sink. For that class it shows more than existence. The simplest decentralized procedure, letting players in turn switch to a cheapest route, always stops, and where it stops is an equilibrium.
A finite directed multigraph has a finite set of arcs; each arc has a tail and a head vertex, and parallel arcs between the same two vertices are allowed. Fix a source and a sink . A simple – path is a sequence of arcs (), each starting where the previous one ends, beginning at , ending at , and visiting no vertex twice; it is identified with its arc set . Write for the finite set of these paths.
The weighted single-commodity game has a finite set of players; player has a weight , arc has a fixed cost , and every player's strategy set is . In a profile let
be the total weight on arc . Player pays
A profile is a (pure) Nash equilibrium if no player can lower its payment by switching alone to another path.
A best-response move of player replaces by a path that minimises 's payment given the other players' paths, provided this strictly lowers 's payment. Best-response dynamics is any sequence of profiles in which each profile arises from the previous one by a best-response move of some player.
For every such game with and :
The goal asserts only termination and existence; it fixes no bound on the length of a run.
For a profile define the marginal cost of a path, , and the tuple of all values , , sorted increasingly. With strictly positive arc costs:
The theorem gives a guarantee about dynamics, not only about existence: in single-commodity weighted network design, any order in which players take turns playing best responses reaches a stable outcome in finitely many steps. This places the single-commodity case on the positive side of the boundary drawn by the nonexistence examples for general weighted games. The tuple of sorted path costs is a potential that is not a single number, a device that applies to other games without an exact potential.
The result is proved in the paper; it has no machine-checked proof that this mission is aware of. A formal development contributes a reusable layer for weighted cost-sharing games (payments, best responses, Nash equilibria on arbitrary strategy families), a treatment of simple directed paths in multigraphs as strategy sets, and a lexicographic termination argument over sorted lists of extended reals. The goal is stated for nonnegative costs, as in the paper's model, while the printed proof uses positive costs; closing that gap is part of the work.
The obvious route, finding a real-valued function that every improving move decreases, is unavailable: the paper notes that Rosenthal's potential is not a potential once weights are added, and that improving moves can increase it. Termination must instead come from an ordinal quantity, a whole sorted list compared lexicographically, and the move of one player changes the marginal costs of every path that shares an arc with the old or the new route, in both directions.
The argument also depends on the shape of the strategy sets. Two distinct simple – paths are never nested as arc sets; with walks that repeat vertices, or with arbitrary strategy families, the comparison between a path's marginal cost before and after a deviation can fail. Arcs of cost zero create a further gap: is on an unused free arc, and the strict inequalities of the proof degenerate, so the nonnegative-cost goal needs more than the printed argument.
Finset of arcs; the strategy family of every player is the finite set of arc sets of simple – paths (a list of consecutive arcs with distinct visited vertices). There are no paths when .IsStandard); the milestones (6.1) and the lexicographic decrease assume .ℝ≥0∞): an unused arc of positive cost contributes . Computing it in the reals, where , would make unused paths free and the milestones false.Contributions welcome: lemmas on simple paths in multigraphs (non-nestedness), the multiset-to-sorted-list lexicographic comparison, and the treatment of zero-cost arcs.
Every step of the dynamic programming algorithm on a general state space does three things: it takes a conditional expectation of the cost-to-go under a transition kernel, it minimizes the resulting function of state and control over the control, and, if a policy is to be produced, it picks a control for each state that attains or nearly attains that minimum. On a finite or countable state space all three are harmless. On an uncountable state space each can destroy the measurability needed to take the next expectation: the infimum over an uncountable family of measurable functions need not be measurable, and a minimizer chosen state by state need not be a measurable function of the state, so it does not define a policy at all.
Section 7.5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), settles the three operations for semicontinuous costs and continuous kernels. The results are the topological half of the book's measurability theory; the descriptive set theory half (lower semianalytic functions and analytically measurable selectors, §7.6–7.7) is a separate mission in this series. The semicontinuous results are what Propositions 8.6–8.7 and Corollaries 9.17.2–9.17.3 of the book use to obtain Borel-measurable optimal policies for finite-horizon and infinite-horizon models with lower semicontinuous costs and compact control sets.
Timeline. The exact selection theorem for lower semicontinuous functions (Proposition 7.33 below) is credited by the book's notes to Dubins and Savage, How to Gamble If You Must (1965). The Hausdorff metric on closed sets goes back to Hausdorff's Set Theory. Measurable selection in the closed-valued setting was later systematized by Kuratowski and Ryll-Nardzewski (1965), whose theorem gives a different route to results of this kind.
Throughout, is the extended real line. A function on a metrizable space is lower semicontinuous if every sublevel set , , is closed, and upper semicontinuous if every superlevel set is closed (Definition 7.13). is the space of bounded continuous real-valued functions on .
For a separable metrizable space , is the set of Borel probability measures on with the weak topology (convergence of integrals of functions in ). A stochastic kernel on given is a map from to , and it is continuous if this map is continuous (Definition 7.12). The integral of a Borel-measurable is with the convention (Eq. (43) of Chapter 7).
For a compact metric space , is the collection of closed subsets of with the topology of the Hausdorff metric (Appendix C). For , the section at is , the projection is , and a function has its graph in if for every . "Borel-measurable" refers to the Borel σ-algebras of the topologies in question; on this is the Borel σ-algebra of the subspace topology.
Let be metrizable, compact metrizable, closed, and lower semicontinuous. Put
Then is closed, is lower semicontinuous, and there is a Borel-measurable with graph in and
The results. Propositions 7.31–7.33 are the closure properties that make the dynamic programming recursion stay inside the class of lower semicontinuous functions bounded below: the expectation step preserves the class (7.31), the minimization step preserves it (7.32, 7.33), and the minimization admits a Borel-measurable exact minimizer (7.33). This is why, in semicontinuous models, the optimal cost functions are lower semicontinuous and optimal policies can be taken Borel-measurable and nonrandomized. Proposition 7.34 gives the weaker, -optimal counterpart for upper semicontinuous costs, where the infimum need not be attained.
Formalizing them. All of these results are proved in the book; none is open. As far as is known, none has a machine-checked proof: Mathlib has semicontinuity, the Hausdorff extended metric on closed and on nonempty compact sets, and the weak topology on probability measures, but no theorem combining them into a measurable selection result of this kind. A formal development would supply measurable selectors for semicontinuous minimization in Lean and the Borel-measurability of set-valued maps into the hyperspace of closed sets, both reusable well beyond dynamic programming.
The obvious attempt at the goal is to pick, for each , some minimizer of over the compact section . The minimizer exists by compactness and lower semicontinuity, but the choice is made pointwise and gives no control on measurability: a minimizer chosen by the axiom of choice need not be Borel-measurable. The argmin sets vary with only semicontinuously: they can jump from a single point to a large set, so a continuous selection generally does not exist, and continuity arguments cannot replace measurability. Lemma 7.18 isolates the hardest part: a choice of a point of each nonempty closed set that is measurable as a function of the set itself.
A second difficulty is bookkeeping at infinity. Values are allowed throughout, so sublevel sets, minima, integrals and -bounds must all be handled in ; the integral in Proposition 7.31 uses the convention , which is not Mathlib's.
EReal. The only place where values of opposite infinite sign are combined is the integral, which is the published definition DupacovaWets.Consistency.expect (reused, not restated): with an explicit case returning when , exactly the book's convention (42). The -bound of Proposition 7.34 adds a real to a value different from , which is safe in EReal.LowerSemicontinuous/UpperSemicontinuous, equivalent to Definition 7.13 for EReal-valued functions. Lemma 7.13 of the book (the sequential characterization) is Mathlib's lowerSemicontinuous_iff_le_liminf together with first countability of metrizable spaces, and is not restated here.LowerSemicontinuousOn f D (resp. UpperSemicontinuousOn); values off play no role. is Prod.fst '' D, selectors are functions on that subtype, and its σ-algebra is the Borel σ-algebra of the subspace topology.Closeds Y, and for compact is NonemptyCompacts Y, each with the Hausdorff extended metric and the Borel σ-algebra of its topology. This topology agrees with the book's (the exponential topology of Appendix C, independent of the metric).BddBelow in EReal would be vacuous and is not used.A complete development needs the Borel structure of the hyperspace (measurability of maps into Closeds Y from upper semicontinuity in the sense of Kuratowski, Proposition C.4 of the book), the construction of a measurable choice function on NonemptyCompacts Y, and approximation of semicontinuous functions by monotone sequences in . Each of these is reusable on its own; proofs of individual milestones by any route are welcome.
We establish the polynomial simulation needed for WordRAM-based NP proofs. It reuses the same machines and Cook–Levin definitions, with uniform programs, logarithmic word widths, and standard bit input/output.
The targets cover function outputs and verifier verdicts, including loading and serialization costs.
This adapts Cook–Reckhow’s Theorem 2(a), pp. 361–363, to Hagerup’s bounded-word operations, including multiplication; no particular simulation exponent is prescribed.
Mean field games (MFG), introduced by Lasry and Lions and by Huang, Caines and Malhamé, describe Nash equilibria of very large populations of identical rational agents. The equilibrium is a coupled system: a backward Hamilton–Jacobi–Bellman equation for the value function of a representative agent and a forward Fokker–Planck equation for the density of the population. In the planning problem, proposed by P.-L. Lions, both the initial density and the final density are prescribed, and one asks for a cost structure under which the population moves from one to the other. This is a mean field analogue of optimal transport.
Achdou, Camilli and Capuzzo-Dolcetta (hal-00465404, SIAM J. Control Optim. 2012) propose finite-difference schemes for the planning problem. Mission I of this series treats the existence of a solution of the discrete planning scheme. Since the two boundary conditions on make the discrete system hard to solve directly, the paper also introduces a penalized scheme, in which the initial condition is replaced by a penalty ; for each this is a standard discrete MFG system with a unique solution. This mission formalizes the paper's §3.2: the penalized solutions converge, as , to a solution of the planning scheme.
Fix integers , , a horizon and a viscosity ; put and . The grid consists of the points , (periodic indices). A grid function is a real function on ; time levels are .
The planning scheme (18) asks for families with, for ,
, and . The penalized scheme (20)–(23) has the same two equations, for , , and in place of .
Under the hypotheses of Theorem 1, for every sequence , every choice of penalized solutions , and every limit in ,
If is strictly convex, the whole sequence converges to the unique solution of (43)–(46) with .
In 3–5 the constant depends on , and the data, never on .
Proposition 4 justifies the penalized scheme as a way to compute solutions of the discrete planning problem. The penalized system has a standard initial–terminal structure that Newton's method (the paper's §4) handles well. The planning system does not, because it prescribes two conditions on and none on . The estimates of Propositions 2–3 and Corollary 1 also give a rate: the initial mismatch of the penalized density is .
The results are proved in the paper. None of them has been machine-checked: the platform holds no formalization of mean field games, of their finite-difference schemes, or of the Lasry–Lions monotonicity argument. A complete development would yield a reusable library of the monotone finite-difference operators on the discrete torus, a formal Lasry–Lions uniqueness argument for discrete MFG systems, and a template for compactness-plus-uniqueness convergence proofs in finite dimension.
Compactness of the densities is free, since is compact. Passing to the limit in the scheme needs only continuity of , and . The substance lies in the two uniform estimates.
All objects live in the namespace MFGPlanning.Penalized.
ZMod Nh × ZMod Nh (periodicity is built in), time levels are Fin (NT + 1), and the four momentum components are Fin 4 indices 0, …, 3.EReal, so unbounded suprema are .Three trivializing formalizations are ruled out. The constants in Propositions 2–3 and Corollary 1 are quantified before and before the solution. The goal quantifies over every sequence and assumes no convergence of and no limit solution. Its part 2 does not assume convergence of .
The existence of a solution of the planning scheme (Theorem 1) is posed in mission I and not restated here. A solver of Proposition 2 will need it once mission I's goal is proved. The existence and uniqueness of solutions of (20)–(23) are quoted by the paper from Achdou–Capuzzo-Dolcetta (2010) and are not items. Welcome contributions include discrete summation-by-parts lemmas on the torus, the discrete comparison principle for monotone schemes, and the Poincaré-type inequality on zero-mean grid functions.
Mean field games (Lasry and Lions, 2006–2007; Huang, Malhamé and Caines, 2006) model the limit of a large population of identical rational agents. Each agent solves an optimal control problem whose cost depends on the distribution of all agents, and the distribution is in turn transported by the agents' optimal feedback. In the continuous setting this gives a coupled system: a backward Hamilton–Jacobi equation for the value function and a forward Fokker–Planck equation for the density .
In the usual formulation, is prescribed at the initial time and at the final time. The planning problem, introduced by P.-L. Lions in his Collège de France lectures, prescribes instead both the initial density and the final density , and asks for a cost (through ) that steers the population from one to the other. According to the paper (§1, pp. 2–3), Lions proved existence for the continuous planning problem in mainly two cases: with a smooth, strictly convex, superlinear Hamiltonian; and with or close to it. In both cases the coupling is local and the densities are smooth and bounded away from . Existence for and more general Hamiltonians was then open, and for sublinear , and short horizons there is no solution.
Achdou, Camilli and Capuzzo-Dolcetta (hal-00465404, 2010; SIAM J. Control Optim. 2012) introduced a finite-difference scheme for the planning problem and proved that the discrete system has a solution. The proof writes the scheme as the optimality system of a discrete optimal control problem, a Fokker–Planck equation driven by a control, and obtains a solution from a saddle point given by the Fenchel–Rockafellar duality theorem. This mission formalizes that existence result: Theorem 1 of §3.1 together with the lemmas on which its proof rests.
Fix integers , a horizon and a viscosity ; let and . The grid is the periodic grid on the two-dimensional torus, with points , . On grid functions the scheme uses the forward differences , , the four-component discrete gradient , the five-point Laplacian , a discrete divergence of four-component fields, and the transport operator .
A numerical Hamiltonian is monotone (nonincreasing in , nondecreasing in ), , convex, and superlinearly coercive in the directions where monotonicity does not bound it. The coupling is local: , with strictly convex, superlinear and . The set consists of the discrete probability densities, , . The discrete planning scheme (18) asks for with
for , with , and .
The duality is set up as follows. With the indicator of , let on dual variables . Let be the linear map sending to the discrete Hamilton–Jacobi operator and the discrete gradient of . Let if with , and otherwise, where . The Legendre–Fenchel transforms , act on primal variables , where is paired with (Remark 2).
Under (G1), (G3)–(G5), (24), , , and either or ( and ):
has a solution , with a finite common value. Moreover for some , and , with appended, solves the scheme (18), with .
Theorem 1 is the existence result for the finite-difference planning problem. It is used in the paper's second part (§3.2), where solutions of a penalized scheme, in which the final condition is relaxed into a penalty, are shown to converge to a solution of (18) as the penalty parameter vanishes. The penalized scheme is what is solved numerically. The discrete existence result covers general convex, monotone, coercive numerical Hamiltonians and every , which includes discretizations of the continuous cases that were still open when the paper was written.
The result has a published proof. What this mission adds is a machine-checked version of it: a complete discrete model of the planning problem (grid, operators, scheme, duality functionals) and the convex-analytic chain that connects it to the Fenchel–Rockafellar theorem. As far as a search of the platform shows, no part of this has been formalized; the series' second mission formalizes the convergence of the penalized scheme on the same model.
Existence for a coupled forward–backward nonlinear system with conditions at both ends of the time interval is not reachable by a fixed-point or time-marching argument: the Hamilton–Jacobi equation runs backward and the Fokker–Planck equation forward, and the final density is imposed rather than computed. The approach goes through duality, and three points are delicate.
The Lean development lives in the namespace MFGPlanning.Existence. A structure Data carries , , , at the grid points, , and . Committed conventions:
ZMod Nh × ZMod Nh (periodic), and as in the paper;Fin 4 indices 0..3;Fin (NT+1) for and the scheme, and Fin NT for the duality variables. M k is and α k is (Remark 2), and Fin.snoc M mT appends ;EReal-valued lattice suprema and infima, so unbounded suprema are and not a junk value. Convexity of an extended-valued functional is convexity of its epigraph.Disclosed encodings:
Theorem 1 is not reducible to "the scheme (18) has a solution". The goal also asserts that the primal and dual problems attain their minima, that there is no duality gap with a finite value, and that . The duality functionals are never real-valued suprema, which would make (30) and (31) hold or fail for junk reasons. A complete development needs finite-dimensional convex analysis on extended-valued functions: conjugates, the Fenchel–Rockafellar theorem with attainment, and subdifferential optimality conditions. These parts are reusable well beyond this mission, and proofs of them as separate theorems are welcome.
Single-machine sequencing is the base case of deterministic scheduling theory. Many multi-machine and shop problems are analysed by reduction to it, and many bounds and approximation algorithms for harder models use it as a subroutine. A central objective class is the bottleneck or minmax objective. Each job carries a nondecreasing cost of its completion time, and the schedule is judged by its worst job. Maximum lateness, maximum tardiness and maximum weighted tardiness are all special cases.
Before 1973 the minmax problem was solved without precedence constraints. Jackson (1955) showed that ordering by due date minimizes maximum lateness. Moore (1968, Management Science 15(1)) gave a procedure for general nondecreasing deferral costs, and Lawler and Moore (1969) gave a related method. In Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5), 1973, Lawler showed that arbitrary precedence constraints can be added at no loss of efficiency. Jobs are chosen from last to first, by a single comparison of costs at a known time. The resulting procedure is the standard algorithm for the problem written in the classification of Graham, Lawler, Lenstra and Rinnooy Kan (1979). It is one of the first polynomial-time results for precedence-constrained scheduling that every survey of the field cites.
A finite, nonempty set of jobs is processed on a single machine, one job at a time and without interruption. Each job has a processing time and a cost function that is monotone nondecreasing. The value is the cost incurred when is completed at time .
The precedence constraints are an arbitrary relation on jobs: means that job is required to precede job . A sequence lists every job of once. It observes the precedence constraints if never holds for positions . The machine starts at time with no idle time, so the completion time of is . The maximum incurred cost of is
and a feasible is minmax optimal if for every feasible .
For a set of jobs, is the set of jobs of that are not required to precede any other job of , and . Lawler's rule builds a sequence from the last position to the first. With the jobs not yet placed, it chooses with , places in the latest open position and removes it from . Ties are broken arbitrarily. In Lean the objects are IsFeasible, lastEligible (), IsMinmaxOptimal and IsLawlerSequence, in namespace LawlerPrec.MinMax. They are built on the published MooreLateJobs.Shared.completionTime and MooreLateJobs.MaxDeferral.maxCost.
Every sequence that Lawler's rule can produce, under any tie-breaking, observes the precedence constraints and satisfies
This is the statement of §3 (p. 545), "An efficient algorithm for finding a minmax optimal sequence follows immediately from the theorem above". It contains no constants.
The result shows that is solvable in polynomial time for every family of nondecreasing costs. The ordering of an optimal sequence depends on the costs only through their values at the partial sums along the way. The deadline problem is a corollary (§5): sequencing from last to first by latest deadline among the currently available jobs avoids tardiness whenever any sequence does. The last-to-first scheme is reused in later backward rules for objectives. A formal statement of the rule, its feasibility and its optimality makes these extensions available for formal reuse.
The result is classical and its proof is short. No machine-checked proof of it is known to be in Mathlib. The work this mission asks for is a formal proof of the known exchange argument and of the induction that turns the Theorem into the algorithm's correctness. The induction needs the reduced problem's sets and times to be the correct ones at each stage, which the definitions fix.
The exchange argument of §2 is elementary. The difficulty lies in stating the algorithm faithfully and carrying the induction. At each stage the eligible set and the time must be recomputed on the remaining jobs, with constraints into already placed jobs ignored. The induction must also show that the rule's sequence is feasible, which is a conclusion and not an assumption.
A first attempt often proves only the Theorem, that some optimal sequence has last. That statement says nothing about a sequence built entirely by the rule, because an optimal sequence of with last need not restrict to an optimal sequence of . Optimality of the rule's whole sequence is the target, and milestone 5 isolates the corresponding step of the page.
ι with decidable equality, and the job set is J : Finset ι.a : ι → ℝ, costs are c : ι → ℝ → ℝ, and the precedence constraints are prec : ι → ι → Prop.J. Positions are 0-based, and completion times are prefix sums (MooreLateJobs.Shared.completionAt).prec is arbitrary: it is not assumed transitive, irreflexive or acyclic. A cycle among distinct jobs leaves no feasible sequence. A self-loop constrains nothing, both in feasibility and in (the "others" of the page exclude the job itself).The standing assumptions of §1 appear as hypotheses wherever they are used: monotone nondecreasing for , and nonempty where the maximum is taken. Two hypotheses are added relative to the page and disclosed in each statement. Processing times are non-negative (), since they are durations and the exchange argument fails without them. The Theorem also assumes the existence of a feasible sequence, which its conclusion presupposes.
The rule is the property IsLawlerSequence of a finished sequence. At each position , the job there lies in of the jobs in positions and minimizes the cost at their total processing time. Every tie-break is covered. The rule is not a deterministic function, and it is not an arbitrary choice function. Feasibility of the rule's output is part of the goal's conclusion, so the goal cannot be obtained by assuming it. A statement that compares the rule only with some sequence, or that asserts only that an optimal sequence exists, is weaker and is ruled out by the goal's form. Milestone 6 shows the goal's hypotheses are satisfiable whenever a feasible sequence exists.
The operation count of §4, the first-to-last rule of §5 and the deadline corollaries of §5 are not part of this mission. A development needs only finite lists and finsets from Mathlib. Lemmas about moving an element to the end of a duplicate-free list, and about prefix sums under that move, are reusable for other exchange arguments in single-machine scheduling.
Empirical risk minimization (ERM) chooses, from a class of loss functions, the one with the smallest average loss on a sample . Its standard guarantees bound the excess population risk by a term of order , whatever the variance of the losses. When good functions in have small variance, a better trade-off is available in principle: minimize the empirical risk plus a standard-deviation penalty . Maurer and Pontil (COLT 2009) showed that this sample variance penalization enjoys faster rates, but the penalized objective is non-convex even for convex losses, so it cannot be minimized efficiently in general.
Duchi and Namkoong (arXiv:1610.02581v3, 2017; NIPS 2017) replace the variance penalty by a distributionally robust objective: the worst-case average loss over all reweightings of the sample within a -divergence ball of radius . This objective is convex whenever the loss is convex, and it equals the empirical risk plus the standard-deviation penalty up to an error of order . Theorem 3 of the paper turns this into a guarantee for the minimizer of the robust objective, using covering numbers of the class. This mission formalizes Theorem 3 and the lemmas its proof rests on.
Let be a measurable space, a probability measure on it, and () an i.i.d. sample from with empirical distribution . Let be a nonempty class of measurable functions , and set . Write , for the variance of , and
For , the ball is the set of weight vectors with , and : the distributions on the sample with for . The robust risk of is
and a robust minimizer is any .
Complexity is measured by empirical covering numbers. For , is the least number of points such that every lies within sup-distance of some . For let , and
Let , , and . With probability at least , every robust minimizer satisfies
Under the same hypotheses and with the same probability, simultaneously for all ,
Inequality (15) says the robust risk is a uniform upper confidence bound on the population risk, with an slack instead of the slack of the empirical risk. Inequality (16) says the robust minimizer competes with the best variance-penalized population risk in the class. When some has small risk and small variance, the excess risk of is of order up to the covering term, a rate ERM does not achieve in general (§3.3 of the paper gives an example). For a parametric class with polynomial in , choosing gives Corollaries 3.1 and 3.2 of the paper.
The results are proved in the paper; none of them has a machine-checked proof that we know of. The mission's output is a formal proof of Theorem 3 and its ingredients: a deterministic analysis of the -constrained linear program (Theorem 1 (10)), a covering-number empirical Bernstein inequality (Lemma C.1, from Maurer and Pontil), concentration of the sample standard deviation (Lemma A.1), and the scalar Bernstein inequality in the form used. Each of these is reusable outside distributionally robust optimization.
The deterministic part, (10), is a short analysis of a quadratically constrained linear program. The main obstacle is Lemma C.1. A union bound over a cover of fails directly: the cover depends on the sample, and a population-level cover of need not be finite. The standard route goes through a ghost sample of size (hence covering at points), a symmetrization that must preserve the sample variance rather than only the mean, and a concentration bound for the sample variance itself. Lemma A.1 needs concentration of , a non-linear and non-smooth function of the sample, at the sub-Gaussian rate . Finally, the oracle inequality (16) holds for an infimum over the whole class, while the concentration step for the comparison function is only proved for one fixed at a time.
The sample is the coordinate process of the product measure on (Measure.pi). Each probability statement bounds the probability of the bad event, the set of samples where the inequality fails for some (or some minimizer). This set need not be measurable, and its measure is then the outer measure, as is standard in empirical-process theory. Probability bounds are computed in , and the covering number is valued in , so an infinite covering number makes the bound trivial rather than collapsing to zero. Covering numbers are internal (centres in ) and use closed sup-norm balls, as on p. 9; this is Mathlib's Metric.coveringNumber. The empirical variance is normalized by . The ball is encoded as weight vectors on the sample points; with tied sample values this gives the same supremum as the paper's distributions on the sample. Statement (16) is formalized for every minimizer of the robust risk, and the event is empty if no minimizer exists. The infimum ranges over the nonempty class , on which every term is at least . Population moments are those of bounded measurable functions, hence finite.
Deviations from the printed text:
A trivializing formalization is ruled out: the bound is not taken over all functions, a probability bound is not formed from the real part of an infinite covering number, and the minimizer is not a hypothesis that can fail to exist for the given sample.
Needed infrastructure: product-measure concentration (Bernstein, and a bounded-difference or convex-Lipschitz inequality for ), symmetrization with a ghost sample, and finite union bounds over a cover. Contributions are welcome on any milestone, in particular a general covering-number empirical Bernstein inequality, which is reusable on its own.
In a network design game each of players must connect its own terminals in a shared graph, and the cost of every edge that is bought is split among the players who use it. Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 2008) studied the fair (Shapley) split, in which the users of an edge each pay . That game is a congestion game in the sense of Rosenthal (Networks 1973), so it has an exact potential function and pure Nash equilibria always exist.
When players carry different amounts of traffic, the natural rule is to split an edge's cost in proportion to weight: a player of weight on an edge whose users have total weight pays . The paper notes that this rule is analogous to weighted generalizations of the Shapley value (Monderer and Samet, Variations of the Shapley Value, Handbook of Game Theory III, 2002). The weighted model leaves Rosenthal's framework: the share depends on which players use an edge, not only on how many, and Chen and Roughgarden (SPAA 2006) showed that weighted games with three or more players need not have a pure Nash equilibrium at all. Section 6 of the paper identifies structural conditions under which equilibria do exist. This mission covers the first of them.
Timeline. Rosenthal (1973): every congestion game has a pure Nash equilibrium, via an exact potential. Monderer and Shapley (GEB 1996): potential and weighted potential games, and the equivalence of exact potential games with congestion games. Anshelevich et al. (FOCS 2004, journal 2008): Theorem 6.1, existence when every resource is shared by at most two players, and Theorem 6.3, existence when all players share a source and a sink. Chen and Roughgarden (2006): weighted network design games with three or more players may have no pure equilibrium.
A weighted cost-sharing game consists of a finite set of players, a finite ground set of edges (resources), and for each player :
together with a fixed edge cost for every . A profile picks for every player. For an edge , is the total weight of the players with , and player 's payment is
A profile is a pure Nash equilibrium when no player has a with , where is the profile in which plays and everyone else keeps their strategy.
The strategy space of player is the set of edges that occur in at least one strategy of . The hypothesis of Theorem 6.1 is that every edge lies in the strategy spaces of at most two players: no edge can ever be shared by three players, whatever they choose.
The network design game is the instance in which is the edge set of a graph and is the set of edge sets of paths connecting player 's source to its sink .
The paper's proof uses an explicit function with when is unused, when alone uses , and when and both use it, where . It is part of the definitions of this mission.
If every edge lies in the strategy spaces of at most two players, there is a weighted potential: a real function on profiles with
and, if every is nonempty, a pure Nash equilibrium exists. The goal asserts the existence of such a rather than fixing the paper's formula, so it remains valid for any other weighted potential.
An extra item states Corollary 6.2: every two-player weighted game with nonempty strategy sets has a pure Nash equilibrium.
The result. Theorem 6.1 is one of the two existence results the paper proves for weighted cost sharing, a game that in general has no pure equilibrium. It shows that the obstruction found by Chen and Roughgarden needs resources shared by three or more players: whenever sharing is limited to pairs, the game is a weighted potential game, so improving moves cannot cycle and equilibria exist. Corollary 6.2 makes the two-player case unconditional, and the paper notes that the same potential gives a (weak) bound on the price of stability.
Formalizing it. The result is proved in the paper; to our knowledge no machine-checked version exists. The mission produces a reusable Lean model of weight-proportional cost sharing (shared in form with the companion mission on single-source single-sink weighted games), an explicit weighted potential, and the general step from a weighted potential to a pure equilibrium, which applies to any finite game with positive weights.
The obvious approach, reusing Rosenthal's potential from the unweighted game, fails: the paper observes that in a weighted game improving moves can increase it. A player's share of an edge depends on the weights of the specific co-users, so no function of the edge loads alone can track all players' costs. The identity must therefore hold for every unilateral move, including moves that leave some edges and join others at the same time, and for every pair of possible co-users of an edge. The statement fails without the at-most-two hypothesis, so any argument has to use it in an essential way. The existence step needs the identity on all profiles reachable by feasible deviations, not only along a single path of moves.
Lean namespace PriceOfStability.WeightedPotential. Players form a Fintype ι and edges a Fintype E; a game is a structure with strategies : ι → Finset (Finset E), weight : ι → ℝ and edgeCost : E → ℝ. Standing assumptions wᵢ ≥ 1 and c_e ≥ 0 are the predicate IsStandard. Profiles are functions ι → Finset E with the feasibility predicate IsProfile; every deviation is to a feasible strategy, via Function.update. Nash equilibria are pure and in cost form. The strategy-space hypothesis is a bound on the number of players whose strategy space (the union of their strategies) contains each edge — not a bound on the users in one profile, which would be a different statement. Φ_e is computed from the current users of e; its value with three or more users is a placeholder that never arises under the hypothesis. Strategies are arbitrary subsets of the ground set, as the paper's remark after the proof allows, so the network game is a special case.
The goal is not satisfiable trivially: the function Φ must satisfy the weighted identity for every feasible unilateral deviation from every profile, and an exact (unweighted) potential is not what is asserted. Nonempty strategy sets are added explicitly for the existence part, since without a profile there is no equilibrium.
Needed infrastructure: finite sums over filtered Finsets, the improvement-path argument over the finite set of profiles. The improvement-path lemma (milestone 3) is reusable for any weighted potential game. Contributions of proofs for any milestone are welcome.
Scheduling in a multiclass queueing network asks which waiting job a server should work on next when jobs of several types share stations and revisit them along fixed routes. Such networks model semiconductor wafer fabs, job shops and communication switches. Optimal policies are rarely computable: the state space is countably infinite, and even deciding properties of optimal policies is hard (Papadimitriou and Tsitsiklis 1999). A practical substitute is the achievable region approach: describe, by constraints that every policy must satisfy, a set containing all performance vectors any policy can achieve, then optimize a linear cost over that set to get a lower bound on the optimal cost.
Bertsimas, Paschalidis and Tsitsiklis (MIT Sloan working paper 1992; Ann. Appl. Probab. 1994) gave a general method for producing such constraints for open networks, by computing the steady-state drift of quadratic potential functions. This mission formalizes their first-order bounds (Section 4).
Timeline:
A network has single-server stations and job classes. Class is served at station , and is the set of classes served at station . Class- jobs arrive from outside as a Poisson stream of rate , service times are exponential with rate , and after service a class- job becomes a class- job with probability or leaves with probability . The traffic equations
have a unique solution (the network is open), and at every station.
The state counts the jobs of each class. A Markovian policy decides from the current state which classes are in service, at most one per station and only classes with jobs present; idling is allowed. Write for the event that station serves class , and for the event that station is idle. Under such a policy is a continuous-time Markov chain. Assumption A requires that it has a unique invariant distribution and that for all . Let , which equals with the mean response time of class (Little's law), and define
For a set of classes, f-parameters are reals for such that is nonnegative and the same for all ; that common value is , and when (restriction (17)). The sums over include the exit .
For every policy satisfying Assumption A, every and every f-parameters satisfying (17),
where
The formal goal is the product form .
Theorem 4.1 gives, for each choice of and , a linear inequality on mean response times valid for all admissible policies. Minimizing a linear holding cost subject to these inequalities is a linear program whose value bounds the optimal scheduling cost from below; the paper reports numerical values of such bounds in its Section 9. Theorems 4.2–4.4 show that a polynomial-size polyhedron in the variables implies all of these inequalities at once, so the parametric search over is unnecessary.
The results are proved in the paper. As far as is known, none of them has a machine-checked proof. Formalizing them requires a Lean treatment of invariant distributions of controlled countable-state Markov chains with unbounded test functions, which is currently absent from Mathlib, and then the algebra of the drift identities. The definitions here (network data, Markovian sequencing policies, the generator, Assumption A) are the substrate that the paper's later results on routing, closed networks and higher-order bounds would reuse.
Every statement except Theorem 4.4 rests on taking expectations of the generator applied to unbounded functions (, ) under the invariant distribution. The invariance condition is stated only for indicators of single states; extending to quadratic needs an interchange of summations justified by the second-moment condition of Assumption A. The utilization identity additionally needs uniqueness of the traffic solution to identify with . Theorem 4.1 then needs the sign bookkeeping that turns an identity into an inequality: the terms dropped are nonnegative only because on , and at most one class per station is in service.
Classes are Fin R, stations Fin N, states Fin R → ℕ, all rates and probabilities real. A policy is a Bool-valued function of the state with the two admissibility constraints; work conservation is not assumed. Invariance is global balance of the generator on the countable state space; expectations are tsums. The uniformized chain and the epochs of the paper are not built: the paper notes that its expectations at are expectations under the invariant distribution of .
Conventions fixed in Lean:
A quotient-form statement of (18) would be trivially true when , and defining as would make the utilization identity hold by definition; both are excluded.
Welcome contributions: a general lemma extending global balance to test functions of polynomial growth under moment conditions; proofs of the drift identities; the deterministic Theorem 4.4.
Periodic-review inventory control with a fixed ordering cost is one of the oldest problems in operations research. A firm reviews its stock at the beginning of each of periods, decides whether to place an order, pays a fixed cost for every order it places, and pays holding costs on leftover stock and penalties on unmet (backlogged) demand. When demand is random and correlated across periods, and the firm's forecast evolves as information arrives, the optimal policy solves a dynamic program over the whole information state. That program is intractable in general, and in practice firms use heuristics with no performance guarantee.
Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2), 2007) gave policies with worst-case guarantees for these models, using a "marginal cost accounting" scheme that charges each unit's holding cost to the period in which it was ordered. For the model with fixed ordering costs, the stochastic lot-sizing problem, they assume that the demand of each period is known at the beginning of that period (make-to-order systems, or settings where the short-term forecast is accurate), while demand further ahead stays random and arbitrarily correlated. Under this assumption they define the triple-balancing policy and prove it costs at most three times the optimum in expectation.
Timeline:
There are periods on a probability space with a filtration : is the information available at the beginning of period . The data are a fixed ordering cost , per-unit holding costs , per-unit backlogging penalties , an initial inventory level , and nonnegative demands . The per-unit ordering cost is zero, the lead time is zero and there is no discounting. The defining assumption is that is -measurable: the demand of a period is known when the period begins. For every period there is a conditional joint distribution of the demands given , under which every conditional mean is finite.
A feasible policy is an order process with and determined by . Its inventory levels are before ordering and after ordering, and its cost is
The triple-balancing policy TB uses two rules. Let be the last period before in which TB ordered ( if none). Rule 1: TB orders in period if and only if, without an order in , the accumulated backlogging cost over would exceed . Rule 2: when it orders in , it orders
the largest quantity whose expected marginal holding cost over is at most . When it orders in period , it orders exactly enough to clear the backorders and meet . Let be the number of orders TB places.
For every instance, the triple-balancing policy TB and every feasible policy satisfy
The constant 3 is the paper's. The statement leaves the demand law, the information structure and the cost data unrestricted beyond the standing assumptions above.
Two non-milestone theorems show that the setting is not empty. A conditional demand law exists whenever demands are integrable, and a triple-balancing policy exists when .
The theorem gives a policy that can be computed online and comes with a worst-case expected-cost guarantee that does not depend on the demand distribution, the horizon or the cost data. In this setting the optimal policy is not computable in general, and the previously used heuristics have no such bound. The two lemmas separate a lower bound on every policy, in terms of TB's own number of orders, from an upper bound on TB's cost. The authors' subsequent work extends the balancing template to capacitated and multi-echelon models (§7 of the paper).
The result is proved in the paper. As far as we know, no machine-checked version exists of this theorem, of the balancing argument, or of a stochastic inventory model with correlated demand and evolving information. A formalization would check the argument, which is terse in places: the printed proof of Lemma 6.2 indexes its final sum loosely and must handle the event . It would also produce reusable infrastructure for policies adapted to a filtration, for regular conditional distributions of future demand, and for cost accounting over random intervals between orders.
The costs of TB and of an arbitrary policy cannot be compared period by period, because the two policies order at different, random times that depend on the evolving information. Any comparison has to be made over intervals whose endpoints are stopping times determined by TB, conditioned on the information at their start. At such a time the other policy may hold more or less stock than TB, and the bound must hold in both cases. Bounding each policy's cost on its own does not work: the guarantee rests on a coupling between when TB orders and what every other policy must pay over the same random stretch of time. The formal side adds a second difficulty. Rule 2 is defined through a conditional expectation viewed as a function of the order quantity, so it needs a regular conditional distribution and a measurable selection of the maximizer.
MeasureTheory.Filtration ℕ. A policy is feasible when it is nonnegative and adapted, and " known at the start of period " means is -measurable.Several trivializing formalizations are ruled out. Junk conditional expectations cannot make Rule 2 hold for every , because it uses kernel integrals in . Infinite expected costs cannot be read as . The policy class is not empty, because a separate theorem gives existence under (without some positive holding cost on the maximum in Rule 2 does not exist).
Contributions welcome: proofs of the existence theorems (measurable selection of , versions of regular conditional distributions), the stopping-time decomposition of the cost over TB's order intervals, and Lemmas 6.1 and 6.2.
The Łojasiewicz inequality states that near a critical point of a real-analytic function there are and with . Łojasiewicz used it in the 1960s to prove that every bounded trajectory of the gradient flow has finite length and converges to a single critical point, a conclusion that fails for general functions. The inequality has since become the standard tool for convergence analysis of descent methods on nonconvex problems.
Optimization problems are, however, rarely smooth: constraints enter through indicator functions, and objectives contain norms, maxima and penalties. Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007) 1205–1223) extended the inequality to nonsmooth subanalytic functions, replacing by a slope built from the limiting subdifferential. Their Section 3.1 treats functions continuous on a closed domain; Section 3.2, the subject of this mission, treats lower semicontinuous convex functions, which may jump to and whose domain need not be closed. The Kurdyka–Łojasiewicz framework built on this paper (Attouch–Bolte–Svaiter 2013; Bolte–Sabach–Teboulle 2014) underlies the convergence theory of proximal and splitting algorithms used throughout operations research.
Work in with the Euclidean norm, and let with domain .
A set is semianalytic if near every point it is a finite union of finite intersections of sets with real-analytic. It is subanalytic if near every point it is the projection of a bounded semianalytic subset of . A function is subanalytic when its graph is. Semialgebraic functions (norms, polynomials, indicators of polyhedra) are subanalytic.
The Fréchet subdifferential is the set of with , for , and is empty otherwise. The limiting subdifferential is the set of limits of with . The nonsmooth slope is , equal to when , and is the set of critical points. For lower semicontinuous convex , is the subdifferential of convex analysis and is the set of minimizers. Write for the minimum value and for the distance from to . The epigraphical sum is the Moreau envelope of .
Ratios follow the paper's conventions and .
Let be lower semicontinuous, convex and subanalytic with . For every bounded set there is such that
The exponent may depend on ; neither nor the bound is fixed.
Theorem 3.3 gives, for convex subanalytic functions, a Łojasiewicz inequality that is uniform on bounded sets rather than local at one critical point, and it needs neither continuity of on its domain nor a closed domain. Remark 3.4 of the paper exhibits a convex function covered by Theorem 3.3 but not by the continuous-case Theorem 3.1. Through inequality (20) of Section 4, it yields finite length and convergence rates for the subgradient flow of such functions. The intermediate inequality (15) is a Hölderian error bound, , of the kind that drives linear and sublinear rate analyses of first-order methods.
The result is proved in the paper; no machine-checked version of it, or of the nonsmooth Łojasiewicz inequality in any form, is known. Formalizing it would add to the library: subanalytic sets and functions, the limiting subdifferential of convex functions and its agreement with the classical one, the Moreau envelope with its critical points and infimum, and the passage from a growth condition to a Łojasiewicz inequality. Remarks 3.5 and 3.6 isolate parts that need no subanalytic geometry at all.
The convex-analysis steps (inequality (16), properties of the Moreau envelope) are classical. The obstacle is subanalytic geometry. The natural first idea, applying the Łojasiewicz factorization lemma directly to and , fails: is neither continuous nor finite, and its domain need not be subanalytic even when is convex and subanalytic (Example 2.5 of the paper). The milestones route through the Moreau envelope, which is continuous and finite, but subanalyticity is not preserved by infima over unbounded sets, so the subanalyticity of the envelope (Proposition 2.9) needs a localization argument. The subanalyticity of and of rests on the stability theory of subanalytic sets (Gabrielov's complement theorem, the projection theorem for globally subanalytic sets), none of which exists in Mathlib.
The space is EuclideanSpace ℝ (Fin n). Functions take values in EReal; "lower semicontinuous, convex, somewhere finite and never " is the published definition MoreauProx.Characterization.GammaZero, whose convexity is convexity of the epigraph. The Fréchet and limiting subdifferentials are the published NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff; the convex subdifferential subgrad appears only in Eq. (5), which proves the agreement and is never assumed. Semianalytic and subanalytic sets are defined from scratch for any finite-dimensional real normed space, so that one definition serves and its products; global subanalyticity is not defined. is written in EReal and converted to a real number only where it is finite. The bounded ratio (14) is encoded as " for every and every ", with real powers (Real.rpow, ). Inequalities (15) and (17) are imposed only where , since Lean sends to under toReal.
Trivializing encodings are ruled out: the goal is stated with the limiting subdifferential rather than an assumed convex subdifferential, the slope is never computed in ℝ≥0∞ where would make the ratio vacuous, and remains existential in with the quantifier order "for every there is ", so that is excluded at critical points in by .
A complete development needs a working theory of subanalytic sets (stability under finite unions, complements, closure, projections of bounded sets, the factorization lemma), the Moreau envelope of a convex function on and its property, and the convex-analytic description of the limiting subdifferential. The subanalytic-geometry layer and the Moreau-envelope facts are reusable well beyond this mission; contributions to either, or proofs of the convex-only milestones (Eq. (5), (16), Remarks 3.5–3.6), are welcome independently.