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?
In a multi-armed bandit problem a learner chooses one of actions in each of rounds and observes only the reward of the chosen action. Two models of the rewards have separate theories. In the stochastic model, each arm pays independent draws from a fixed distribution; algorithms such as UCB1 (Auer, Cesa-Bianchi & Fischer 2002) have regret of order , logarithmic in . In the adversarial model, an adversary chooses the rewards; Exp3 and its variants (Auer, Cesa-Bianchi, Freund & Schapire 2002) have regret of order , which is optimal there. An algorithm tuned for one model fails in the other: stochastic algorithms can suffer linear regret against an adversary, and adversarial algorithms pay even when the rewards are i.i.d.
Bubeck and Slivkins (arXiv:1202.4473, COLT 2012) asked whether one algorithm can be near-optimal in both models without knowing which one it faces. They answered yes with the algorithm SAO. This result started the "best of both worlds" line of work on bandits. Later contributions include EXP3++ (Seldin & Slivkins 2014) and Tsallis-INF (Zimmert & Seldin 2021).
There are arms and rounds. On round the algorithm draws an arm from a probability vector computed from the history it has observed. At the same time a reward vector is fixed, and the algorithm observes only .
The analysis uses importance-weighted estimates , the sample means , the averages , and the play counts .
SAO (Algorithm 1 of the paper) takes a parameter . It keeps a set of active arms, initially all arms, and samples them uniformly at first. On each round it applies a test, (12), that deactivates an arm whose estimate falls far below the best active one. The probability of a deactivated arm then decays as , where is the deactivation time and the arm's probability at that moment. Three further tests, (13)–(15), check that the observations stay consistent with stochastic rewards. If any of them fails on round , SAO switches permanently to the adversarial algorithm Exp3.P (Bubeck & Cesa-Bianchi 2012, Fig. 3.1) for the remaining rounds.
For every let . With probability at least , SAO with parameter satisfies, in the stochastic model (whenever some arm has ),
and, against every adaptive adversary with rewards in ,
The milestones follow the paper's proof in order:
The theorem shows that the stochastic and adversarial regret rates are not in conflict. A single algorithm, with no information about the model, gets pseudo-regret on stochastic rewards and regret against adaptive adversaries. Each rate is within polylogarithmic factors of optimal for its model. Later algorithms improved the logarithmic factors and removed the explicit switching, but they are compared against this result.
The theorem is proved in the paper. It is not known to have a machine-checked proof. Formalizing it requires a precise model of an adaptive adversary interacting with a randomized algorithm, martingale concentration with random variance (Lemma 4.4), and an exact statement of SAO including its boundary cases. The pieces are reusable: the interaction model, the estimators, Exp3.P and its high-probability guarantee all apply to other adversarial bandit results.
Neither standard analysis carries over. In the stochastic model, SAO's sampling probabilities are random and depend on the past, and a deactivated arm's probability keeps changing. Hoeffding-type bounds for a fixed sampling scheme therefore do not apply to . The variance of the importance-weighted estimate grows like , which is controlled only through the algorithm's own schedule (16). This is why Lemma 4.5 has the two-part radius with . In the adversarial model, the deterministic argument has to show that whenever the consistency tests pass, the regret accumulated before the switch is already small, for an adversary that adapts to the arms played. A union bound over all quantities, all arms and all times (§4.1) is needed before any deterministic reasoning, so every constant in the event matters.
All declarations live in the namespace BestBothWorlds.SAO.
Fin K and rounds are . An arm path is Fin n → Fin K.Real.log is the natural logarithm. All constants of Theorem 4.1 are explicit, with .A trivializing formalization is ruled out. The goal's hypotheses concern only the instance (, , , the distributions or the adversary). The algorithm's quantities (, , , the sampling probabilities) are computed by the definition of SAO and are never free variables or hypotheses. The adversarial half covers adaptive adversaries, not only oblivious reward tables.
The expectation form of Theorem 4.1 ( bounds with ), Theorem 1.1 and the two-armed warm-up of §3 are out of scope. Proofs of any milestone are welcome, as are alternative proofs of the concentration lemmas from Mathlib's martingale library.
Periodic-review inventory control with backorders is one of the basic models of operations research: in each period a manager decides how much to order, orders arrive after a lead time, unmet demand is backlogged at a penalty, and stock left over is charged a holding cost. When demands in different periods are independent, dynamic programming yields an optimal base-stock policy and computing it is tractable. In practice demands are correlated and forecasts evolve over time, for example under the martingale model of forecast evolution (Heath and Jackson, 1994, doi:10.1080/07408179408966604). The dynamic program then has to range over all possible information states, whose number is typically exponential in the input (Zipkin, 2000), so optimal policies are out of reach and the heuristics in use came without performance guarantees.
Levi, Pál, Roundy and Shmoys (Math. Oper. Res. 32(2):284–302, 2007) gave the first policy for this model with a worst-case guarantee that holds for arbitrary correlated, nonstationary demand distributions: the dual-balancing policy costs at most twice the optimum in expectation. The analysis rests on a marginal cost accounting that charges each order, at the time it is placed, all the holding cost its units will ever incur. This mission formalizes that guarantee.
There are periods and a known lead time : an order placed in period arrives in period . Period has a per-unit holding cost and a per-unit backlogging penalty . Ordering costs are zero (), which is the standing assumption of the paper's §4. The initial data are the net inventory and the pipeline orders .
Demands are nonnegative random variables on a probability space with a filtration ; is the information at the beginning of period , and is -measurable. A feasible policy places orders that are -measurable. Write (with for ), for the inventory position before ordering and after ordering.
The marginal holding cost of period is the holding cost that the units ordered in incur until the end of the horizon, and the marginal backlogging cost is the penalty incurred one lead time later:
The cost of is ; by Eq. (3) it differs from the total holding and backlogging cost only by a policy-independent nonnegative term.
A dual-balancing policy orders nothing after period , and in each period orders the quantity that balances the two conditional expected marginal costs:
For every dual-balancing policy and every feasible policy ,
The paper writes ; quantifying over all feasible is the same statement whenever an optimum exists and needs no existence assumption.
Two further items are not milestones. Eq. (3) states that, along every realization, the period-by-period holding and backlogging cost equals , which is why the cost of Eq. (4) is the right objective. The other states that a dual-balancing policy exists when and the demands are integrable, so the goal is not about an empty class.
The theorem gives a policy that is computable period by period, by a one-dimensional search, with a factor-two guarantee that holds for every joint demand distribution, including correlated, nonstationary and forecast-driven ones, where the optimal policy cannot be computed. The constant is tight: the paper exhibits instances where the ratio tends to two. The second mission of this series treats the stochastic lot-sizing problem of the same paper, which uses the same marginal cost accounting.
The result is proved in the paper; no machine-checked proof of it is known. Formalizing it produces a reusable model of the periodic-review backlogging system with lead times and adapted policies, a verified marginal cost identity, and a formal approximation guarantee for a stochastic inventory policy. The pathwise comparison lemmas are stated for arbitrary pairs of order sequences and so apply to other balancing-type policies.
The obvious attempt compares the two policies period by period. That fails: in a given period the dual-balancing policy may hold far more or far less inventory than the comparison policy, and neither the holding nor the backlogging cost of one period is bounded by the comparator's cost in that period. The comparison only works after re-charging holding costs to the period in which the units were ordered, which requires the identity Eq. (3) to be established exactly, including the pipeline units, the initial stock and the lead-time shift. The probabilistic step then needs the random index sets and to be determined by the information of period , so that conditioning on commutes with the indicators; this is where the nonanticipativity of both policies enters. The existence of a balancing quantity needs a measurable selection from conditional laws, and it fails without a positive late holding cost.
ℤ). Orders and demands are functions ℤ → Ω → ℝ; only periods are read, and the pipeline is substituted for .Filtration ℤ to which demands are adapted with a one-period lag; the paper's information vectors are a special case, and randomized policies are covered when their randomness is part of the information.A complete development needs finite-sum manipulations for Eq. (3) and Lemma 4.2, conditional expectation (tower property, pulling out bounded -measurable factors) for Lemma 4.1 and the goal, and regular conditional distributions with a measurable selection for the existence item. Theorem 4.2 (the randomized policy for integer demands) is outside this mission.
The bullwhip effect is the observation that the variability of orders grows as one moves up a supply chain, from the retailer to the wholesaler, the distributor and the factory, even when customer demand is stable. It was documented in industry practice by Lee, Padmanabhan and Whang (Management Science, 1997), who identified demand forecasting as one of its main causes. Amplified order variability raises the safety stock, capacity and transportation costs of every upstream firm, so the question of how large the effect is, and what reduces it, is central to supply chain management.
Chen, Drezner, Ryan and Simchi-Levi (Management Science 46(3), 2000) quantified the effect for a retailer that forecasts with a moving average and follows an order-up-to policy. Their §3 asks whether sharing customer demand information with every stage removes the effect. Theorem 3.1 (the companion mission of this series) shows that it does not; Theorem 3.2, the goal of this mission, gives the lower bound for the chain in which no demand information is shared.
Time is indexed by the integers . The retailer faces i.i.d. demand
where the error terms are independent and identically distributed from a symmetric distribution with mean and variance .
Single-stage policy (§2). With observations, a lead time , a safety factor and a constant , the retailer forms the moving-average estimates
raises its inventory position to the order-up-to point , and so orders . Orders may be negative: excess inventory is returned without cost.
Decentralized chain (§3). Stages form a serial chain; stage 1 is the retailer, and is the lead time between stages and . No stage sees customer demand except the retailer. Stage forecasts from the orders it receives,
uses the order-up-to point , and orders
For every stage and every period ,
The bound is the paper's, with its explicit constants. The paper asserts no tightness for this theorem, and none is claimed.
For the single-stage policy with any safety factor and any constant ,
This is the i.i.d. case of the paper's Theorem 2.2. With and the single-stage orders are the stage-1 orders of the chain, so Eq. (6) contains the case of the goal.
The result. Theorem 3.2 is half of the paper's comparison between centralized and decentralized information. When demand information is shared, the amplification from the retailer to stage in the i.i.d. case equals (Eq. (8)), which grows additively in the lead times. Without sharing, the lower bound (7) is a product over stages and grows multiplicatively. The paper concludes that centralizing demand information "can significantly reduce the bullwhip effect", and that the gap widens as one moves up the chain. Eq. (6) is the single-stage statement that forecasting with a moving average alone already amplifies variability, by a factor depending only on the ratio .
Formalizing it. The paper gives no proof of Theorem 3.2; it refers to Ryan (1997, PhD thesis) and to Chen et al. (1998). A machine-checked proof would therefore supply the first self-contained, verified argument for the multiplicative bound. The Gaussian special case of Eq. (6) is already formalized on Prove2Me, in the Snyder–Shen chapter on the bullwhip effect (SupplyChainTheory.bullwhip_signal_processing at ); that statement assumes Gaussian errors, whereas this mission assumes only symmetry, mean and variance . Neither the multistage bound nor the symmetric-error version of Eq. (6) has a formal proof.
The natural first idea is induction on the stage: treat the orders of stage as the demand of stage and apply the single-stage bound. That step fails, because the single-stage bound is a statement about i.i.d. demand, and the orders reaching stage are not i.i.d.: they are autocorrelated, and stage 's moving average of those orders interacts with the correlation in a way that can raise or lower the variance. Whether the product bound survives depends on controlling that interaction at every stage. For Eq. (6), the safety-stock term is a nonlinear function of the demands, and only symmetry of the errors, not normality, is available to control its interaction with the linear part of the order.
All objects live in the namespace ChenBullwhip.Decentralized.
IIDDemand P is the demand model on a probability space : a constant mu, sigma > 0, and errors eps : ℤ → Ω → ℝ that are measurable, mutually independent (iIndepFun), identically distributed, symmetric (eps t and -eps t have the same law), in , with mean and variance sigma ^ 2. Demand is D t = mu + eps t. Variances are Mathlib's ProbabilityTheory.variance.SingleStage defines , , , and of §2; is a free real parameter, as the paper does not fix it.Chain defines the forecasts and the orders by recursion on the stage, with the convention , so that stage 1 orders . The recursion is not printed in the paper; it is the §2.2 order identity applied to a stage whose incoming demand is , as the sequence of events on p. 440 describes.Disclosed hypotheses not on the page: (a moving average needs an observation), (the paper divides by ), and square-integrable errors (Mathlib's variance is off ). The paper's model (1) asks ; since affects no variance, no sign condition is imposed. Lead times are natural numbers. The statements hold in every period , with no stationarity hypothesis.
Trivializing formalizations are excluded: the orders are computed from the demands, not posited processes with a given covariance; the variances are genuine because every random variable involved is square integrable; and the ratio's denominator is .
A complete development needs variance and covariance calculus for finite linear combinations of independent variables, and, for Eq. (6), the vanishing of the covariance between an odd and an even function of a symmetric random vector. Both are reusable well beyond this mission. Proofs of either target, and general lemmas on variances of linear filters of i.i.d. sequences, are welcome.
SupplyChainTheory.*).The stochastic multi-armed bandit is the basic model of sequential decisions under uncertainty with partial feedback: a forecaster repeatedly picks one of options and observes only the reward of the option it picked. It models clinical trials, ad placement, routing and dynamic pricing, and is the building block of many reinforcement-learning algorithms. The question is how much reward is lost, compared with always playing the best option, through having to learn which option is best.
Chapter 2 of Bubeck and Cesa-Bianchi's monograph (arXiv:1204.5721v2) answers this for upper confidence bound (UCB) strategies.
There are arms. Arm has an unknown reward distribution with mean . At each round the forecaster selects an arm based on the past and receives a reward drawn from , independently of the past. Write , for the gap of arm , and for the number of times arm is selected in rounds . The pseudo-regret is
Moment condition (2.2). There is a convex with and for all and every arm's reward . Its Legendre–Fenchel transform is . For rewards one may take , for which .
-UCB. With the mean of the first rewards of arm , at round select
If the rewards satisfy (2.2), then -UCB with satisfies, for every ,
This is the bound the book's proof establishes. The printed statement has in place of ; see Formalization scope.
Theorem 2.1 says that the cost of learning grows only logarithmically in the horizon, with a constant set by how well each suboptimal arm can be told apart from the best one. Theorem 2.2 shows that, up to constants, this cannot be improved: for Bernoulli rewards any strategy that is good on every instance must pay per suboptimal arm, with constant . By (2.8) this constant is at least of order , matching (2.4). Together they are the template for the analysis of most optimistic algorithms: KL-UCB, linear and contextual UCB, and UCB-style reinforcement learning.
All results of the chapter are classical and proved on paper. This mission makes them machine-checked in a common model. That model has an explicit pseudo-regret, an explicit (generalized) inverse of , an explicit initialization rule for the algorithm, and a randomized-strategy model for the lower bound. Later chapters of the series and later papers on optimistic algorithms can build on it.
The deterministic part of the upper bound is short, so the main difficulty is probabilistic. The sample mean is taken over a random number of samples that depends on the algorithm's past. A Chernoff bound for a fixed sample size does not apply to it directly. The proof needs a union bound over all possible sample sizes, together with the representation in which the -th reward of each arm is a fixed random variable. Summing the resulting tail over rounds is where enters.
The lower bound needs a change-of-measure argument between two Bernoulli instances, applied to a forecaster that may be randomized and never knows the horizon. Expressing "the forecaster cannot distinguish the instances" requires the law of the whole interaction under two environments.
Model. Arms are Fin K with , rounds are , and the natural logarithm is used. Rewards are a stack: is the reward of the -st pull of arm , all mutually independent, identically distributed per arm. For every strategy this gives the same law of arms and rewards as the book's protocol. , and are the published definitions of ImprovedLinBandits.UCBDelta.armModel. The pseudo-regret is (2.1), , not the expected regret. The arms played are measurable random variables, so that every expectation is genuine.
and its inverse. takes values in the extended reals. .
Algorithm. The index is undefined while . Unplayed arms are therefore played first, so each arm is played once in rounds . Ties are broken arbitrarily.
Corrected misprint. The book prints Theorem 2.1 with constant term . Its proof yields (bound on times ). The printed form is false for Gaussian rewards with large gaps. The goal states the proof's version. (2.4) is correct as printed because .
Constants. No O(·) appears in the chapter's statements. The constants are the book's: in Theorem 2.1 and (2.4), and the factor in (2.4) and (2.8).
Conventions made explicit.
Conventions 1–3 hold for every the book uses.
Theorem 2.2. The forecaster is a measurable rule from the history and a fresh uniform seed to an arm. It does not depend on the horizon. Consistency is required on every Bernoulli instance, every suboptimal arm and every . A term with () is , and the is taken in the extended reals. The book proves only .
Ruled out. The algorithm cannot see unplayed rewards (its index uses only the sample means of rewards already received). Non-measurable arm choices, which would make the expectations vanish in Lean, are excluded. Consistency cannot be assumed only on the instance of the conclusion.
Needed infrastructure. Cramér–Chernoff bounds for sums of i.i.d. variables, Hoeffding's lemma, the stack representation of bandit interactions, and the divergence decomposition for randomized strategies. All are reusable beyond this mission, and contributions of any of them are welcome.
The inverse Galois problem asks whether every finite group occurs as the Galois group of a finite Galois extension of . For finite simple groups, a large part of the problem was settled by the rigidity method (Shih, Fried, Belyi, Matzat, Thompson) and its refinements such as the braid-group method. Between 1984 and 1989 this machinery realized 25 of the 26 sporadic simple groups as Galois groups over , in fact as Galois groups of regular extensions of . The Mathieu group was the single exception.
Timeline.
denotes the group of permutations of the 23 points , acting on the left, so . The paper fixes three explicit permutations
and the Mathieu group is the subgroup of generated by and . A -extension of a field is a Galois extension together with an isomorphism . A finite extension of is regular if it contains no nontrivial algebraic extension of .
For a triple of conjugacy classes of , the set consists of triples with that generate , and the Nielsen class is the set of orbits of under simultaneous conjugation by . The paper works with the classes , , , represented by .
Facts about stated in §3 (order , simplicity, 4-transitivity, 17 conjugacy classes), the membership , the count , the Riemann–Hurwitz count of Lemma 3.1, the hyperbolic triangle of Lemma 3.2, and the group-theoretic step of Corollary 3.6 ( is not normal in any strictly larger subgroup of ).
Theorem 1.1 removes the last sporadic exception: combined with earlier work, every sporadic simple group is the Galois group of a regular extension of (Corollary 1.4), and hence occurs as a Galois group over every number field, in infinitely many mutually independent ways.
The paper's proof is computer-assisted: Belyi maps were computed numerically and the final claims were certified in Magma and PARI/GP. No machine-checked proof in a proof assistant is known. A formal proof of the explicit-polynomial statements (Examples 1.2 and 3.7) would give an independent, kernel-checked certificate of Theorem 1.1. The group-theoretic milestones (order, simplicity, transitivity, class counts, the Nielsen count) are reusable for any later work on or the other Mathieu groups.
The rigidity method fails for : for every -stable triple of conjugacy classes the Nielsen class has size different from , so no rational point of a Hurwitz space is forced. The smallest positive size, for , leaves seven covers, and the fact that one of them has field of moduli was found by explicit computation, with no conceptual explanation. Certifying that a particular degree-23 polynomial has Galois group exactly requires both a lower bound (the group contains , for instance via cycle types and the classification of transitive groups of degree 23) and an upper bound (the group is contained in a conjugate of , for instance via resolvents or reduction modulo primes). Neither bound is a finite check inside current Mathlib.
is Equiv.Perm (Fin 23). The paper's point corresponds to k - 1 : Fin 23, and permutations compose as functions, which matches the paper's left-action convention. is defined as Subgroup.closure {g₁, g₂}, so it is not described up to isomorphism. Galois groups are groups of field automorphisms, K ≃ₐ[ℚ] K, and a -extension is recorded as a group isomorphism with . is RatFunc ℚ. "Unramified outside " for a number field is encoded as "every prime dividing the absolute discriminant lies in ", which is equivalent by Dedekind's discriminant theorem. The Nielsen class is the set of orbits of under simultaneous conjugation. Hyperbolic angles in the Poincaré disk are defined through the hyperbolic law of cosines.
The geometric statements Lemma 3.3 and Proposition 3.5 concern the numerically computed curve and the polynomial , which the paper does not print, so they are not milestones. Lemma 3.1 enters only through its Riemann–Hurwitz count.
Contributions are welcome on decidable certificates for permutation-group facts in Lean, on Galois-group certification for explicit polynomials, and on Hilbert irreducibility.
Many queues observed at well-chosen instants are Markov chains on the nonnegative integers. For the single-server queue with Poisson arrivals and general service times (M/G/1), D. G. Kendall showed in 1951 that the number of customers left behind at successive departure epochs is such a chain, the imbedded Markov chain (Kendall 1951; Kendall 1953). Whether the queue settles into a steady state, keeps returning to empty without settling, or grows without bound is then a question about this chain: is it ergodic, null recurrent, or transient?
F. G. Foster's 1953 paper (doi:10.1214/aoms/1177728976) answers this question by first proving general criteria for an irreducible chain on , stated as solvability conditions for linear inequalities in the transition matrix, and then applying them to the M/G/1 and GI/M/1 chains. Theorem 2 of the paper is the drift condition now known as Foster's criterion, the starting point of the Lyapunov-function method for the stability of queues and stochastic networks (Meyn and Tweedie 2009). This mission is the M/G/1 half of the paper.
Timeline:
A Markov chain on the states is given by a transition matrix : and for every row . Write for the probability that the chain started in first reaches (for , first returns to ) at step . The chain is irreducible if every state can be reached from every other, and aperiodic if for every state the return times have greatest common divisor . A state is recurrent if and transient if ; a recurrent state is ergodic (positive recurrent, "recurrent-nonnull") if in addition its mean recurrence time is finite. The mean first-passage time from to is .
The M/G/1 matrix is built from a sequence of positive numbers summing to one ( is the probability of arrivals during one service):
that is, and, for , when and otherwise. The traffic intensity is
the mean number of arrivals per service.
The goal leaves arbitrary apart from positivity and normalization; in particular is allowed and falls in the transient case.
The result. The classification is the stability theorem for the M/G/1 queue: for the departure-epoch queue length has a stationary distribution, which is what the Pollaczek–Khinchine formula describes; for the queue empties infinitely often but has no steady state; for it grows without bound. The general criteria behind it (Theorems 2, 4, 5) apply to any chain on the nonnegative integers and are reused in the companion GI/M/1 mission and throughout queueing and Markov-chain stability theory.
Formalizing it. All results here are proved on paper (Kendall and Foster, 1951–1953, with Theorems 3 and 7 classical lemmas from Feller). None of them is known to have a machine-checked proof against a Lean development of countable-state Markov chains. The mission produces such proofs on the published discrete-chain vocabulary (transition matrices, first-passage probabilities, return probabilities, positive recurrence), together with the general Foster criteria as reusable theorems. Theorem 2 is already posed as an open platform theorem and is reused here.
The queue-specific part of the argument is short once the general criteria are available; the weight of the mission is in those criteria. They relate qualitative properties of an infinite chain (ergodicity, recurrence, transience) to solvability of infinite systems of linear inequalities, and this needs limit behaviour of the -step probabilities and of hitting probabilities of state , none of which follows from finite-state arguments. Two further points resist the naive approach. The converse directions (ergodic , recurrent ) need exact identities for mean first-passage times, not just bounds, and these must be handled in because the means may be infinite. And the boundary case (null recurrence) separates the two equivalences: an argument that only compares the mean drift with , such as a law of large numbers for the increments, cannot tell recurrence from transience there.
QueueingFundamentals.Foundations.TransitionMatrix (entries P.p i j, rows summing to as a HasSum), with its firstPassage, returnProb, Irreducible, Aperiodic and PositiveRecurrent. "Ergodic" is P.PositiveRecurrent; aperiodicity is the paper's standing assumption and is not folded into it a second time.i ≠ 0.mg1Matrix k : ℕ → ℕ → ℝ; the goal and the §3 display quantify over every TransitionMatrix P with P.p = mg1Matrix k. Such a P exists for every admissible k (checked in a sorry-free local file for ).Summable or HasSum); Theorem 3's equation (6) is written as in together with finiteness of the , .Ruled out: as a real tsum (which is for a divergent series and would call a heavy-tailed chain ergodic); defining "ergodic" or "recurrent" through the existence of Lyapunov or drift functions (which would make the criteria tautological); a goal over a matrix that need not exist.
Contributions welcome: proofs of the general criteria (Theorems 2–5) on the published chain vocabulary, the limit theorem for irreducible aperiodic chains, first-step analysis for hitting times, and Theorem 7 as a lemma on probability generating functions; all of these are reusable beyond this mission.
Temporal-difference (TD) learning estimates the value function of a Markov chain — the expected discounted sum of future rewards from each state — from a single stream of observed transitions, without knowing the transition probabilities. With a linear function approximator the value of state is represented as for a feature vector and a parameter . Classical TD() updates by stochastic approximation, and its behaviour depends on a step-size schedule that must be tuned.
Bradtke and Barto (Machine Learning 22, 1996) replaced the stochastic-approximation update by a least-squares solve: LS TD (Eq. (11)) recomputes at every step as the instrumental-variable least-squares solution of the empirical consistency condition. The method, later generalized as LSTD() by Boyan (Machine Learning 49, 2002), is the basis of least-squares policy iteration and of the "LSTD" methods in standard reinforcement-learning texts (Sutton and Barto, Reinforcement Learning, 2nd ed., 2018, §9.8). Its appeal is that it has no step size; the question this mission formalizes is whether it nonetheless converges, with probability one, to the true parameter.
Timeline. Sutton (1988) introduced TD(). Watkins and Dayan (1992) and Tsitsiklis (1994) proved probability-one convergence of tabular TD(0) and Q-learning. Bradtke and Barto (1996) proved probability-one convergence of LS TD on absorbing chains (Theorem 1) and on ergodic chains (Theorem 2). Tsitsiklis and Van Roy (IEEE TAC 42, 1997) proved convergence of linear TD() with general features on ergodic chains.
A finite Markov chain on a finite nonempty set is a matrix with and . A transition earns reward ; the expected reward out of is . For a discount factor the value function is
The chain is ergodic (Kemeny and Snell) if every state can be reached from every state: for all there is with . An invariant distribution is a probability vector with ; write .
Each state has a feature vector ; is the matrix with rows . The true parameter is a vector with for all .
The algorithm (Figure 3) starts at an arbitrary state , lets the chain move , and after transitions computes
the sums running over the transitions observed so far.
If is ergodic, (1) is linearly independent, (2) each has dimension , and (3) , then is finite and, from any initial law,
The goal leaves the chain, the rewards, the features and the initial law arbitrary.
The result. Theorem 2 shows that an LS TD learner running on one long trajectory recovers the exact value function whenever the features can represent every function on the states, with no step-size schedule. It is the step-size-free counterpart of the tabular TD(0) convergence theorems and the starting point for the later analysis of LSTD with fewer features than states, where the limit is the TD fixed point rather than . Lemma 5 is the general identification of that fixed point as the almost-sure limit of LSTD.
Formalizing it. The result is proved in the paper; it has not been machine-checked. A formalization adds three things the paper delegates: the strong law of large numbers for occupation times of a finite irreducible Markov chain, which the paper cites to Kemeny and Snell and which is not in Mathlib; the per-state transition frequencies used in the first sentence of the proof of Lemma 5; and the linear algebra of the limit. The first is reusable well beyond reinforcement learning.
The algebra is short once the empirical averages in (11) are known to converge. The difficulty is probabilistic: the averages are over a dependent sequence, so the ordinary strong law of large numbers does not apply. Two facts are needed: that the fraction of time in each state converges to almost surely for any starting law, including periodic chains, where itself does not converge; and that, among the visits to , the fraction followed by a move to converges to , which needs the strong Markov property at successive visit times. Neither follows from convergence of the chain's distribution, and neither holds for a chain started at a fixed state without an argument that every state is reached.
X with Fintype, DecidableEq, Nonempty, a row-stochastic matrix P : Matrix X X ℝ (structure Chain), rewards R : X → X → ℝ, features φ : X → Fin m → ℝ. Condition (2) is m = Fintype.card X; condition (1) is LinearIndependent ℝ φ.tsum is on a divergent series, so "θ* is finite" is stated as convergence of the series together with existence of with . is existential, never defined as Lemma 5's limit.Needed infrastructure: the strong law for occupation times of a finite irreducible chain under an arbitrary initial law (milestone 1), the strong Markov property at visit times, positivity of the invariant distribution of an irreducible chain, and the invertibility of for . Contributions to any of these, as standalone lemmas, are welcome.
A supplier who sells to a retailer at a per-unit wholesale price above her own production cost induces the retailer to order less than an integrated firm would. This effect, double marginalization, goes back to Spengler (1950) and is the standard benchmark against which supply chain contracts are judged: a contract coordinates the channel if it makes the decentralized decisions coincide with the integrated optimum. Revenue-sharing contracts, as used in the video-rental industry, coordinate the channel; the plain wholesale-price contract does not. Whether a supplier should bother with the administrative cost of revenue sharing depends on how much the wholesale-price contract actually loses and how much of the remaining profit the supplier keeps.
Cachon and Lariviere answer that question for a retailer whose revenue depends only on the quantity ordered, in Section 4.1.1 of their working paper Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations (June 2000; the 2005 Management Science version renumbers and revises the material). They show that the answer is governed by the curvature of the marginal revenue curve, and they compute it exactly for a one-parameter family. The source is the June 2000 working paper, whose results are unnumbered; every item cites its section, page and display.
A supplier produces at unit cost and sells to a single retailer. The retailer's expected revenue from units is , where , is strictly concave and differentiable on with derivative (the marginal revenue), is differentiable on with derivative , the product is viable (), and a finite quantity is optimal ( for some ). The supply chain profit is ; the integrated quantity maximizes over .
Under a wholesale-price contract with price , the retailer orders to maximize . Each order is induced by exactly one price, , so the supplier can be thought of as choosing . Her profit, the retailer's profit, and their sum are then
Following the paper, is assumed decreasing, which makes unimodal. The supplier's optimal quantity to induce maximizes over , and is her optimal wholesale price. The efficiency of the contract and the supplier's profit share are
In the α-family, for and , so : marginal revenue is convex for , linear for and concave for .
For and , the quantities and are the unique maximizers of and on , the profit share is , and
a quantity that does not depend on , is strictly increasing in , tends to as and to as .
The general milestones turn the paper's area argument (the triangle under the tangent to marginal revenue at ) into three comparisons: convex marginal revenue makes the wholesale-price contract worse for the chain and leaves the supplier at most two thirds of a smaller pie, concave marginal revenue the opposite. The α-family makes the trade-off exact: efficiency never falls below , while the supplier's share moves much faster than efficiency, which is the paper's argument for why revenue sharing is most attractive when marginal revenue is convex.
These results are proved on paper but, to our knowledge, not machine-checked anywhere; Mathlib has no supply chain contract theory. The formalization provides a reusable single-retailer wholesale-price model, a checked version of the convex/concave tangent comparisons, and a corrected statement of the α-family's monotonicity (see the scope section).
The general comparisons are short on paper but rest on a picture: they need the first-order condition at an interior maximizer, the tangent-line inequality for a convex or concave derivative, and the fundamental theorem of calculus for a function whose derivative is known only on a half-line and one-sided at . Strictness needs a strictly positive integrand on a nondegenerate interval.
The α-family is where the analysis is not routine. The closed forms involve real powers with exponents and , which must be combined carefully. The limit as is classical, but the monotonicity of on all of is not a one-line derivative sign check: the derivative mixes with rational terms, and its sign has to be established uniformly near and near .
Quantities and prices are real numbers. "Optimal" always means a maximizer over all admissible quantities (IsMaxOn on , or on in the α-family, as the page restricts), never a root of a first-order condition. The derivative of the general model is linked to by a one-sided derivative hypothesis on ; is required only on , since for it blows up at . In the α-family the marginal revenue is deriv of , not a separate function, and is assumed (implicit on the page: and ). Efficiency and profit share are real divisions; their denominators are positive at the optimal quantities.
Deviations from the page, all disclosed in the items:
A trivializing formalization is ruled out: the efficiency in the goal is the ratio of profits computed from at the maximizers, not a definition equal to , and the maximizers are characterized as unique argmaxes rather than assumed.
Welcome contributions: proofs of the general tangent comparisons, which are reusable for any concave revenue model; the real-analysis lemmas on ; and the α-family closed forms.
A revenue-sharing contract lets a supplier charge a retailer a wholesale price per unit and, in addition, collect the share of the retailer's revenue. The video-rental industry adopted such contracts at scale in the late 1990s, and Cachon and Lariviere showed that in a broad class of models they coordinate the supply chain: the retailer's privately optimal decisions coincide with those that maximize total channel profit, and the profit can be split arbitrarily between the firms (missions 1 and 2 of this series).
The same authors also studied where revenue sharing breaks down. The most practically relevant limitation is retailer effort: shelf space, service, store cleanliness and promotion raise demand, cost the retailer money, and cannot be written into a contract. Once the retailer gives away part of its revenue, it earns only a share of the return on its effort while still paying the whole cost. This mission formalizes Section 4.2 of the authors' working paper, which shows that revenue sharing then cannot coordinate the channel while leaving the supplier any profit, and, in an explicit linear-demand example, determines exactly when the supplier is better off with the plain wholesale-price contract.
The source is the June 2000 working paper (Cachon and Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations), whose results are displayed claims inside numbered sections rather than numbered theorems; the milestones cite section, printed page and display. The published version appeared in Management Science 51(1), 2005.
General model (Sec. 4.2.1). A supplier produces at unit cost . The retailer chooses an order quantity and an effort level after observing the contract . Expected revenue is continuous, differentiable, strictly increasing in and concave in ; effort costs the retailer , where is continuous, increasing, differentiable and convex with . The profits of the integrated channel, the retailer and the supplier are
The integrated solution maximizes over .
Linear example (Sec. 4.2.2). Inverse demand is with an effort-impact parameter , revenue is and effort costs . For a share the supplier's profit when the retailer responds optimally to is , and the supplier's optimal profit is
The share is the wholesale-price contract.
For , and every , the supremum defining is attained at the price , and
Consequently is strictly increasing on if (the wholesale-price contract is the supplier's unique best share), constant if , and strictly decreasing if , with as .
The general result (milestones 1–2) is a clean impossibility statement: with non-contractible effort, the only contract in the revenue-sharing family that coordinates the channel is the wholesale-price contract at marginal cost, which leaves the supplier zero profit. It marks the boundary of the coordination results of the earlier sections, and contrasts with the price-dependent newsvendor, where revenue sharing does coordinate price and quantity because the cost of expanding demand is captured in the revenue function and shared by both firms.
The example turns the impossibility into a design rule. Because coordination is out of reach, the supplier compares contracts by her own profit, and the threshold separates two regimes: when effort matters a lot she should leave the retailer all revenue and charge only a wholesale price ("a smaller share of a larger pie"); when it matters little she should take as much revenue as possible. The same threshold governs the counterintuitive comparative static that the integrated channel's retail price falls as production cost rises.
All results are proved on paper in the source. None has a machine-checked proof; this mission produces the first. The example is a fully explicit two-stage optimization problem, so the formal development also yields a verified computation of a Stackelberg equilibrium with moral hazard that other contract-design missions can reuse.
The individual calculations are elementary, and the work lies in getting the optimization statements right. The page solves the retailer's problem sequentially (effort first, then quantity) and writes the supplier's objective by substituting closed forms. A faithful proof must instead show that these closed forms are global optima over the constrained domains: the retailer optimizes jointly over the quadrant , the corner is optimal whenever , and the supplier's objective is a quadratic on glued to the zero function on , which is not concave on all of . The first-order-condition argument of the general model similarly needs an interior integrated optimum and a strictly positive marginal effect of effort, which "strictly increasing in " alone does not provide.
All quantities are real numbers. The general model is a structure RevShareCoord.Effort.Model carrying , its partial derivatives, , and ; derivatives are one-sided within , and joint differentiability of is replaced by its partial derivatives and joint continuity. The example lives in RevShareCoord.Effort.Linear. "Optimal" always means a maximizer over the whole admissible set ( for the retailer, for the supplier), and the supplier's value is defined as the supremum of her attainable profits, not by the printed formula.
Deviations from the page, each disclosed in the item's Formalization Note:
Plugging the printed into and comparing across would turn the dichotomy into a statement about an arbitrary price schedule; the goal instead asserts that attains the supremum over all , with the retailer best-responding jointly in .
No external library beyond Mathlib's real analysis and convexity is needed. Contributions welcome: proofs of the milestones, reusable lemmas on maximizing strictly concave quadratics over orthants, and a generalization of milestone 2 to non-interior optima.
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.