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 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?
Chapter 5 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), asks what happens to PAC learning when the labels are unreliable. In the classification noise model of Angluin and Laird, each label returned by the oracle is flipped independently with a fixed probability . The algorithms of Chapter 1 collapse at once: the elimination algorithm deletes a correct literal on the strength of a single mislabeled example, and the tightest-fit rectangle may not exist. The chapter's remedy is to learn from statistics: an algorithm that forms its hypothesis only from estimates of probabilities of simple events is insensitive to occasional wrong labels. Kearns's statistical query model makes this precise, replacing the example oracle by an oracle that returns the probability of any predicate of a labeled example to within a tolerance, and the main theorem (5.3) shows that every class learnable from statistical queries is PAC learnable in the presence of classification noise. The proof rests on a single identity, Equation (5.2), that expresses the true value of a statistical query in terms of three quantities that can each be estimated from noisy examples, and on the observation that a hypothesis's disagreement with the noisy label is an affine function of its true error, which lets the best of several candidate hypotheses be recognized without clean data.
The framework is that of Mission I. The noisy example law is that of with and flipped with probability . A statistical query is a predicate of a labeled example with value . The inputs split into , where the label matters to , and , where it does not; and is conditioned on . For conjunctions over , is the probability that a literal is set to and the probability that it is on a positive example; is significant if and harmful if .
For and every statistical query ,
the probabilities on the right being taken under the noisy oracle.
The §5.2 analysis behind Theorem 5.2 (the conjunction of all significant, non-harmful literals has error at most ); the product estimate bound of p. 115 (); the identity of p. 117 ().
Equation (5.2) is the entire mechanism of noise-tolerant learning in the statistical query model: the noisy oracle cannot be de-noised example by example, but the probability of any predicate can be recovered exactly from noisy probabilities, because on the inputs where the label matters the noise acts as a known affine contraction and on the others it acts not at all. Together with the p. 117 identity, which turns hypothesis selection into a comparison of noisy disagreement rates, and the Chernoff bounds of Mission IV, it yields Theorem 5.3 and hence noise-tolerant algorithms for every class the book has learned so far (conjunctions, decision lists, -CNF). The §5.2 analysis is the first statistical-query algorithm and shows the pattern: a hypothesis defined by thresholds on a few probabilities, with enough slack between the thresholds that estimates suffice. None of this is machine-checked. The formalization fixes the noisy example law on the platform's sample framework and proves the exact identities on which the noise-tolerant simulation depends.
Equation (5.2) is a computation with the pushforward of a product measure: one must express the noisy law on as a mixture of the clean law and its label-flipped image, solve the affine relation for the clean probability, and combine with the restriction to , where the flipped and unflipped labels give the same value of ; the degenerate case , in which the conditional measure is zero and the first term vanishes, must be handled separately. The p. 117 identity is the same computation without the split. The §5.2 analysis is two union bounds over the literals after the observation that a literal of the target is never harmful and that a literal of the hypothesis is never insignificant. The product lemma is elementary arithmetic with a case split at .
The noisy oracle is a measure on labeled examples obtained by mapping the product of and a Bernoulli() coin; the conditional is Mathlib's conditional measure; queries are arbitrary measurable predicates of a labeled example, with no tolerance or query-count bookkeeping. Theorem 5.3 itself, the definitions of efficient learnability from statistical queries (Definition 14) and of efficient noisy PAC learnability (Definition 13), Theorem 5.1, Theorem 5.2 as a statement about an algorithm with oracle access, and Corollary 5.4 are not stated: they quantify over query algorithms and their running times, for which this series has no model; the mission carries their exact probabilistic content. The error-propagation analysis of §5.4.2–5.4.3 with tolerance and the guessing resolution is not stated beyond the product lemma, since the factor is not in and the book's constant does not account for it. Hypotheses: for the decomposition, for the disagreement identity, for the conjunction analysis, all reals in for the product lemma.
Trivializing readings are excluded: the decomposition is an exact identity for every measurable query, and the conjunction bound is for the exact thresholds with the union bound's . Welcome contributions: the mixture representation of the noisy law, the restriction of a pushforward to , and the two union bounds.
Chapter 4 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), asks whether the PAC model's demand for arbitrarily small error and confidence is essential. A weak learning algorithm need only, with some fixed positive probability, output a hypothesis that beats random guessing by a fixed margin. Schapire's theorem, the chapter's main result, says that this apparently much weaker requirement is equivalent to the original one: any weak learner can be converted, by running it on carefully filtered distributions and combining its hypotheses by majority votes, into a strong learner. The construction is boosting, which became one of the most influential ideas in machine learning. The chapter proves the equivalence in two steps. Boosting the confidence is elementary: run the learner several times and validate. Boosting the accuracy is the substance: a modest procedure that combines three hypotheses, each with error at most on its own distribution, into a majority with error at most , applied recursively until the error is driven below the target. The Chernoff bounds of the Appendix, the book's workhorse for estimating probabilities from samples, are what makes the validation steps rigorous.
The framework is that of Mission I. A class is weakly learnable using if for some advantage , confidence and sample size , an algorithm outputs hypotheses in that, for every target in and every distribution, have error at most with probability at least ; the algorithm's prediction is a measurable function of the sample and the instance together, as it is for every algorithm. Given a hypothesis , the filtered distribution gives weight to the instances on which errs and to those on which it is correct, preserving relative weights within each part, and is conditioned on ; the modest procedure outputs . Ternary majority trees over are the closure of under the majority of three. For confidence boosting, independent samples yield hypotheses, and a fresh sample selects the one with the fewest mistakes. Bernoulli trials are independent coin flips with success probability .
If is weakly PAC learnable using measurable hypotheses in , then is PAC learnable using the class of ternary majority trees with leaves from : for all some sample size and some algorithm outputting majority trees achieve error at most with probability at least , for every target in and every distribution.
Theorem 9.2 (the additive and multiplicative Chernoff bounds); the two facts of §4.2 behind confidence boosting (independent runs all fail with probability at most ; the fewest-mistakes selection loses at most with probability at least ); Lemma 4.1 (the modest procedure: error at most ).
Theorem 4.9 is one of the landmark results of learning theory: it shows that the PAC model has no intermediate strength, that Occam learning, weak learning and strong learning coincide, and that the resources of a strong learner can be bounded polylogarithmically in in memory and hypothesis size. Its constructive proof is the first boosting algorithm, ancestor of AdaBoost and of gradient boosting. Lemma 4.1 is the analytic core, a clean inequality about three hypotheses and three distributions in which the filtered distribution is exactly calibrated so that has no advantage on it. The Chernoff bounds are the concentration inequalities invoked throughout the book, and their formalization on the product law of Bernoulli trials makes every later "estimate to within with confidence " step reusable. None of these is machine-checked in this form; the boosting theorem in the sample-complexity sense is, to our knowledge, not formalized anywhere.
Lemma 4.1 is a computation with conditional measures: writing of the majority as the weight of the instances on which and both err plus times the weight of their disagreement, mapping weights under back to by the factors and (Equation (4.1)), and maximizing the resulting polynomial in ; the degenerate cases where a conditioning event is null must be handled separately. The Chernoff bounds require the exponential moment method on a finite product measure. The confidence-boosting facts are the product bound for independent blocks and Hoeffding plus a union bound. The goal is a genuine construction: from a large sample of one must simulate the recursive algorithm Strong-Learn, whose calls to the weak learner on filtered distributions are served by rejection sampling from the remaining examples, bound the depth of the recursion by the growth of iterates (Lemma 4.2), bound the number of examples consumed at each node (Lemmas 4.3–4.7) and allocate the confidence over all the places the simulation can fail; then package the result as a deterministic function of a sample of fixed size. An alternative route is available: weak learnability with a fixed sample size forces a finite VC dimension (a class shattering a large set defeats any fixed-size learner on the uniform distribution over it), after which Theorem 3.3 gives a consistent strong learner; but its hypotheses lie in , not in the majority trees over , so it does not prove the stated conclusion.
The weak-learning hypothesis is the book's with constants in place of the inverse polynomials, which is what the definition says for a fixed class; hypotheses in are required to be measurable, and the weak learner jointly measurable in the sample and the instance, because Strong-Learn runs it on distributions filtered through its own earlier outputs and the analysis integrates over the earlier samples (for an arbitrary function the combined failure event need not be measurable, and outer-measure bounds on separate runs do not combine); the conclusion is the book's hypothesis class, the majority trees over , built as an inductive predicate. Filtered distributions use Mathlib's conditional measure, so that a null conditioning event yields the zero measure; Lemma 4.1 is stated for and holds in those degenerate cases too. The confidence-boosting milestone states the two probabilistic facts rather than the composite algorithm, whose sample indexing across runs and validation is bookkeeping; the selection rule is any rule minimizing mistakes. Chernoff's bounds are stated with non-strict inequalities in the events, for and . Running time, the recursion-depth and sample-size lemmas with unspecified constants (4.2–4.8), and Exercises 4.1–4.3 are not stated.
Trivializing readings are excluded: the weak-learning guarantee is uniform over all targets and distributions with an advantage strictly positive, the strong conclusion is for every , and Lemma 4.1 requires all three error bounds on their respective distributions. Welcome contributions: Lemma 4.1 itself, the Hoeffding bound on the product law, and the rejection-sampling lemma that turns a sample of into a sample of a filtered distribution.
The bandit processes that motivated the index theorem are sampling processes: an arm is a population from which one draws i.i.d. observations whose distribution has an unknown parameter, and each draw both earns something and teaches something. Chapter 7 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), develops the theory of such processes in the Bayesian setting: the state of the process is the current posterior for the parameter, continuing it samples the next value from the predictive distribution and moves to the new posterior. When the observations are themselves the rewards one has a reward process, the classical Bayesian multi-armed bandit; when the aim is to find as quickly as possible an individual whose measurement reaches a target (a compound active enough to warrant further testing, in the drug-screening problem from which the index theorem came) one has a target process, which is a job that completes when the target is reached. Two questions organize the chapter. When can the index be written down without any optimization, and when do symmetries of the model reduce the index to a function of fewer variables? The first is answered by the notion of a favourable prior (Section 7.3): if no run of observations below the target can raise the current probability of success, then the index is that probability, exactly, by Proposition 2.7. The second is answered by the invariance theorems of Section 7.4: a location parameter with a conjugate prior gives , a scale parameter gives , and for target processes the target can be absorbed into the state, . These identities are what make the tables of Chapter 8 one-dimensional.
A sampling model consists of a likelihood , a family of priors on the parameter indexed by the parameters of a conjugate family, and the Bayes update of those parameters after observing ; the family is conjugate if the posterior of given is . The predictive distribution is . The reward process moves from to with and earns . The target process with target moves to the completion state if and to otherwise, earning the current probability of success , and in . A state is favourable if for every finite sequence of observations . For the invariance theorems the parameters are with the update ; is a location parameter of the likelihood if is shifted by , and is a location parameter of the prior family if is shifted by ; scale parameters are defined with , . The Gittins index is that of the Bandit Algorithms model on these chains.
If is a location parameter of a reward process with a conjugate prior family in which is a location parameter and the parameters update as the sample mean and count, then for every
under the standing assumptions that the observations have a mean and the discounted rewards of the chain are integrable.
Proposition 7.4 (favourable state: ); Example 7.5 (Bernoulli target process, ); Example 7.6 (normal target process with known variance, for ); Theorem 7.11 (scale parameter: ); Theorem 7.17 (target process with a location parameter: ).
Theorem 7.9 and its companions are the reason the Gittins index of the normal reward process is tabulated as a function of alone and that of the exponential process as a function of and one ratio; every computational method of Chapter 8 starts by reducing the state space with them. Proposition 7.4 is the source of every closed-form index in the book: it identifies the states in which sampling for information is worthless, so that the index collapses to the immediate expected reward, and Examples 7.5 and 7.6 show that for the Bernoulli target process this is every state and for the normal target process every state with a nonnegative posterior mean. The formalization gives the platform its first Bayesian sampling-process model, in which the state is a posterior and conjugacy is stated through the posterior kernel of the likelihood, and its first index identities on unbounded-reward chains, which is where the integrability assumptions of the Bandit Algorithms model do real work.
None of this is machine-checked. The invariance theorems are stated in the proper-prior form of the corollaries, with the model's symmetry as hypotheses, so that they apply to any conjugate family with the stated structure rather than to a particular density.
The invariance theorems require showing that the chain of parameters from the shifted (scaled) state is the image of the chain from the original state under the shift (scaling) of trajectories, which is an equivariance of the Ionescu–Tulcea construction with respect to a measurable bijection commuting with the kernel; that stopping times are carried to stopping times; that the discounted reward of a stopping time shifts by times the discounted time; and that the supremum of a nonempty bounded set of reals shifts and scales accordingly. Boundedness of the set of ratios is where the integrability assumption enters. Proposition 7.4 is the chain-level statement that all rewards along every trajectory from a favourable state are at most , which needs an induction on the trajectory law of the target chain, followed by the argument of Proposition 2.7. Example 7.6 needs the monotonicity of in the observations below the target, a small inequality, plus the Gaussian probability of a half-line as the current probability of success; Example 7.5 needs only that decreases.
The sampling model is a structure with Markov likelihood and prior kernels and a jointly measurable update; the predictive distribution is the kernel composition; conjugacy is an almost-everywhere identity between Mathlib's posterior of the likelihood with respect to the prior and the prior at the updated parameters, and is carried as a hypothesis of the invariance theorems and of Proposition 7.4 so that their subject is the Bayesian process. For the parameters it is required on only (IsConjugateOn): a proper prior has , and conjugacy at every is impossible with a location parameter, since at the update divides by zero and sends every observation to one state, which made the first draft's location theorems vacuous. The chains are built with Kernel.map of product kernels, so their measurability is structural, and the target process lives on P ⊕ Unit with the completion state absorbing. The book's improper priors are replaced by proper conjugate families with the location or scale structure of Corollaries 7.10 and 7.12, as those corollaries do; the discrete-time correction factor of Section 2.8 is not applied since it cancels in every identity stated. The two examples are built directly from a uniform or Gaussian seed with the transition probabilities the book computes (the beta and normal posterior computations of Exercise 7.1 are not formalized). Hypotheses: ; integrable observations and L&S Assumption 35.6 for the reward processes; for the invariance theorems and for the scale theorem; ; and for the normal example.
Trivializing readings are excluded: the indices are the genuine suprema of the Bandit Algorithms definition with integrable rewards, the update rule is the book's and not a free parameter, and the favourability condition ranges over all finite observation sequences. Welcome contributions: the equivariance of the trajectory measure under a state bijection commuting with the kernel, the transport of stopping times, and the reward bound along the target chain from a favourable state.
Every proof of the index theorem in Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), uses the fact that a bandit not being processed is frozen. Chapter 6 drops that: Whittle's restless bandits evolve under the passive action too, by a different law, and of must be active at every time. The problem is PSPACE-hard in general, so Whittle proposed a heuristic built from a Lagrangian relaxation: replace the hard constraint by a subsidy paid whenever a bandit is passive, solve the resulting single-bandit average-reward problem, and read off, for each state, the least subsidy at which the passive action becomes optimal. When the set of states where passivity is optimal grows monotonically with , the bandit is indexable and is its Whittle index; the Whittle index policy activates the bandits of largest index. It reduces to the Gittins index policy when the passive action freezes, it is asymptotically optimal as grows under a fluid-stability condition (Weber and Weiss), and it has become the standard heuristic for sensor management, opportunistic channel access, maintenance and queueing control. The price is that indexability must be established model by model. Section 6.5 shows how easy this is when the single-bandit problem is solved by a monotone policy, on two bi-directional models: the spinning plates asset, which improves under investment and deteriorates when neglected, and the vigour bandit of Whittle's Ehrenfest project, which tires when worked and recovers when rested.
A restless bandit is a Markov decision process with two actions, active () and passive (), each with its own transition kernel and reward. Under a deterministic stationary Markov policy with passive subsidy the reward in state is , and the average reward from is the Cesàro limit of the expected rewards. The optimal average reward is the supremum over such policies and initial states; a policy is optimal if it attains from every initial state; is the set of states in which some optimal policy is passive; the bandit is indexable if is nondecreasing in ; and .
The spinning plates asset lives on : active moves at rate , passive moves at rate , , and is earned under both actions, increasing. Uniformized so that rates are at most one, it is a discrete-time bandit whose kernels move with the rate's probability and otherwise stay. The monotone policy is passive exactly on ; under it the asset alternates between and , spending the fraction of its time at , so its average reward is with , and . The vigour bandit is the mirror image: active moves down at rate and earns , passive moves up at rate and earns nothing, , and .
For the spinning plates asset: (i) if is strictly decreasing over the thresholds , the asset is indexable; (ii) if additionally is strictly decreasing over the states, the Whittle index is
Eqs. (6.9)–(6.10): the monotone policy earns from every initial state and , because a monotone policy always achieves ; Theorem 6.5, the same two statements for the vigour bandit with increasing and increasing.
Theorem 6.4 is the chapter's template for proving indexability: the single-bandit value is the upper envelope of finitely many lines whose slopes decrease in the threshold, so the optimal threshold moves monotonically with the subsidy and the hinge points of the envelope are the indices. The same argument gives Theorem 6.5, the admission-control indices of Section 6.7, and the marginal productivity indices of Niño-Mora; it is the reason Whittle indices are computable in closed form for bi-directional models. Its formalization establishes, on the platform, the first restless-bandit model with a proved index, and the general notions of passive set, indexability and Whittle index that every later restless-bandit statement will use.
None of this is machine-checked. The average-reward optimality notion is stated without the DP equation (6.6), through optimality from every initial state, which is what the equation's solution encodes on a finite state space and avoids the relative value function altogether.
The proof in the book is two paragraphs, but it stands on the reduction to monotone policies, which is only sketched: every deterministic stationary policy, from every initial state, drives the asset into an absorbing endpoint or a two-state cycle whose average reward is that of the monotone policy , so no policy beats the best monotone one and the passive set under an optimal-from-everywhere policy is exactly for the smallest maximizing threshold. Formalizing this needs the average reward of a finite Markov chain as a limit determined by the stationary distribution of the recurrent class reached, for the two-point kernels of the model, and a case analysis of policies as -strings. The envelope argument then needs that the smallest maximizer of is nonincreasing in when is strictly decreasing, and that with strictly decreasing the maximizer is exactly when . Theorem 6.5 is the same with the roles of up and down exchanged. Nothing in Mathlib computes Cesàro limits of finite Markov chains.
Restless bandits are the two-action DecisionProcesses of the superprocess module; average reward is a real limsup of Cesàro means of Bochner integrals over the chain law of the Bandit Algorithms model under the stationary kernel; the optimal average reward is a supremum over the finite type of deterministic stationary Markov policies and the finite state space, bounded by the reward bound. Both models are on Fin k with the book's states shifted down by one, kernels driftKernel p f that move to f x with probability p x, and the boundary conventions of and (the book's "convenient positive values") replaced by their values and at the two extreme thresholds; the model assumptions , , rates in , and increasing and nonnegative are hypotheses. Theorem 6.5's "increasing" is read as strictly increasing, as in Theorem 6.4, since a nonstrict admits zero interior rates for which the monotone reduction fails. The milestone (6.9) requires and positive interior rates, which Theorem 6.4's hypothesis (i) implies.
Trivializing readings are excluded: indexability is monotonicity of the passive set over all real subsidies, the passive set is defined through policies optimal from every initial state, and the index identity is for every state. Welcome contributions: the average reward of a two-state cycle, the reduction of an arbitrary -policy to a monotone one, and the envelope lemma for lines with decreasing slopes.
Chapter 5 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), presents the achievable region methodology of Tsoucas, Bertsimas and Niño-Mora, Glazebrook and Garbe, and Dacre, Glazebrook and Niño-Mora: instead of arguing about policies, one argues about the set of performance vectors they can produce. For a multi-armed bandit the natural performance of a policy is the vector of discounted numbers of times each state is continued; the expected return is linear in it; and the set of achievable performances turns out to be a polytope cut out by conservation laws, one inequality per subset of states, with equality exactly for the priority policies that put that subset last. Optimizing a linear objective over a polytope is a linear program, its dual is solved by an adaptive greedy algorithm, and the primal solution is the performance of a priority policy whose priorities are the algorithm's outputs, the Gittins indices. This gives yet another proof of the index theorem (Section 5.3) and, more importantly, a definition, generalized conservation laws (Section 5.4), of the class of systems for which the same argument works: branching bandits, multi-class queues, job scheduling with discounted rewards, systems with imposed priority classes. The chapter's main result, Theorem 5.5, is the statement that every such system is solved by an index policy.
There are job types . A policy has a performance , a vector of expectations; a permutation of defines the permutation policy giving highest and lowest priority, and is the set of the lowest-priority types. The system satisfies GCL(1) if there are a base function and a matrix , positive on and zero off it, such that for every policy
with equality in the first for every permutation policy whose lowest-priority types are . GCL(2) reverses the inequality. The adaptive greedy algorithm picks maximizing , sets to the maximum, removes , and repeats with the adjusted rewards divided by ; its outputs are the order , the dual variables and the indices .
For the SFABP of Section 5.3, identical bandit processes on with kernel and discount factor in the model of the Bandit Algorithms series, is the discounted number of continuations of a bandit in state , is the discounted return time to from , and is the minimal cost , namely with the number of continuations needed to bring every bandit into .
For a GCL(1) system whose achievable region is convex, and any reward vector : the achievable region is the polytope
its extreme points are performances of permutation policies; has an output; and for every output the permutation policy in the order it finds, the Gittins index policy, maximizes over all policies.
Lemma 5.1 (the SFABP satisfies the conservation laws, with equality for policies giving priority to states outside ); the identification on p. 123 of the adaptive greedy indices of a SFABP with the Gittins indices, together with their monotonicity along the order found; Theorem 5.10, the GCL(2) counterpart of the goal for cost minimization.
Theorem 5.5 is the index theorem in its most general form of this kind: it says nothing about Markov chains, only that performances are expectations, objectives are linear and conservation laws hold, and it delivers both the optimal policy and the algorithm that computes its priorities in polynomial time in the number of job types. It is the theorem behind the index results for branching bandits and Klimov's multi-class queue and behind the suboptimality bounds of Sections 5.5 and 5.7, all of which are calculations on the polytope. Lemma 5.1 and the p. 123 identification are what tie the abstract theorem to the Gittins index: they show that the multi-armed bandit is a GCL(1) system and that the priorities the algorithm produces are the same indices as Chapters 2 to 4 define through stopping times.
None of these is machine-checked. Formalizing Theorem 5.5 puts an LP-duality index theorem on the platform in a form any system can instantiate by verifying its conservation laws; formalizing Lemma 5.1 relates the Bandit Algorithms run law to the single-chain return times, which is the first conservation law on that model; and the p. 123 theorem gives an algorithmic characterization of the Gittins index on finite chains, distinct from the restart and largest-remaining-index characterizations of Chapter 2.
The goal's optimality clause is weak LP duality once one shows that the greedy dual variables are nonpositive except and satisfy the dual constraints with equality, which is a finite induction on the stages; the extreme-point clause needs that every vertex of a polyhedron is the unique maximizer of some linear functional, and the region clause that a compact convex set is the convex hull of its extreme points (Krein–Milman in finite dimension, or the polyhedral fact directly). None of this is in Mathlib in the required form. Lemma 5.1 is probabilistic: the lower bound requires the strong Markov property of the continued bandit under an arbitrary past-measurable policy, a pathwise accounting of the discounted periods paid for by each continuation from , and the observation that at most slots can be spent on bandits that have never been in ; the equality for priority policies requires that these policies use exactly those slots first and then tile the future with return excursions, and the product form of requires independence of the bandits' process-time trajectories under the run law, which is built decision time by decision time rather than as a product. The p. 123 theorem is the computation (5.13) to (5.14) combined with the optimal-stopping characterization of Chapter 2 for the stop sets , which lie between and ; ties make the induction delicate, and the statement is claimed for every tie-breaking.
GCL(1) and GCL(2) systems are structures over an arbitrary policy type: performance, base function, matrix, permutation policies and the three laws are fields, so the theorems are statements about finite-dimensional data and the platform's proof needs no probability. The adaptive greedy algorithm is specified relationally, as the set of its possible outputs with arbitrary tie-breaking, and the conclusion holds for each of them; existence of an output is asserted separately. The optimality clause is stated as a comparison with every policy rather than as a real supremum. The hypothesis that the achievable region is convex is explicit: the book's argument from extreme points to the whole polytope uses randomization of policies, and without it the region of a system with only its permutation policies is finite. The SFABP items use identical bandits on Fin N in the Bandit Algorithms model, the coefficients through Mission I's stoppedTime at the return time, and in the product form , which is the minimal cost the argument on p. 120 establishes; the book prints a sum, which is when all bandits start in where the minimal cost is . Discount factors are in throughout.
Trivializing readings are excluded: for is part of the structure and of Lemma 5.1's conclusion, the polytope equations are over all subsets, and the index clause quantifies over every greedy output. Welcome contributions: the nonpositivity and dual feasibility of the greedy variables, the vertex-exposure lemma for polyhedra, and the product decomposition of the run law of identical bandits.
A recommendation system learns from the users it serves: the diner who tries a restaurant produces the review the next diner reads. Each user would rather exploit what is already known than explore for the benefit of those who come later, so a population of self-interested agents under-explores, and an alternative that looks bad on sparse early evidence may never be tried again even when it is the best. Chapter 11 of Slivkins, Introduction to Multi-Armed Bandits (arXiv:1904.07272), treats incentivized exploration: a principal who cannot force the agents but can recommend, and who, because it aggregates what earlier agents observed, knows more than any one of them. The question is whether recommendations alone can induce enough exploration to learn as fast as an ordinary bandit algorithm. The model is that of Kremer, Mansour and Perry (JPE 2014) and the results are those of Mansour, Slivkins and Syrgkanis (EC 2015, Operations Research 2020), specialized to two arms; the single-round problem is Bayesian persuasion in the sense of Kamenica and Gentzkow (AER 2011).
There are arms and rounds. A mean reward vector is drawn from a known prior , and each pull of arm yields a reward drawn from a known family with mean . In round the principal recommends an arm ; agent , who knows the prior, the family, the algorithm and the round but not the past, sees only , chooses , collects and leaves; the principal observes . The chapter works with two arms, ordered so that the prior means satisfy , with a prior of finite support and finitely many reward values.
An algorithm is Bayesian incentive-compatible (BIC, Definition 11.4) if following its recommendation is in every agent's interest given what the agent knows: for every round and arms with ,
where is the event that all previous agents complied. A BIC algorithm is then an ordinary bandit algorithm whose recommendations are followed, and the run has the law of the Bayesian bandit of Chapter 3. Two contrasting policies frame the chapter. GREEDY reveals the history and lets agents exploit, (11.2); it is BIC and it fails. HiddenExploration (Algorithm 11.1) hides a little exploration in a lot of exploitation: on a signal , with probability it recommends a target arm , otherwise the arm maximizing , ties to arm 1. Its posterior gap is . RepeatedHE (Algorithm 11.2) runs it round after round with an arbitrary bandit algorithm as the target: initial rounds recommend arm 1; afterwards, with probability the round is an exploration round in which chooses (and is fed the reward), and otherwise the exploitation branch recommends , where is the data of all exploration rounds so far (11.10). The quantity that governs everything is (11.11), the posterior gap after samples of arm 1, and Property (11.12), that for some : arm 2 can appear better after enough samples of arm 1.
RepeatedHE with exploration probability and initial samples of arm 1 is BIC as long as
for any bandit algorithm and any horizon. The threshold depends on the prior alone.
Theorem 11.7 (GREEDY never chooses arm 2 with probability at least ) and Corollary 11.8 (linear Bayesian regret of GREEDY under independent priors); Lemma 11.10 (HiddenExploration is BIC when ) with Claim 11.12 (the arm-2 side of the constraint suffices); Corollary 11.14 (RepeatedHE is BIC under the round-by-round condition); Theorem 11.19 (without Property (11.12) no BIC algorithm ever plays arm 2, ties to arm 1).
The results say when exploration can be incentivized at all and how. Theorem 11.7 shows that revealing everything is not a solution: the greedy dynamics gets stuck on arm 1 with a probability that does not shrink with , and Corollary 11.8 turns that into Bayesian regret. Theorem 11.15 shows that a recommendation-only principal can induce any amount of exploration it wants, with arbitrary, at a per-round rate fixed by the prior; Theorem 11.17 (stated with a proof sketch, and omitted here) then transfers 's regret to RepeatedHE up to the prior-dependent factors and , so regret is attainable subject to incentives. Theorem 11.19 closes the picture: Property (11.12) is necessary as well as sufficient. Together they characterize which priors admit incentivized exploration and give an algorithm that works for all of them.
Nothing of this is machine-checked. The mission adds to the Bayesian layer of mission III (prior, posterior by Bayes' rule, Bayesian regret) the BIC constraint on a joint law, GREEDY as a policy, the single-round HiddenExploration on an abstract finite signal, and the law of RepeatedHE; all of it is reusable for the -arm and the "explore all explorable arms" extensions of the literature review.
Theorem 11.7 is a martingale argument: the posterior gap along the history is a Doob martingale, the first round in which arm 2 is chosen is a bounded stopping time, and optional stopping gives ; all of this has to be set up on the joint law of of mission III, where the posterior is defined by Bayes' rule and the identification with a conditional expectation is itself a theorem (posterior_eq_condProb). Lemma 11.10 is the heart of the chapter and is not a computation about : it works with , splits along the two branches, uses that the exploitation branch recommends arm 2 exactly when , and closes with ; the only place where the analysis uses that both branches are functions of the signal is the step , and a formalization has to make that step explicit. Theorem 11.15 requires seeing each later round of RepeatedHE as a HiddenExploration with signal , where 's choice is a randomized function of , and then the monotonicity of in , a two-line consequence of determining that presupposes the posterior given is the Bayes posterior of the exploration data alone, which is true because the exploration decisions do not depend on given that data. Corollary 11.8 needs the independence of the event " and arm 2 is never chosen" from . Theorem 11.19 is an induction in which the inductive hypothesis is a probability-zero statement about all earlier rounds.
Arms are Fin 2, the book's arm 1 being index 0; rounds are Fin T. The prior is a probability measure on mean vectors supported on a finite set , with as a hypothesis; the reward family is mission III's RewardFamily (finitely many values, mean for ). BIC is defined on a joint law of of the run in which every agent complies, with the recommendation of each round read off the record; the compliance event of (11.1) is the sure event of that law, which is the standard reading of "the agents believe all previous agents complied". For a bandit policy the law is mission III's jointMeasure. Conditional expectations are written as finite sums over , so there are no integrals and no integrability side conditions; a posterior mean off the support is a junk that never enters a theorem. GREEDY allows arbitrary tie-breaking; HiddenExploration's exploitation branch breaks ties toward arm 1 as Algorithm 11.1 does; the tie convention of Theorem 11.19 is the strict form of BIC for arm 2. The law of RepeatedHE is an explicit finitely supported measure, and record weighted by the prior times the product of the round probabilities (initial rounds forced to arm 1, then the -coin, 's kernel on its own history, or the exploitation arm, then ); it is written this way because is fed a history of variable length. Two conditions are stated exactly as printed: Lemma 11.10 with (non-strict, checked at equality) and Theorem 11.15 with the strict inequality.
Trivializations are excluded: throughout; the BIC condition is asserted only where the recommendation has positive probability, and the sums in it are over the finite support, so an unsatisfiable hypothesis cannot hide in a measure-zero set. Welcome contributions: the optional-stopping argument on jointMeasure, the identification of explPostMean with the conditional expectation given the exploration data, the Bayes-rule algebra behind Lemma 11.10, and the counting lemmas on heRecords.
Airlines selling last seats, Priceline's name-your-own-price, procurement of supply contracts: Chapter 6 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) treats auctions as pricing mechanisms and asks what revenue they earn and how to design them. Its centre is Myerson's (1981) theory for independent private values: whatever the mechanism, so long as bidders with higher valuations are more likely to win and the lowest type gains nothing, the firm's expected revenue is the expected virtual value of the winners, with (Theorem 6.1, the revenue equivalence theorem). Maximizing that expression pointwise gives the optimal auction: the standard first- or second-price auction with a reserve price at the zero of (Theorem 6.2). This mission formalizes the second-price form of Theorem 6.2 as its goal, with the dominant-strategy and first-price equilibria of the informal analysis, Theorem 6.1, the optimal allocation and Proposition 6.1 on list prices as supporting results.
customers have i.i.d. valuations on with a continuously differentiable,
strictly increasing distribution and positive density (PrivateValues, IsRegular); the
joint law is the product measure (joint). A direct-revelation mechanism (Mechanism) maps
reported valuations to allocations , at most units in total, and
payments . For a report by customer , is the win probability,
the expected payment and the surplus (winProb, expPayment,
expSurplus); incentive compatibility, , is the equilibrium
condition of the direct mechanism (IsIncentiveCompatible). The chapter's mechanisms are the
-unit second-price auction with reserve price (secondPriceReserve: the highest
valuations above win and pay the larger of and the highest losing valuation), the
list-price mechanism for (listPrice), and the single-unit first-price auction with
its equilibrium bid , (firstPriceBid).
With strictly increasing (Assumption 7.2) and its zero, the -unit second-price
auction with reserve price is a feasible, incentive-compatible mechanism with monotone
allocations and zero surplus at zero, and its expected revenue is at least that of every such
mechanism: reserve_price_auction_optimal.
Bidding one's valuation is dominant in the second-price auction (Sect. 6.2.2.1); the bid (6.4) solves the first-order condition (6.3), is a symmetric equilibrium of the first-price auction and shades below the valuation (Sect. 6.2.2.2); Theorem 6.1, revenue equals expected virtual surplus and each expected payment is ; the pointwise optimal allocation of Sect. 6.2.5; and Proposition 6.1, a list price at is optimal when .
Proposition 6.2 (asymptotic optimality of list prices, a law-of-large-numbers statement about scaled auctions), the first-price form of Theorem 6.2 with its equilibrium (6.9) stated without proof, and the dynamic, replenishment and network auctions of Sects. 6.3-6.5 (Propositions 6.3-6.11, from Vulcano, van Ryzin and Maglaras and from Cooper and Menich) are not targets of this mission.
Theorem 6.1 is the tool that lets revenue be computed from allocations alone, which is why the first- and second-price auctions of Examples 6.1-6.3 earn the same and why any dynamic pricing scheme that ends with the same winners earns the same as the optimal auction (Sect. 6.2.6.3). Theorem 6.2 says a firm with private-value customers cannot do better than a standard auction with the right reserve price, and Proposition 6.1 that with enough capacity a list price already does it: auctions are a small-numbers phenomenon. These are the foundations on which the chapter's dynamic auctions and the list-price comparisons of Sects. 6.3-6.4 rest, and Myerson's optimal auction has no machine-checked proof in its multi-unit form.
Theorem 6.1 is an envelope argument in measure-theoretic clothing: incentive compatibility gives the two-sided inequalities of Appendix 6.A, monotonicity of makes convex with derivative almost everywhere, so , and then an integration by parts against the density converts into ; the win probabilities are integrals over a product measure with one coordinate replaced, and Fubini is needed to return to . The goal then needs the reserve-price auction shown incentive compatible (a dominant-strategy argument on the threshold payment), measurable, monotone and with zero surplus at zero, and the pointwise optimal allocation integrated. The first-price item is calculus on an interval integral with a vanishing denominator at and a monotone comparative-statics argument for the equilibrium inequality.
Mechanisms are direct-revelation mechanisms on , as the book reduces to in Sect. 6.2.3.1; expectations over the other customers are integrals over the joint law with customer 's coordinate overwritten by the report. Payments are assumed bounded on reports in (not on all of , where the second-price payment is unbounded) and the rules measurable. Ties in the second-price auction are broken by index, a null event, and when every customer wins the losing supremum is so the winner pays the reserve. Theorem 6.2 is stated for the second-price auction; the first-price version with reserve price, whose equilibrium (6.9) the book asserts without proof, is left out and noted. Optimality is over mechanisms satisfying conditions (i) and (ii) of Theorem 6.1 and incentive compatibility, which is the class the book compares against. The virtual value's zero is a parameter with rather than the maximum of (6.8), which under strict monotonicity is the same point.
Every airline, hotel and car-rental firm sells more reservations than it has capacity, because some customers cancel or do not show. Chapter 4 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) is the theory of that decision. Its static models pick one overbooking limit from the show distribution; its dynamic model, a simplification of Chatwin's (1998), follows reservations, cancellations and refunds period by period and proves that the optimal control is still a limit, one that declines toward the deadline and falls when more demand is expected; and its substitutable-capacity model, from Karaesmen and van Ryzin (2004), sets joint limits for several classes whose oversold customers can be moved between resources, showing the expected net revenue is concave in each limit and submodular across them. This mission formalizes the chapter's four propositions and the corollary the book draws from the last.
Dynamic overbooking (Sect. 4.3.1). With reservations on hand in period , new
requests arrive; the firm books up to at revenue each, and every
reservation survives the period with probability , a cancellation refunding . At the
deadline the firm pays the convex denied-service cost on reservations beyond
capacity , Eq. (4.11). The recursion is
with
and
(value,
postValue). The greatest optimal overbooking limit (overbookingLimit) is the
largest level at which is at least its value at every smaller level, an
element of ; the limit policy books
(limitPolicy).
Substitutable capacity (Sect. 4.5). Classes hold reservations and
are overbooked to levels ; in the service period
customers show and are assigned to resources of capacities , or to the
virtual resource (denied service), at net benefit , by the transportation problem
(TP) with value (serviceValue). The expected net revenue (4.21) is
(expNetRevenue),
and jointLimit is the greatest optimal limit of one class with the others fixed.
With Poisson show demands, has decreasing first differences in every direction:
for all and all classes , which
is component-wise concavity () and submodularity ():
joint_overbooking_concave_submodular.
Proposition 4.1, with a convex denied-service cost the limit policy with the greatest optimal limit attains the maximum of the recursion at every state; Proposition 4.2, under the greatest optimal limits decline with time; Proposition 4.3, stochastically larger demand to come gives limits that are no larger; and the corollary of Sect. 4.5.2, the greatest optimal limit of class is nonincreasing in the level of any other class.
The static overbooking models of Sect. 4.2 (binomial, normal and Gram-Charlier approximations, Type 1 and Type 2 service levels), the net-bookings heuristics of Sect. 4.3.2, the combined capacity-control models of Sect. 4.4 and the stochastic-gradient algorithm of Appendix 4.A carry no numbered results and are not targets.
Proposition 4.4 is the structural fact that makes joint overbooking of related resources tractable: concavity gives each class a critical booking level and submodularity makes those levels move in opposite directions, so a stochastic-gradient or coordinate search on the limits is well behaved, and the pattern of Example 4.5, overbooking an early flight aggressively because its oversold passengers can be moved to later ones, is a consequence rather than a heuristic. The dynamic propositions are the theoretical support for the overbooking curves that reservation systems post, limits that fall as departure approaches, and they quantify the sense in which a static model, which ignores future demand, overbooks too much. The proof of Proposition 4.4 passes through the discrete concavity of the transportation problem's value in its supply vector, an M-natural-concavity fact in the sense of Murota, and the Poisson-expectation identity for second differences; none of this has a machine-checked proof.
The dynamic model needs the concavity of on to be propagated through two
operations, the binomial thinning and the windowed
maximum , both of which preserve discrete concavity
but require explicit manipulation of binomial sums and of the argmax; Propositions 4.2 and 4.3
then compare greatest maximizers of concave sequences through lower bounds on marginal values,
with the value handled in ℕ∞. The substitutable-capacity goal is harder: the value of
(TP) as a function of the integer supply vector must be shown to have decreasing differences,
which is the submodularity of a max-weight transportation value in its supplies, a linear
programming duality argument (or Murota's M-natural-concavity of min-cost flow), and the
Poisson expectation of it, a tsum over , must be differenced in two coordinates
using the identity for Poisson pmfs.
The linear terms of cancel in second differences and the refund term is linear in .
Periods are natural numbers with value t the value with periods to go, and the
book's ranges are hypotheses. The denied-service cost is normalized,
and , as a cost "penalizing denied service" is. Convexity of the sequence alone is not
enough, because (4.11) never reads . Demands are pmfs on and cancellations
exact binomial sums. The greatest optimal limit lives in because a
mild denied-service cost can make accepting every request optimal, in which case the book's
critical value is ; the limit policy then accepts everything. Proposition 4.3 is stated
for two demand families ordered by first-order stochastic dominance rather than a parametrized
family. In the substitutable-capacity model the virtual resource is uncapacitated, the book's
"finite but very high" taken as infinite so that (TP) is feasible for every Poisson
realization, and (TP) is over real assignments, whose optimum at integer supplies is integral.
Eq. (4.21) is printed with ; being the maximum net benefit, the
expected net revenue adds it, and the definition uses , without which Proposition 4.4 fails
numerically on every sampled instance.
An airline sells one flight, a hotel one night, a car-rental firm one day of one car: a fixed capacity, perishable at a deadline, sold to customers who arrive over time and are willing to pay different amounts. Chapter 2 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) is the theory of that single resource. Its three models answer the same question with increasing generality: Littlewood's two-class rule, the -class static model and its dynamic-arrival version give the seller a protection level per class, a booking limit or a bid price, all three equivalent; the discrete-choice model, in which customers buy down when a cheaper fare is open, replaces classes by offer sets and shows that only the efficient sets, ordered by their purchase probability, are ever offered, with a higher set the more capacity or the less time remains. This mission formalizes that last result, Theorem 2.3, together with the structural results of the two earlier models that it generalizes.
Static model. Classes with prices arrive in
stages, lowest class first, with demands distributed on . With units left at
stage the seller observes and accepts units; the value function
is the Bellman equation (2.3), ,
(staticValue), and is the marginal value of capacity. The
protection level (protLevel), the booking limit
(bookLimit) and the bid price
(bidPrice) define the three controls of Theorem 2.1.
Dynamic model. Over periods at most one request arrives per period, of class with
probability ; the value function (2.17) is
(dynValue), with time-dependent protection levels (2.19), booking limits (2.20) and bid
prices (2.18).
Choice model. When the set of classes is open an arriving customer buys class
with probability ; is the purchase probability and
the expected revenue (purchaseProb, expRevenue). The value
function (2.26) is
(choiceValue). A set is inefficient (Definition 2.1, IsInefficient) if a
randomization over the subsets has and
, and efficient otherwise.
In every period with capacity left, some efficient set maximizes (2.26); and, the efficient
sets being ordered by , the largest optimal set is nondecreasing in the remaining capacity
and nondecreasing in the period : choice_optimal_policy. Monotonicity is stated as
"every efficient optimal set at is matched by one at , , with at
least as large a purchase probability", and likewise in .
Littlewood's rule (2.1), and the acceptance criterion; Proposition 2.1, the marginal values of the static model are decreasing in and increasing in the stages remaining; Theorem 2.1, nested protection levels, nested booking limits and bid-price tables each attain the Bellman maximum at every stage; Proposition 2.2 and Theorem 2.2, the same two results for the dynamic model, with marginal values now decreasing in time; Proposition 2-2.A.4 of the appendix, the marginal values of the choice model are decreasing in and in ; Proposition 2.3, an inefficient set is never optimal; and the ordering of efficient sets, implies when is efficient.
The continuous-demand optimality conditions (2.9) of Sect. 2.2.2.3, stated without proof, the computational and heuristic methods of Sects. 2.2.3-2.2.4, the overbooking models of Sect. 2.7 and the nested-policy characterization of Sect. 2.6.2.5 are not targets.
Theorem 2.3 is the structural result behind choice-based revenue management: it reduces the offer sets to the efficient frontier of , orders that frontier, and shows the optimal policy walks up it as capacity grows or the deadline nears. It was the analytical core of Talluri and van Ryzin's (2004) choice-model paper and is the reason the efficient sets, not the fare classes, are the unit of control when customers substitute between fares. The static and dynamic results, from Littlewood (1972) and Brumelle and McGill (1993) to Lee and Hersh (1993), are the foundation of every airline seat inventory control system; the equivalence of protection levels, booking limits and bid prices is what lets the same optimal policy be implemented on any of the three kinds of reservation system. None of these results has a machine-checked proof.
The two marginal-value propositions are inductions in which the inductive step is the discrete
concavity of a max-plus convolution, Lemma 2-2.A.1 of the appendix: is concave when is, which in Lean requires reasoning about the
argmax on and the truncated subtraction. The static model's expectation is a
tsum against a pmf, so every step also needs summability of a bounded family. The
protection-level theorems then need the down-set structure of
under monotonicity of , and the three controls have to be shown to coincide unit by
unit. For the choice model, Proposition 2.3 is a one-line convexity argument once
is known, and the monotonicity in Theorem 2.3 is a monotone comparative-statics
argument on the objective , which is easy in but must be combined
with Proposition 2-2.A.4 in both and ; the existence of an efficient maximizer uses
Proposition 2.3 and the finiteness of the subsets.
Capacities, stages and periods are natural numbers, the value functions recurse on the stage or
on the number of periods to go, and the book's ranges (, , ) are
hypotheses of the theorems. Demand in the static model is a pmf on rather than a
random variable, so the expectation in (2.3) is a tsum; the dynamic model's expectation over
is written out, including the no-arrival term, which vanishes under nonnegative prices.
The choice model is defined by its compact form (2.26), and the maximization includes the empty
offer set. Optimality of a control means attaining the inner maximum of the Bellman equation at
every state, which is what the book's proofs establish. The bid-price control is formalized with
the bid price of the -th unit allocated; the book prints ,
which is one unit off from (2.5). The appendix's Proposition 2-2.A.4 prints its time
monotonicity in the reverse direction; the formal statement is the direction consistent with
Proposition 2.2 and Theorem 2.3. The ordering of efficient sets is stated with non-strict
inequalities, since Definition 2.1 admits ties in revenue.
Chapter 10 of Axsäter's Inventory Control turns to reorder points and safety stocks in multi-echelon systems, where the installations cannot be treated separately: a large stock downstream lets an upstream site run lean, and a long upstream lead-time argues for stock at the top. The best-known exact technique for serial systems is the decomposition of Clark and Scarf (1960), which the book presents in the infinite-horizon form of Federgruen and Zipkin (1984). It is also where the echelon stock measure comes from. The section's argument is short and self-contained, and its conclusion is a complete description of the optimal policy for a two-level serial system: order-up-to levels at both installations, one of them a newsboy solution, the other the minimizer of a convex function in which upstream shortages appear as an induced cost. It is the capstone of Chapter 10.
Installation 1 faces normally distributed period demand with mean and standard deviation , independent across periods, so the demand over periods, , is normal with mean and standard deviation . Installation 1 replenishes from installation 2 with lead-time periods; installation 2 replenishes from an outside supplier with infinite supply and lead-time . Demand that cannot be met is backordered. Costs per unit and period are echelon holding costs , so the installation holding costs are and , and a shortage cost at installation 1; there are no ordering costs. Events in a period occur in the order: installation 2 orders, its delivery arrives, installation 1 orders, its delivery arrives, demand, cost evaluation.
Consider an arbitrary period . After ordering, installation 2 has an echelon inventory position , and by the standard argument its echelon stock in period is . Installation 1 then orders, realizing an echelon position that cannot exceed what is available: (Eq. 10.1). Its inventory level after the demand in period is . The expected period costs are at installation 2 and at installation 1, and the book reallocates the term to obtain
with and . As a function of a free , is the newsboy-type function of Eq. (10.6), minimized at the level given by the fractile equation (10.8). Passing everything available up to to installation 1, , gives the total cost of Eq. (10.9), whose minimizer is the order-up-to level of installation 2.
With from (10.8) and a minimizer of : for every and every allocation rule with and finite expected cost,
and the order-up-to policy attains .
Eq. (10.3), the stage-1 period cost through the expected backorders; the reallocation (10.4)-(10.5), which leaves the total unchanged; the closed form (10.6) of through the loss function ; the convexity of , its derivative (10.7), and the fractile characterization (10.8) of its minimizers; the pointwise rule that is the cheapest feasible ; the identity (10.9); and the convexity of (Problem 10.1) with the existence of its minimizer when .
The result itself. The decomposition reduces a two-dimensional stochastic control problem to two one-dimensional convex problems solved in sequence, from downstream to upstream, and it identifies the optimal policy class. The downstream level is a newsboy solution with overage cost , the value added, and underage cost , and it is independent of the upstream installation altogether; the upstream level sees the downstream installation only through the induced shortage cost, the last term of (10.9). The book notes the extensions the argument admits, to more echelons, to batch ordering at the top, and, via Rosling's equivalence, to assembly systems, and its Sect. 10.1.2 adapts it, now only approximately, to distribution systems under the balance assumption. Example 10.1 shows the typical outcome: the optimal average stock at the upstream installation is slightly negative.
Formalizing it. The section's mathematics is a chain of expectations under Gaussian laws and two convexity arguments. Formalizing it fixes what "optimal" means, a per-period comparison against every allocation rule, and separates the two convexity claims the book makes in one clause each. Nothing here is open; no statement has a machine-checked proof yet.
The pointwise allocation rule and the newsboy fractile are the same arguments as in the newsboy mission. The two places where work is needed are the identity (10.9), an expectation of a piecewise function split at , and the convexity of , which requires seeing that is convex precisely because is a minimizer of the convex (for any other cut-off the function is not convex), and that convexity is preserved by integrating against the law of , which needs the integrability of the linearly growing . Existence of then follows from the growth of at both ends, which comes from the asymptotics of the loss function: as and as .
is csDemand mu sigma n, the Gaussian law newsboyDemand (n μ) (√n σ) from the newsboy
mission, so the loss function and its closed form are reused as references. The costs are
parametrized by with and written out; ,
, the pre-reallocation period cost and are Bochner integrals against these
laws. Every statement assumes ; the goal and the convexity statements assume
and , the book's cost signs. is allowed and makes a
point mass, which is the setting of the book's Problem 10.2.
enters as any solution of the fractile equation (10.8) and as any minimizer of ; the other items show that both exist when . When the fractile is , no exists, and the goal is vacuous, which is faithful: the book observes that then and installation 2 never carries stock. Symmetrically, when and , decreases towards its infimum without attaining it, so no exists and the goal is again vacuous: with free upstream holding the optimal is unbounded. Allocation rules are arbitrary functions of the realized with an integrability hypothesis; without it Lean's integral of a non-integrable cost would be and could undercut , which is negative in Example 10.1's stage-1 term.
What is not modelled is the infinite-horizon dynamic problem: the book's optimality claim is made period by period, and the passage to the stationary policy rests on the remark that the outside supplier has infinite supply, so the same can be chosen in every period. The definitions are reusable for the three-echelon extension and for the distribution system of Sect. 10.1.2; contributions formalizing Problem 10.2 () as a first step are welcome.
A serial supply chain is the simplest multiechelon system: a retailer orders from a warehouse, which orders from a plant, which orders from an outside supplier with unlimited stock. Only the retailer sees customer demand, only the retailer pays a stockout penalty, and every stage pays to hold inventory. Choosing how much each stage should hold looks like a joint optimization over all stages at once, because an upstream stockout delays every downstream replenishment. Clark and Scarf (1960) showed that it is not: measured in echelon terms, the optimal policy is a base-stock policy at every stage, and the optimal levels can be found one stage at a time from the customer upward, each step a single-variable convex minimization. Chapter 6 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) presents the infinite-horizon form of that result as its Theorem 6.3, the bounds of Shang and Song (2003) that make the levels cheap to approximate, and the contrasting guaranteed-service model of Graves and Willems (2000), in which stages quote delivery times rather than fill rates and the optimal safety stocks are all-or-nothing. This mission formalizes the chapter's numbered results, with Theorem 6.3 as its goal.
Stages are numbered from the customer upward. Stage has a local holding
cost per unit per period; its echelon holding cost is with
, so that (localHolding, echelonHolding). Stage
's echelon consists of stages , and its echelon on-hand inventory
(echelonOnHand) is all on-hand and in-transit stock in that echelon. Stage 1 pays a
stockout cost per unit per period. Orders placed by stage arrive after a lead time
if stage can ship them; denotes the lead-time demand at stage .
An echelon base-stock policy gives each stage a level and orders to keep its echelon
inventory position at . The chapter derives, from conservation of flow, a recursion that
evaluates the expected cost of any echelon base-stock vector (csBar, csHat, csG):
and the expected cost of the system under is . The term is the
implicit penalty function: it charges stage for the downstream consequences of
running short. A vector is sequentially optimal (CSSequential) when each minimizes
, which depends only on .
The Shang-Song bounds compare with the cost of the -stage truncated system when all its
local holding costs are set to one value, for the lower bound and for
the upper (ssLower, ssUpper). With equal holding costs all stock is held at stage 1, so each
bound is a single-stage newsvendor cost for the demand over the
cumulative lead time (tildeLaw) with stockout cost , plus the holding cost of the
stock in transit to stages , whose mean is
(pipelineMean).
In the guaranteed-service model each stage has a processing time , quotes a
committed service time to its customer, and receives an inbound time
from its supplier (gsInbound), being external. Demand is bounded, so the stage can meet
every order within by holding safety stock with ,
and the holding cost is (gsCost) over the
feasible times (GSFeasible).
For echelon holding costs , stockout cost and lead-time demands of finite mean, if is sequentially optimal then for every echelon base-stock vector ,
and is the optimal cost. This is clark_scarf_sequential.
Proposition 6.1, ; the stage-1 identities (6.29) and (6.30), that is a newsvendor cost with penalty and its minimizer solves ; convexity of every under sequential optimality; existence of a sequentially optimal vector when and ; Theorem 6.4, , and where minimizes and minimizes (the book's pairing, p. 200); and Theorem 6.5, that in the guaranteed-service serial system with every optimal is or .
Theorem 6.2, the optimality of echelon base-stock policies among all policies, is stated in the book without a model of the policy space and is not a target here; Theorem 6.3 is the optimization it licenses.
Theorem 6.3 is what Zipkin calls the fundamental equations of supply chain theory. It reduces a joint optimization over coupled levels to one-dimensional convex problems, and every exact method and most heuristics for serial and assembly systems, Rosling's reduction of assembly systems to serial ones included, run through it. Theorem 6.4 turns the recursion into closed-form bounds and the Shang-Song heuristic, which the book reports as accurate to within a fraction of a percent. Theorem 6.5 explains the shape of optimal safety stock placement under guaranteed service and why its dynamic program only needs to examine endpoints.
None of these results has a machine-checked proof. The book proves none of them in full: Theorem 6.3 is asserted after an informal derivation, Theorem 6.4 is cited, and Proposition 6.1 and Theorem 6.5 are left as exercises. Formalizing the recursion's convexity and the exchange argument behind Theorem 6.3 produces a reusable treatment of the implicit penalty function; the concavity-on-a-polytope argument for Theorem 6.5 is reusable for the tree systems of Sect. 6.3.5.
The obvious attack on Theorem 6.3, differentiating the system cost in each , fails immediately: the cost depends on through inside nested expectations and is not convex in jointly. The argument that works is an induction along the recursion, comparing with pointwise. Its key step is that, for the convex minimized at , the value is the least value of on , so that any other truncation point can only cost more. That step needs convexity of , which needs convex, which needs to be a minimizer; for an arbitrary the functions are not convex, and the induction must carry both vectors at once.
Integrability is a second, silent obstacle. Each is an expectation of translates of ; the recursion preserves Lipschitz continuity with a constant growing with the costs, and finite means are exactly what make every integral in the recursion a genuine expectation rather than Lean's default value zero.
Theorem 6.4 requires relating the recursion, in which demands enter one stage at a time, to a single newsvendor cost in the sum , which is a convolution; the inequalities come from the structure of (6.31) in the two extreme holding-cost profiles and are not obvious from the recursion's formulas. Theorem 6.5 is a statement about every minimizer, not the existence of an extreme one, so the proof must show the cost is strictly concave along every feasible direction that changes a net lead time and then classify the vertices of the feasible region.
Stages are indexed by natural numbers ; the cost functions take total functions on and never read values outside that range. The recursion is defined for every vector , so the theorem compares values of one family of functions rather than a separately defined system cost; the identification of with the steady-state expected cost of the physical system is the book's derivation and is not restated. Expectations are Lebesgue integrals under the lead-time demand laws, assumed to be probability measures on with finite means. Sequential optimality is a hypothesis of the goal; a separate target shows it is satisfiable when and , so the goal is not vacuous.
The bounding functions of Theorem 6.4 keep the holding cost of pipeline stock that the truncated cost (6.31) charges. The book omits that constant when it writes their minimizers, which it does not affect, but part (a) compares values, and without the constant the upper bound fails already in the book's own Example 6.1. For part (b) the minimizers of the bounding functions are asserted to exist and to bracket ; when the fractiles of are unique these are the book's quantile values. Theorem 6.5 is stated over real service times; because the feasible region's vertices are integral when the data are, every integer-optimal vector is optimal over the reals, so the real statement contains the book's integer program (6.38) to (6.42). Proposition 6.1 is stated with built into the echelon sum.
The definition module is shared by all nine items. The dynamic program (6.43) to (6.44) for guaranteed-service serial systems and the tree-system algorithm of Sect. 6.3.6 are natural extensions on the same definitions.
A firm that holds inventory in five warehouses needs more safety stock than one that holds the same inventory in one warehouse, because the demands of five regions do not all run high at once. Eppen (1979) made this precise for a multi-location newsvendor and gave it its name, the risk-pooling effect. Chapter 7 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) follows the same idea through three settings in which pooling happens without physical consolidation: two retailers who ship stock to each other after seeing demand (transshipments, after Tagaras 1989), and plants that can each make more than one product (process flexibility, after Jordan and Graves 1995). The chapter's capstone is the theorem of Simchi-Levi and Wei (2012) that, among designs in which every plant makes two products and every product is made at two plants, a single long chain through all of them is best. This mission formalizes the chapter's numbered results, with that theorem as its goal.
Risk pooling. distribution centers face normally distributed per-period demands
with correlation coefficients , and each runs a
base-stock policy with holding cost and backorder cost per unit per period, so its
optimal expected cost is the optimal newsvendor cost optNvCost h p D, the infimum over
base-stock levels of . Merging the centers gives one
facing the total demand, normal with mean and variance
(pooledVariance).
Transshipments. Two retailers with base-stock levels face independent
demands. After demand is observed, under complete pooling the retailer with a surplus sends
the retailer with a shortage units (transship), and
nothing moves otherwise. The type-1 service level is the probability of no stockout,
without and with
transshipments; the type-2 service level is the fill rate, one minus expected unmet demand
over expected demand, and likewise.
Process flexibility. A flexibility design on products and plants is a set
of (product, plant) pairs, an edge meaning plant can make product . Given a
demand realization and a common plant capacity , the performance (perf)
is the maximum sales obtainable by assigning production along the edges of without
exceeding any capacity or demand, the linear program (7.22) to (7.26). A balanced system
(BalancedSystem) has equal capacities and an exchangeable demand vector, one whose joint
law is invariant under permutations of the products, and is the
expected performance (expPerf). The named designs are the dedicated design ,
the long chain in which plant also makes product (and plant makes
product ), the open chain obtained from by deleting the edge , and
, the open chain on the first pairs together with the dedicated edges of the rest. A
2-flexibility design (TwoFlex) is one in which every product has exactly two plants and
every plant exactly two products; is one, and so is any union of disjoint shorter chains.
For a balanced system of size with exchangeable demand,
that is, is a 2-flexibility design and for every 2-flexibility design .
This is long_chain_optimal.
The chapter's route to the goal: Lemma 7.5, supermodularity of sales in the flexible edges of the long chain for every realization, for ; Corollary 7.6, the same in expectation; Lemma 7.7, the increments are nondecreasing in , ending with ; and Lemma 7.8, .
Risk pooling, Theorem 7.1: , the optimal cost of the merged center is at most the sum of the optimal costs of the separate ones, with the covariance inequality as a separate lemma.
Transshipments, Theorems 7.2 to 7.4: , , and all four post-transshipment service levels are nondecreasing in .
Theorem 7.9 is the analytical answer to a question that had been settled only by simulation: Jordan and Graves reported that one chain through all plants achieves nearly twice the sales benefit of three short chains with the same number of edges, and Simchi-Levi and Wei proved that no arrangement of the same edge budget does better. It is the justification for the chaining guideline used in automotive and semiconductor capacity planning, and Lemma 7.8, which expresses the long chain through open chains, is what makes the long chain's performance computable by a greedy pass. Theorem 7.1 is the quantitative basis for consolidation decisions and for postponement, since a generic product is pooled inventory. Theorems 7.2 to 7.4 quantify what transshipments buy in service, which is the argument for allowing them despite their cost.
None of these results has a machine-checked proof. The book proves Lemma 7.7, Lemma 7.8 and Theorem 7.9 in full given Lemma 7.5, which it cites to Simchi-Levi and Wei, and omits the proofs of Theorems 7.3 and 7.4 and the identity (7.30) behind Lemma 7.8. Formalizing Lemma 7.5 and (7.30) means formalizing the structure of maximum flows on a cycle, which is reusable for the later results of Simchi-Levi and Wei on the long chain's performance relative to full flexibility and for the multi-echelon flexibility models the chapter cites.
The obvious approach to Theorem 7.9 is to compare with an arbitrary 2-flexibility design directly. Nothing in the definitions supports that: the two designs share no structure beyond their degree sequences. The book's argument instead routes everything through the long chain's own edges. Lemma 7.5 gives supermodularity only for subsets of , and the decomposition of an arbitrary 2-flexibility design into disjoint cycles, each a relabeled long chain on a subsystem, is what allows the comparison. A solver must therefore prove that a 2-regular bipartite graph is a disjoint union of even cycles, that exchangeability makes every relabeling of a cycle worth the same as on its subsystem, and that the performance of a disjoint union is the sum of the performances of its parts.
Lemma 7.5 itself is where the combinatorics lives. It says that on the cycle the maximum flow is supermodular in the flexible edges, and the proof in Simchi-Levi and Wei goes through the structure of augmenting paths on a cycle. The natural first idea, that supermodularity follows from some general property of maximum flows, is false: maximum flow is not supermodular in arbitrary edge sets, and the lemma is specific to subsets of a single cycle.
Lemma 7.7 is where exchangeability is used, and it is used in a way that is easy to state and tedious to formalize: removing the edge from leaves a design that is only after the pair is moved to the end, so the argument needs the invariance of under relabeling the products and plants by a common permutation. The book notes that Lemma 7.7, unlike Lemma 7.5, is false realization by realization.
For the transshipment theorems, the book differentiates a density formula by Leibniz's rule. Under the weaker hypothesis stated here, laws without atoms and with finite means, the derivative of in has to be obtained by dominated convergence from the pointwise derivative of a piecewise-linear function whose kinks lie on null sets.
perf is a supremum over a set of reals, nonempty because is feasible when
and , and bounded by ; the demand is nonnegative for every outcome and the
capacity nonnegative in BalancedSystem, and Lemma 7.5 carries these as hypotheses. The
supremum is attained, but the definition does not assert it. Expected performance is a Lebesgue
integral; the demand is integrable by assumption and is -Lipschitz in , so the
integrand is integrable, and a solver must prove this measurability rather than assume it.
Exchangeability is the equality of the laws of and for every
permutation . Designs are finite sets of pairs of Fin n; the chains are defined with
finRotate, so indices wrap modulo and the closing edge of is in the book's
numbering, which is the edge its proofs and Figure 7.3(c) use. Lemma 7.8 involves open chains on
subsystems of sizes and ; these are designs on Fin k evaluated on the first
coordinates of the demand (subDemand, subPerf).
Theorem 7.1 states the optimal costs as infima of the newsvendor cost over all base-stock
levels, on Mathlib's gaussianReal; a nonpositive pooled variance gives a degenerate law, for
which the inequality still holds, so the statement is not trivialized by that convention. The
transshipment theorems take the two demand laws as probability measures on with no
atoms (Theorem 7.2) and finite, positive means; the quantity is defined for all
outcomes and the service levels are probabilities and expectations under the product law.
The definition module is shared by all eleven items. Beyond the milestones, formalizing the
identity (7.30) as its own lemma and the disjoint-union additivity of perf would be natural
contributions.
Procter & Gamble observed in the 1990s that the orders its distributors placed for diapers were far more variable than the retail sales of diapers, and that its own orders to suppliers were more variable still, although the end demand for diapers is about as stable as demand gets. The phenomenon, a growing amplification of variability as one moves upstream in a supply chain, is the bullwhip effect. Lee, Padmanabhan and Whang (1997) argued that it is not a symptom of irrational behaviour: four rational responses of an inventory manager to their own environment each produce it. Chapter 13 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) makes three of the four quantitative, following Chen, Drezner, Ryan and Simchi-Levi (2000) for demand signal processing, Lee et al. for the rationing game, and Cachon (1999) for order batching. This mission formalizes those three models and the theorems the chapter proves about them.
Demand signal processing. A retailer faces a demand process , , that follows the stationary first-order autoregressive model
with a constant , a correlation constant , and errors that are independent variables, each independent of the demands before period . In steady state every has the law . The retailer replenishes with a lead time of periods under a base-stock policy but does not know the demand parameters, so it estimates the lead-time demand from a moving average of the previous demands:
and sets the base-stock level , where
is a safety factor. The book writes the constant in as and does
not give its form; here it is a free parameter . Each period the retailer orders
, which may be negative. In Lean the process is the structure
AR1Demand, whose fields are the parameters, the errors, the demands, the recursion, the
independence properties and the stationary law; muHat, err, sigmaHat, baseStock and
order are the five quantities above.
Order batching. retailers face independent demands in every period and
each orders once every periods, the order being its demand over the previous
periods. The supplier's order in a given period is the total ordered by the retailers whose
ordering day falls in that period. Three patterns are compared: random ordering, in which each
retailer's day is uniform over the days, so the number of retailers ordering on a given
day is binomial; positively correlated ordering, in which all retailers order on the
same day, so with probability and otherwise; and balanced ordering, in which
the retailers are spread as evenly as possible, so with , , is
with probability and otherwise. The structure BatchOrders P N R mu sigma carries the
demands, the ordering count independent of them, and supplierOrder, the sum of the last
demands of retailers ; each pattern enters a theorem as a hypothesis on the law of .
Rationing game. Two identical retailers face single-period demand with distribution function , holding cost and stockout penalty , so the newsvendor quantity satisfies . With probability the supplier can deliver only units in total and allocates them pro rata to the orders, retailer 1 receiving ; with probability supply is unlimited. Retailer 1's expected cost when the retailers order and is
with the newsvendor cost; this is rationingCost.
with equality when . This is bullwhip_signal_processing. The bound exceeds
whenever , whatever the value of : a lead time and a moving-average forecast are
enough to produce the effect.
The chapter's own route to the goal, each a milestone: the steady-state moments (13.2) to (13.4), , and ; the identity ; Lemma 13.1, for ; the vanishing of the cross term (13.12); and the variance of the demand part, .
Order batching, Theorem 13.4: under the three patterns the supplier's order has mean and
through the three variance formulas , and .
The rationing game, Theorem 13.3: if is a symmetric Nash equilibrium, that is, minimizes over positive order quantities when the other retailer orders , then .
The three theorems are the quantitative core of the chapter. Theorem 13.2 is the single-stage building block that Theorems 13.6 and 13.7 later iterate along a serial chain, giving the product-form and the exponential lower bounds on the amplification at stage ; its comparative statics, the bound decreasing in and increasing in , are the basis of the remedies the chapter recommends (shorter lead times, smoother forecasts, sharing point-of-sale data). Theorem 13.4 ranks the ordering patterns and justifies the advice to balance ordering days when batching cannot be avoided. Theorem 13.3 shows that pro-rata rationing alone inflates orders; the book is careful to note that inflated orders are not by themselves inflated variances, and that the variance statement for this model is due to Rong, Shen and Snyder (2017).
None of these results has a machine-checked proof. The book's proofs of Theorems 13.2 and 13.4 are complete but informal, and the proof of Lemma 13.1 is omitted with a citation to Ryan's 1997 thesis; formalizing it requires a self-contained argument. The variance decomposition of and the conditioning argument for Theorem 13.4 are reusable for the multistage results of Sect. 13.2.5, which are natural follow-up missions on the same definitions.
The obvious computation of expands the order into its demand part and its safety-stock part and hopes the cross term disappears. It does, but not for a reason visible in the formulas: is a square root of a sum of squares of forecast errors, a nonlinear function of demands, and its covariance with a single demand is zero only because the errors are jointly Gaussian with mean zero and is an even function of them, so the covariance is the expectation of an odd function of a centred Gaussian vector. That is Lemma 13.1, and the vanishing of the cross term needs two further covariances, and , which the book reduces to the lemma through the recursion (the second reduction divides by ) but which hold for every by the same symmetry. A solver must set up the joint Gaussian structure of the demand vector and prove the odd-function argument; nothing in Mathlib does this directly.
The second obstacle is that the moments (13.2) to (13.4) are not assumed but derived: the structure carries the stationary law of each and the independence of from the past, and the autocovariance has to be obtained from the recursion by induction on the lag, with integrability supplied by the Gaussian laws.
For Theorem 13.4 the work is the conditioning on : given the supplier's order is a sum of independent normals, so its conditional mean is and conditional variance , and the total variance is . The order is defined by a sum over retailers , so the independence of from the demands has to be used through the indicator structure rather than through a conditional-expectation library result.
For Theorem 13.3 the argument is a first-order condition. It requires that the newsvendor cost be differentiable with derivative , which holds when is continuous, and that the symmetric equilibrium be an interior minimizer, which is why and the minimization over are hypotheses.
Time is indexed by so that exists for every . AR1Demand asserts the
recursion for every outcome, the independence of the whole error family, the independence of
from , and the stationary law of every ; these are the
"steady-state" assumptions the book makes in words. The structure is satisfiable: the stationary
Gaussian AR(1) process on a full-measure set of error sequences has all these properties. The
constant is a free real parameter ; no theorem depends on its value.
The goal divides by , which is under the structure's
hypotheses and , so the ratio is a genuine quotient. Mathlib's
ProbabilityTheory.variance and covariance are used; both are the ordinary real quantities
for square-integrable variables, which every variable here is, included.
In BatchOrders the demands are indexed by Fin N × Fin R, the count is a natural-valued
random variable bounded by and independent of the demand family, and supplierOrder sums the
demands of retailers , the book's "without loss of generality" choice. The laws
of are hypotheses on point probabilities P.real {ω | X ω = j}; with each of the
three families of hypotheses is satisfiable by a structure with the corresponding law. The
subtractions and are real.
In the rationing game the demand law is a probability measure on whose distribution function is continuous and strictly increasing on ; the newsvendor loss is assumed integrable at every order quantity. The pro-rata allocation uses Lean's total division, which is never at in the theorem since .
Beyond the ten milestones, the multistage Theorems 13.6 and 13.7 and the centralized-information
bound of Theorem 13.5 are welcome as extensions on the same AR1Demand.
When a system is controlled indefinitely and decisions are frequent — a router admitting packets, a queue accepting jobs, a machine being maintained — discounting future rewards is often unjustified, and what matters is the long-run average reward per period. Puterman's Chapter 8 (doi:10.1002/9780470316887) develops the theory of this criterion, and its central object is a single equation, the average reward optimality equation , whose unknowns are a scalar gain and a bias function . For unichain models, in which every stationary policy generates a Markov chain with one recurrent class, this equation determines the optimal gain and an optimal stationary policy. The results go back to Howard (Dynamic Programming and Markov Processes, MIT Press, 1960) for the recurrent case and to Blackwell (Discrete dynamic programming, Annals of Mathematical Statistics 33, 1962, doi:10.1214/aoms/1177704593) and Derman for the general finite case; Puterman's Section 8.4 proves them through the discounted theory of mission II, by letting the discount factor tend to one.
The model is stationary (Assumption 8.0.1): a finite set of states, for each a finite nonempty set of actions, a reward and transition probabilities , none depending on the decision epoch. A policy may randomize and may depend on the whole history; the deterministic stationary policy applies the decision rule at every epoch. Its transition matrix is .
For a policy , is the expected reward over epochs. Since the limit of need not exist (Example 8.1.1), the chapter works with the lim sup and lim inf average rewards and , and with . A policy is average optimal when for all and , the strongest of the three criteria of Section 8.1.2.
The optimality residual is , and the optimality equation is . A decision rule is -improving when it attains at every state. A transition matrix is unichain when it consists of a single recurrent class plus a possibly empty set of transient states, and the MDP is unichain when is unichain for every deterministic decision rule.
For a finite unichain model: (a) some deterministic stationary policy is average optimal; (b) the optimality equation has a solution, and (d) its scalar satisfies for every ; (c) for every solution, every -improving decision rule gives an average optimal stationary policy.
If then ; if then ; if then .
In a finite unichain model has a solution, and every solution has the same .
If and is -improving, then is average optimal.
Theorem 8.4.1(c) is what the source calls "one of the most important results for average reward models": a solution of the optimality equation with constant pins down the optimal gain under every criterion at once, so that in finite unichain models the three optimality criteria of Section 8.1.2 coincide. Theorem 8.4.3 guarantees such a solution exists, and Theorem 8.4.4 reads an optimal policy off it. Together, Theorem 8.4.5 reduces the infinite-horizon average reward problem over all history-dependent randomized policies to a finite system of equations in , which is what policy iteration, value iteration and linear programming solve in Sections 8.5 to 8.8.
The results are classical and proved. Formalizing them fixes the chain-structure hypothesis in
a checkable form and pins down which criterion "average optimal" means, two places where the
literature is loose. The platform's MarkovDecisionProcesses series has the finite-horizon
(mission I) and discounted (mission II) models; this mission adds the undiscounted stationary
model, the gains, and the unichain classification, on which Chapter 9's multichain optimality
equations and Chapter 10's sensitive discount optimality can be built.
The obvious argument for Theorem 8.4.3 is to take the discounted optimal value of mission II and let . It fails as stated because blows up like ; what converges is the Laurent expansion of the value of a fixed stationary policy, Corollary 8.2.4, and that expansion needs the limiting matrix and the deviation matrix of a unichain chain. So the proof must first develop the Markov chain theory of Section 8.2 and Appendix A, choose a subsequence of discount factors along which one policy is discount optimal (possible because is finite), and only then pass to the limit in the discounted optimality equation.
Theorem 8.4.1 looks elementary and hides the analytic step: iterating along an arbitrary history-dependent policy and dividing by requires the telescoping term to vanish, which uses boundedness of , and requires the reduction from history-dependent randomized to Markov randomized policies (Theorem 8.1.2). For Theorem 8.4.4 the step is Corollary 8.2.7, that forces the gain of to be , which is the multiplication by that annihilates .
The traps are in the definitions. Recurrence and the unichain property must be stated so that the source's Example 8.4.3 comes out as the book says — the policy using has the absorbing state as its single recurrent class — and the optimality residual must use the lim sup / lim inf gains, since a definition through a limit that need not exist would be a junk value on the policies of Example 8.1.1.
State and action spaces are Fintypes and admissible actions are nonempty Finsets, as in
missions I and II; the stationary model is a new structure because mission II's DiscountedMDP
bundles a discount factor, and carries the same data otherwise. Policies are history-dependent
and randomized, so "average optimal" has its full strength; a stationary policy is the
deterministic one built from a decision rule. Expected total reward is defined by the policy
evaluation recursion, as in the earlier missions, rather than through a measure on
trajectories.
Gains are Filter.limsup and Filter.liminf of on ; these are
the source's because the sequence is bounded by , and the suprema over the
nonempty family of policies are genuine real suprema for the same reason. The residual
is a Finset.sup' over the admissible actions. Recurrence is "every state reachable from
reaches " and unichain is "any two recurrent states communicate", the definitions of Appendix
A for finite chains, applied to for every admissible deterministic decision rule.
Restrictions relative to the printed text, all noted in the items: Theorem 8.4.1 is stated for finite where the source says countable, since the chapter's standing assumption and the model are finite; the gain of a stationary policy in (8.4.5) is written as its lim inf gain, which equals it; and the chain of (8.4.6) is stated through and , since presupposes existing limits. Nothing is trivialized: the existential in Theorem 8.4.5(a) has to produce a decision rule, and with a junk maximum is impossible since every is nonempty. Welcome contributions beyond the milestones: Theorem 8.1.2 (reduction to Markov policies), Corollary 8.2.7 (the gain of a stationary policy from the evaluation equations), and the equivalence of the three optimality criteria in finite models.
A decision maker who does not want to be judged by expected loss alone needs a functional that weighs the bad outcomes more heavily than the good ones and still behaves well under optimization: monotone, convex, unchanged by shifting the loss, and scaling with it. Kusuoka's theorem (mission II) says every such law-invariant functional on an atomless space is a supremum of mixtures of Average Values-at-Risk. The mixtures themselves are the distortion risk functionals of Denneberg (Distorted probabilities and insurance premiums, Methods of Operations Research 63, 1990) and Acerbi (Spectral measures of risk: A coherent representation of subjective risk aversion, Journal of Banking and Finance 26, 2002, doi:10.1016/S0378-4266(02)00281-9), also called spectral risk measures: integrals of the quantile function against a nondecreasing density . They are the risk functionals used throughout Pflug and Pichler's book (doi:10.1007/978-3-319-08843-3) in the multistage objectives of Chapters 5 and 6, and the three representations proved in Sections 3.2 to 3.4 — as a supremum over densities , as a maximum over uniform variables, and as an infimum over convex-conjugate constraints — are what make them computable inside an optimization model. This mission formalizes those representations.
Fix a probability space . A random variable is a loss, and the functionals act on , the bounded measurable ones. The Value-at-Risk at level is the lower quantile and the Average Value-at-Risk at level is , extended to by the essential supremum (mission II). A risk functional satisfies the four axioms (M), (C), (T), (H) of Definition 3.2.
A distortion function is a nonnegative, nondecreasing with , and the distortion risk functional with density is
The Average Value-at-Risk is the case . A random variable is dominated by , , when , and for every . A variable is uniformly distributed when on . For the conjugate is .
satisfies (M), (C), (T) and (H).
There is a probability measure on with for all .
For , ; for the latter with the upper bound dropped.
On an atomless space, , the maximum attained.
over measurable .
Theorem 3.16 identifies the conjugate of a distortion functional: is when and otherwise, so is the support function of an explicit convex set of densities. Everything else follows from that. Corollary 3.18 recovers the classical dual of the Average Value-at-Risk and shows that its constraints can be relaxed to the levels in ; Corollary 3.19 turns the supremum into a maximum over couplings and identifies the maximizer, the co-monotone one, which is how distortion functionals are evaluated on scenario trees; Corollary 3.21, not stated here, combines the theorem with Kusuoka's representation to give the dual of every version independent risk functional. Theorem 3.22 goes the other way and writes as an infimum, which is what converts a minimax problem — minimize a supremum over — into a plain minimization over the decision and an auxiliary function , the form in which the book solves risk-averse programs in Chapters 5 and 6.
Everything here is proved in the source and in the cited papers; the platform has the finite-scenario Artzner–Delbaen representation of coherent risk measures but nothing on distortion functionals, and Mathlib has no risk-measure material and no quantile-based representation theory. The definitions of this mission sit on those of mission II and are reused as such.
The obvious route to Theorem 3.16 is Fenchel–Moreau duality: is convex and lower semicontinuous on , so it equals its biconjugate, and the task is to compute . The step where the naive computation stalls is bounding by a quantity that depends only on the distributions of and : this is the rearrangement (Chebyshev, Hardy–Littlewood) inequality , with equality for co-monotone couplings. Given it, , and testing with indicator-type shows the supremum is exactly when the upper-tail averages of are dominated by those of , which is the constraint . Neither the rearrangement inequality nor the identification of the conjugate is available in Mathlib.
For the corollaries the difficulties are concrete. Corollary 3.18 needs to be deduced from the constraints, which the source does by contradiction through the value . Corollary 3.19 needs the co-monotone coupling to exist, which is where the atomless hypothesis enters, and needs to be feasible for (3.15), which uses . Theorem 3.22 needs, besides the inequality from Fenchel–Young, an admissible that nearly attains it; the source builds it from and via Corollary 3.23.
Random variables are functions on an arbitrary measurable space with a
probability measure, exactly as in mission II, whose MemLinfty, valueAtRisk,
averageValueAtRisk, IsRiskFunctional, Atomless and IsKusuokaMeasure are imported and not
redefined. The distortion density is a function on constrained on ; its
integrability on is part of the definition, and both and
integrate over the open interval, which excludes the level where the quantile formula is
not meaningful and changes no value.
Every supremum and infimum is over a subtype of functions satisfying the constraints, and the prose of each item records why the family is nonempty and bounded, so that no real supremum takes its junk value. Pointwise constraints on are almost sure. The constraint of (3.15) is stated for : at the source's expression is and means the limit, and the constraint there is implied by the others; (3.19) at is stated separately with the upper bound dropped. The conjugate takes values in the extended reals, and admissibility in Theorem 3.22 requires finite almost everywhere, integrable, with integral at most , and integrable — the conditions under which the expectations in (3.24) are the integrals the source means.
Two hypotheses are added beyond the printed statements and are flagged in the items: atomless for Corollary 3.19, because otherwise no uniform variable need exist and the maximum would be over an empty set; and integrability of in Theorem 3.22, without which Lean's integral of a non-integrable is . Theorem 3.16 itself carries no atomless hypothesis, and the mission notes check the identity on two-point spaces by hand. A trivializing formalization — a constraint set that is empty or unbounded, so that the supremum is — is excluded by the constant density , feasible for every , and by .
Welcome contributions beyond the milestones: Corollary 3.15 (the representation through the distribution function for ), Corollary 3.21 (the dual of a version independent risk functional through its Kusuoka set), Corollary 3.23, and the explicit mixing measure (3.12).
Introductory physics is normally taught as a sequence of unrelated chapters — kinematics, dynamics, energy, optics, gravitation — each with its own rules. A recurring proposal in physics education is to teach instead from a single organising statement: among all conceivable histories of a system, the one realised in nature is the one that makes a certain integral, the action, stationary. Edwin Taylor's editorial A Call to Action (American Journal of Physics, 2003) argued for building the first-year curriculum on it; Lachlan McGinness and Craig Savage reported classroom results for such a course at the Australian National University (Action physics, American Journal of Physics, 2016); Massimiliano Malgieri tested a sum-over-paths treatment in an Italian secondary school (2017).
The source monograph for this mission, Julliana Rodrigues Martins, A Ação Estacionária como Eixo Unificador do Ensino de Física no Ensino Médio (Trabalho de Conclusão de Curso, Universidade Federal do Ceará, 2025), develops this programme for secondary education. Its Chapters 2 and 3 are quantitative: they follow the historical line from antiquity to the nineteenth century and carry out every calculation in full. This mission formalises that quantitative core, and nothing of the pedagogical Chapter 4.
The historical line the monograph reconstructs, and which the milestone list follows:
Fix real endpoints and an integrand , a real-valued function of three real arguments. A path is a function , and its action over is
Neighbouring paths are produced by an admissible variation: a twice continuously differentiable with , giving the family . The path is stationary when
Writing and for the partial derivatives of in its first and second slots, the Euler–Lagrange expression along is
In mechanics one takes , and , so that stationarity of is Hamilton's principle and is the Lagrange equation of motion.
For , twice continuously differentiable in all three arguments and twice continuously differentiable, if is stationary for then
This is equation (3.9) of the monograph, and — through the substitution , , — equation (3.17). It is stated as the weakest stable form: stationarity, not minimality, and an arbitrary admissible integrand rather than a particular Lagrangian.
The supporting statements are the analytic ingredients of that derivation (the fundamental lemma, the first variation formula, the first integral for a cyclic coordinate), its two mechanical applications worked out in the monograph (harmonic oscillator, plane pendulum), its geometric application (shortest path), and the historical minimisation problems of Chapter 2 (Heron, Galileo, Fermat, Maupertuis).
The Euler–Lagrange equation is the bridge the whole unification argument rests on: once it is available, Newton's second law, the pendulum equation, Snell's law, geodesics and conservation laws all become consequences of one statement about an integral, which is exactly the claim the monograph makes to justify teaching physics this way. The Chapter 2 statements are the historically prior special cases, each obtained by a one-variable minimisation rather than by the general machinery, and together they exhibit how far elementary optimisation alone reaches before the calculus of variations is needed.
What this mission adds beyond the source is a machine-checked version of an argument that, in every textbook presentation including this one, is carried out at the level of rigour of formal manipulation: the interchange of differentiation and integration is performed without justification, the passage from a vanishing integral to a vanishing integrand is asserted, and the regularity needed for to exist is left implicit. All of it is true under the stated hypotheses; none of it is proved in the source. Mathlib has the analytic infrastructure (interval integrals, differentiation under the integral sign, smooth bump functions) but, at the environment pinned for this mission, no Euler–Lagrange equation and no calculus-of-variations layer built on it. The definitions published here — action, admissible variation, stationary path, Euler–Lagrange expression — are reusable by any later variational mission.
The obvious argument is three lines: differentiate under the integral sign, integrate by parts, and conclude that the integrand vanishes because is arbitrary. Each line is where the work is.
Differentiating under the integral sign needs a dominating bound valid uniformly for near ; it is available here because the data are and the interval is compact, but it has to be produced. The integration by parts needs to be differentiable, which is where the second derivative of and the second derivatives of are consumed — a path is not enough for this formulation. The final step needs test functions: a bump supported in a small interval around a point where the continuous coefficient is nonzero, which is why the fundamental lemma is a separate milestone rather than a step.
A standing trap in the Lean formulation is that deriv returns at points where a function is not differentiable, so a statement about can be accidentally true for the wrong reason unless the regularity hypotheses are genuinely strong enough. Every statement here carries the hypotheses that make each derivative a real derivative.
The development is one-dimensional and real: paths are , the integrand is a curried with argument order matching the source's , and all integrals are interval integrals over . Partial derivatives are one-dimensional derivatives in the frozen remaining arguments; smoothness of is stated for its uncurried form on . Regularity is throughout — for the integrand, for the path, and for the variations — matching the monograph's requirement that have continuous first and second derivatives.
Stationarity is a hypothesis quantified over all admissible variations, so the goal cannot be satisfied by exhibiting one convenient ; and the conclusion is an equation at every point of the closed interval, not almost everywhere, so it cannot be weakened to a null-set statement. The mechanical milestones are stated as equivalences between the Euler–Lagrange equation for the explicit Lagrangian and the classical equation of motion, which rules out a one-directional reading that would be vacuous for a path that never satisfies either.
Physical constants (, , , , the speeds ) are free real parameters, with positivity or non-vanishing assumed only where the source's conclusion requires it — the pendulum equivalence divides by , so and appear, while the oscillator equivalence needs no such assumption. Angles never appear as primitive objects in the optics milestones: the sines of the incidence and refraction angles are written as the ratios that the figures define them by, so no convention about angle ranges is smuggled in.
Contributions welcome: proofs of any milestone, and reusable infrastructure for differentiation under the interval integral sign and for bump functions with prescribed support, both of which are of use well beyond this mission.
A sum of independent random increments is a basic model for accumulated noise. A continuous Gaussian process offers a different description of that noise, one that can be studied at every nonnegative time. To compare their individual trajectories, both objects must live on the same probability space. The question is whether their paths can remain close over a whole finite range of observation times, with a quantitative bound on the chance of a large discrepancy. Ethier and Kurtz state such a result for independent sums in Chapter 7, Section 5, Theorem 5.1 of Markov Processes: Characterization and Convergence, printed page 356.
Let be a probability measure on the real line. Assume that it has finite exponential moments in a neighborhood of zero: there is such that
This hypothesis controls both tails of the distribution. In particular, its mean and variance are finite. The distribution need not be centered, symmetric, bounded, or have positive variance. Let denote independent random variables each with distribution , and write for their partial sums.
A Brownian motion with drift and variance rate can be written as , where is standard real Brownian motion and is the nonnegative square root of the variance. When , this expression gives the deterministic path . A coupling specifies a joint probability law for the entire sequence and the Brownian path while preserving their required individual laws. The sequence coordinates are independent of one another; independence between the sequence and the Brownian path is not part of the requirement.
Theorem 5.1 asserts that a coupling and positive constants , depending only on , exist such that
for every integer and every real . Both inequalities displayed here are strict. One joint construction works simultaneously for every horizon and every positive excess ; neither the coupling nor the constants are chosen anew after those parameters are specified. At , the logarithmic term is zero, so the same assertion controls the discrepancy at the first observation time.
The mission consists of this full theorem. The rescaling and Poisson consequences discussed later in the section are outside its target. There are no separate supporting theorem milestones in the accepted grouping.
The estimate controls the largest discrepancy among all partial sums up to a specified horizon. Its deterministic threshold grows logarithmically with that horizon, and its remaining tail decreases exponentially with the excess above the threshold. This makes the theorem a quantitative comparison of trajectories on a common space. The opening of Section 5 identifies strong approximation of independent sums as its subject and introduces approximation of the Poisson process as a subsequent consequence.
The mathematical result is a known theorem stated by Ethier and Kurtz. The present formal target asks for a checked proof of that statement, including the existence of its coupling. The statement is supplied with an unproved theorem body; no proof of the strong approximation estimate is asserted here.
The prescribed marginal laws do not themselves determine the joint relationship that makes the paths close. The construction must preserve independence within the entire increment sequence and the Brownian finite-dimensional laws while also satisfying a maximal estimate for every finite horizon. A comparison of the distributions at one terminal time does not supply these simultaneous path requirements. The exponential tail and the uniform choice of constants are both part of the goal.
The common carrier is a pair consisting of a real sequence indexed by natural numbers and a continuous real path indexed by nonnegative real times. A probability measure on this carrier is the unknown coupling. Its first coordinate at index zero represents , so summing over the first natural indices represents exactly. Its second coordinate is standard Brownian motion; the affine expression supplies the general drift and variance.
The finite maximum event is expressed by the existence of an integer with whose error exceeds the threshold. This avoids any convention for a maximum of an empty set. Exponential integrability supplies the finite moments needed for the mean and variance. The probability bound uses the nonnegative extended-real embedding of the positive finite quantity . The formal statement retains the full exponential-moment class, including point masses. Existing probability-measure, independence, law, Brownian-motion, and variance definitions supply the mathematical vocabulary.
Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986 (held reprint copyright 1986/2005), Chapter 7, Section 5, Theorem 5.1 and equation (5.1), printed page 356; local source PDF page 365. The book title and authors are recorded on local PDF page 2.
Hubble's law — officially the Hubble–Lemaître law — is the observation that galaxies recede from us at a speed proportional to their distance, . It is the first observational basis for the expansion of the universe and one of the standard pieces of evidence cited for the Big Bang model. Georges Lemaître derived the proportionality from relativistic cosmology in 1927; Edwin Hubble published the observational relation in 1929, building on Vesto Slipher's redshifts and Henrietta Swan Leavitt's Cepheid distance scale. Alexander Friedmann had already shown in 1922 that the Einstein field equations admit expanding solutions, with an expansion rate governed by what is now called the scale factor.
Behind the astronomy sits a piece of elementary mathematics that is rarely written out in full: in a spatially homogeneous expansion, the linear velocity–distance relation is forced, it holds with the same constant for every observer, and the Hubble "constant" is in fact a function of time whose evolution is fixed by a single dimensionless parameter. This mission formalizes that kinematic core: the statements are about the scale factor and its derivatives, and involve no Einstein equations.
A scale factor is a function of cosmic time . A comoving point is labelled by a fixed coordinate (with the Euclidean norm), and its proper position at time is
The proper distance between the comoving points and is
The Hubble parameter and the dimensionless deceleration parameter are
denotes the present-day value of ; the name "Hubble constant" refers to the fact that is constant in space at a fixed time, not in time.
The goal theorem is the idealized Hubble law, stated in the source as a theorem of Euclidean geometry: any two points moving away from the origin, each along a straight line and with speed proportional to its distance from the origin, move away from each other with a speed proportional to their distance apart. Formally, for , a time and curves with
the separation satisfies
The relative velocity is parallel to the separation vector and its magnitude is times the separation, with the same for every pair — so no comoving observer occupies a distinguished centre of the expansion.
The milestones supply the cosmological content that surrounds this geometric fact:
The result itself is elementary but load-bearing: it is what licenses reading a linear redshift–distance diagram as evidence for uniform expansion rather than for a privileged position in space, and items 4–6 are the statements through which cosmological observations (the sign of , the approach of to in CDM) are turned into claims about the past and future behaviour of and .
Formalizing it produces a small, reusable Lean layer for expansion kinematics: the scale factor, the Hubble and deceleration parameters, proper position and proper distance, with the differentiation lemmas that connect them. The platform already carries Friedmann-equation missions that fix the dynamics of ; this mission is the kinematic complement, and its Hubble parameter is the same function that those developments use. Nothing here is an open research problem: every statement is a known textbook fact, and the work is the formalization.
The mathematical content is a few lines of calculus, so the difficulty is entirely in the encoding. Three places are easy to get wrong. First, proper distance is defined through a norm, so the identity needs positivity of , and differentiating it needs positivity on a neighbourhood, not just at the point. Second, is defined by a quotient with in the denominator: in Lean division by zero returns zero, so a statement about that forgets silently changes meaning. Third, milestone 5 propagates a hypothesis stated on down to the endpoint , where the Big Bang condition lives; the continuity argument at the endpoint is the only step with any technical content.
Time is and space is EuclideanSpace ℝ (Fin 3); derivatives are Mathlib's
deriv / HasDerivAt, so "velocity" is always a derivative at a point rather than a
difference quotient. Smoothness is assumed exactly where it is used: differentiability at a
single time for the first-order statements, ContDiff ℝ 2 for the statements involving
. Positivity of the scale factor is stated explicitly wherever it is needed, as is
in the statements mentioning .
Degenerate readings are excluded: the goal's hypotheses are satisfiable (any pair of comoving points in an expanding universe satisfies them, as milestone 2 shows), and the milestones are non-vacuous for concrete scale factors such as and . The goal theorem's second clause is a norm identity that is true for every ; it carries the "speed proportional to distance" half of the source's statement, while the first clause carries the "moving away from each other along the separation" half.
The definition layer is a single self-contained file (scale factor derived quantities, proper position, proper distance); it is reusable by any mission about expansion kinematics. Contributions of the milestone proofs, and of variants such as the redshift relation derived from null geodesics rather than assumed, are welcome.
Battery-powered and energy-harvesting wireless devices cannot treat transmission power as free: a control algorithm that maximizes throughput without regard to energy will drain a device long before the network's other resources are exhausted. Chapter 6 of Georgiadis, Neely & Tassiulas's survey Resource Allocation and Cross-Layer Control in Wireless Networks (Foundations and Trends in Networking, 2006) extends the drift-plus-penalty framework of Chapter 5 to problems with an explicit average-resource-budget constraint, and works out the Energy Constrained Control Algorithm (ECCA) of Neely [116] as its flagship example: a joint flow-control and power-allocation policy that keeps every data queue and a virtual "excess energy" queue bounded by an explicit, finite constant on every single time slot — not merely in expectation or in the long run.
A multi-user wireless downlink serves users over channels with a time-varying collective topology state and link rate function under power allocation , subject to a per-slot power budget and a target average power constraint . Exogenous arrivals are entirely admitted or entirely dropped each slot (no transport-layer storage). The ECCA algorithm runs, every slot: flow control — admit into queue if (a fixed parameter), otherwise drop it entirely; power allocation — choose to maximize subject to the power budget, where is a virtual power queue tracking accumulated excess energy expenditure, updated by .
where is the constant in the rate function's marginal-benefit inequality ( being with its -th entry zeroed). These bounds hold for every topology state process and every admissible arrival process , on every sample path — the weakest, most general level, with no distributional assumption whatsoever on either process.
Theorem 6.3 gives a hard, deterministic worst-case guarantee — every queue in the system, actual or virtual, is bounded by an explicit closed-form constant on every single slot, not merely on average or asymptotically — which is exactly the kind of guarantee a resource-constrained embedded or battery-powered device needs: a device can be provisioned with buffer and battery-reserve capacity of the theorem's own , and know, with certainty rather than in expectation, that it will never overflow. The corollary that no -slot interval spends more than in energy translates directly into a battery-lifetime guarantee. This is also, methodologically, the one point in the whole book's drift-plus-penalty method where an elementary induction — not a probabilistic Lyapunov drift argument — suffices, because ECCA's flow control rule directly caps regardless of what the channel or arrivals do.
Formalizing it. No result in this mission has a machine-checked proof anywhere; nothing adjacent exists on the platform (searched for virtual queue, energy-constrained control, power allocation — no faithful hits; one unrelated coincidental keyword match in a neural-coding combinatorics item was checked and is not relevant). This mission is the first formalization of the ECCA performance guarantee.
The obvious first idea is to bound and by unrolling their recursions and applying a probabilistic drift argument, as in every other capstone in this series. This is unnecessary and would in fact obscure the actual mechanism: follows from a two-case induction that needs no probability at all — if , the flow control rule admits at most more, giving ; if , flow control drops everything, so by the induction hypothesis. The harder part is : it requires connecting the virtual queue's own accumulation to the fact that the power-allocation optimization (6.14) will stop spending power on link once grows past — a consequence of 's optimality for (6.14) together with the -inequality on , not a property one can read off the -recursion alone.
The power-allocation rule is stated as an explicit optimality hypothesis (hPopt): for every
competing power vector respecting the budget, the objective (6.14) at the chosen is at
least as large — the faithful rendering of " is chosen to maximize (6.14)" without needing
Lean's argmax/IsMaxOn machinery. The rate function's -inequality is stated exactly as
the book gives it, using Function.update P i 0 for . Out of scope for this mission:
the throughput conclusion under i.i.d. (an expectation/liminf statement, unlike the
rest of this theorem, needing the same conditional-expectation machinery as the other chapters'
capstones) and Theorem 6.2 (the general GCLC framework this specializes, which needs Assumptions
1-4's four simultaneous existential clauses over an "S-only" policy) — both left for a future
mission. A trivializing formalization to rule out: weakening the two sample-path conclusions to a
limsup/expectation-style bound (the convention used elsewhere in this series) would misstate
this theorem, whose entire distinguishing content is that the bounds hold for every time slot
and every sample path, not merely in the long run.
Chapters 3-4 of Georgiadis, Neely & Tassiulas's survey Resource Allocation and Cross-Layer Control in Wireless Networks (Foundations and Trends in Networking, 2006) answer "can the network stay stable?" — the backpressure algorithm's throughput optimality (Theorem 4.5) says yes, for any arrival rate inside the capacity region. But networks are usually operated with plenty of unused capacity precisely so that they can also serve a second goal: maximizing some concave utility (throughput, fairness, revenue) of the rates actually delivered. Answering "how close to utility-optimal can a stable policy get, and at what congestion cost?" needs a single theorem that treats stability and utility optimization in one drift analysis. Theorem 5.4, adapted from Neely, Modiano & Li [108], Georgiadis, Neely & Tassiulas [115] and Neely [116], is that theorem, and it is the technique — "Lyapunov optimization" or "drift-plus-penalty" — behind a large fraction of the cross-layer control literature that followed this book.
A network of queues has backlog vector , and a -dimensional control process influencing the system's dynamics (e.g. admitted data rates). For any nonnegative function of the backlog vector, the one-step Lyapunov drift is , the expected one-slot change in conditioned on the current backlog. Given any scalar-valued concave utility function of a -dimensional rate vector and an arbitrary target value , the goal is to stabilize while making the time-average utility of close to . The time-average rate vector is (5.18), and the achieved long-run utility is .
The most abstract drift lemma in the whole book: are arbitrary scalar processes, not necessarily linear or even a function of .
This is the weakest, most general level — a drift-minus-utility condition, checked against an arbitrary target , with no reference to any specific control policy.
Theorem 5.4 is the abstract engine that every concrete utility-maximizing algorithm in the rest of the chapter (the CLC1 joint flow-control/routing/scheduling algorithm of Theorem 5.1, and its robustness variant under approximate scheduling, Corollary 5.2) instantiates by exhibiting a control rule whose per-slot decision satisfies (5.19) for some — the drift condition does the work of turning a per-slot optimization rule into a global performance guarantee. Its tradeoff (utility gap shrinks like , congestion grows like ) is the quantitative signature of every "Lyapunov optimization"/"drift-plus-penalty" algorithm in the cross-layer control literature that followed this book, making Theorem 5.4 the single result a reader needs to understand that entire family of algorithms at once, independent of which specific control problem it is applied to.
Formalizing it. No result in this mission has a machine-checked proof anywhere; nothing adjacent exists on the platform (searched for Lyapunov optimization, drift-plus-penalty, utility fairness, concave utility — no hits at all, not even an adjacent object). This mission is the first formalization of the book's utility-optimization engine.
The central subtlety, flagged explicitly by the book's own notation, is that (5.20) and (5.21) compare two different kinds of quantity that are easy to conflate: is a limsup of an expectation of utility, , while in (5.21) is the utility evaluated at the time-averaged expected rate. Jensen's inequality (using 's concavity) is exactly what would relate to — and it is not proved or needed by this theorem's own statement, only by later results that connect the two more tightly. A formalization that silently merges these into one "utility" quantity would be proving something the book does not claim. The second trap is the target : it is a free parameter of the hypothesis, not the true optimal utility — the theorem's strength is exactly that it says nothing special about how was chosen, so a formalization must not add a hidden side condition forcing to equal a genuine optimum.
∆(U(t)) is restated locally in this chunk's own sub-namespace (drafts cannot import chunk
04-backpressure's copy), via Mathlib's condExp on the σ-algebra generated by the current
backlog vector, exactly as in Chapter 4. Explicit Measurable/Integrable guards on U, R,
g∘R and every drift term prevent condExp/∫ from silently defaulting to 0 (a trivializing
formalization this mission rules out: without these guards, a non-integrable process would satisfy
the hypotheses vacuously and "prove" a stability/utility conclusion for a process that is not
actually controlled). r(t) and \bar g are written inline as their defining Cesàro averages
rather than as separate named definitions, since each is used exactly once. Out of scope for
this mission: Theorem 5.1 (the CLC1 algorithm's concrete instantiation), Corollary 5.2 (the
robustness-to-suboptimal-scheduling variant), and Lemma 5.5 (continuity of near-optimal solutions,
which needs the capacity region Λ as a hypothesis object). All three need substantially more
setup (a named algorithm, or the capacity-region machinery of Chapter 3) than this session's time
budget allowed without approximating either — left for a future mission rather than approximated.
Every stability result in Georgiadis, Neely & Tassiulas's survey Resource Allocation and Cross-Layer Control in Wireless Networks (Foundations and Trends in Networking, 2006) — the throughput optimality of the dynamic backpressure algorithm (Theorem 4.5), the utility-optimal Lyapunov drift bound of Chapter 5, the energy-constrained control algorithm of Chapter 6 — is proved the same way: exhibit a drift condition on a quadratic Lyapunov function of the queue backlog vector, then invoke one fixed abstract lemma to conclude stability and an explicit congestion bound. That fixed lemma, Lyapunov drift stability (Lemma 4.1, adapted from Kingman [67], Loynes [87] and Neely, Modiano & Li [110]), is the engine this mission formalizes — the single result the rest of the book's algorithm-specific theorems are instances of.
A network of queues has backlog vector process on slots , on a common probability space . The quadratic Lyapunov function is . A single queue's backlog sequence (read as ) is strongly stable if ; a network is strongly stable if every one of its queues is. The conditional drift of given the current backlog vector, , measures how the aggregate squared backlog is expected to change over one slot, conditioned on where the network currently is — formalized via Mathlib's conditional expectation on the -algebra generated by .
This is the weakest, most general level: a bounded-outside-a-compact-region drift condition implies both a qualitative stability conclusion and a quantitative congestion bound, with no mention of any particular algorithm, arrival distribution, or network topology.
Lyapunov drift stability is the one lemma every later result in this book's method reduces to: Chapter 4's own Theorem 4.5 (backpressure throughput optimality) applies it directly to the dynamic backpressure algorithm's per-slot optimality property; the book explicitly notes ("This drift inequality is in the exact form for application of the Lyapunov drift lemma... proving the result", p. 57) that once a drift bound of this shape is established, the stability conclusion is free. The T-slot version (Lemma 4.2) extends the reach of the method to settings — Markov-modulated channels, non-i.i.d. arrivals — where no single slot need have negative drift.
Formalizing it. No result in this mission has a machine-checked proof anywhere; nothing adjacent exists on the platform (searched for Lyapunov drift, max-weight, differential backlog, backpressure — the one Lyapunov-drift hit, a Foster-Lyapunov hitting-time bound for a finite-state MDP with an absorbing target state, is a different mathematical object from a vector queue backlog with no absorbing state, and is not reused). This mission is the first formalization of the book's stability engine.
The obvious first idea is to bound directly via the one-step queueing recursion and telescope. This fails for the same reason it fails in Chapter 3: expectation does not commute with . Lemma 4.1's actual content is a genuine Foster–Lyapunov drift argument on the aggregate quadratic quantity , not a per-queue linear one — the quadratic form is what turns a one-sided drift condition into a bound on itself (via the elementary inequality of Lemma 4.3, which converts the linear queueing recursion into a quadratic one that the drift condition directly controls). A second trap is conditioning: the drift bound is conditioned on the current backlog vector , not on the full history — a weaker, memoryless form of conditioning that is exactly what makes the lemma apply uniformly to i.i.d., Markov-modulated, and adversarial channel processes alike, provided the algorithm itself is memoryless in the state.
The Lyapunov-drift hypothesis conditions on the σ-algebra generated by the current backlog vector,
MeasurableSpace.comap (U t) inferInstance, via Mathlib's condExp; explicit Measurable/
Integrable guards on U t and on the drift term prevent condExp/∫ from silently defaulting
to 0 for a non-measurable or non-integrable process (a trivializing formalization this mission
rules out: without those guards, an arbitrary non-integrable backlog process would satisfy the
drift hypothesis vacuously and "prove" the theorem for a process that manifestly is not stable).
The limsup ≤ B/ε conclusion is stated as ∀ t, (Cesàro average at t) ≤ B/ε rather than via
Mathlib's Filter.limsup, matching the standard telescoping proof (which bounds the average for
every t, not merely eventually) and avoiding Filter.limsup's junk value on an unbounded
sequence in the non-complete lattice ℝ. Out of scope for this mission: the algorithm-specific
Theorem 4.5 (dynamic backpressure throughput optimality) and Lemma 4.4 (the single-queue corollary
via admissible processes) — the former needs the book's named algorithm plus Chapter 3's capacity
region restated as a local hypothesis and the explicit constant B of Eq. (4.12); the latter needs
this chunk's own restatement of Chapter 3's admissibility structures. Both are left for a future
mission with a larger time budget rather than approximated.
Every wireless network control algorithm — routing, scheduling, power control, admission control — is ultimately judged against one question: which traffic loads can it keep stable? Answering that question requires a precise, algorithm-independent notion of queueing stability under random arrivals and a randomly time-varying, possibly non-ergodic-looking channel. Tassiulas & Ephremides (1992) and Neely, Modiano & Rohrs (2005) developed the framework used throughout Georgiadis, Neely & Tassiulas's survey Resource Allocation and Cross-Layer Control in Wireless Networks (Foundations and Trends in Networking, 2006): "strong stability" of a queue backlog process, defined purely through the time-averaged expected backlog, with no assumption that the arrival or service process is stationary, Markov, or even has a well-defined long-run average. The present mission formalizes the chapter's foundational single-queue results — the two structural facts every later network-wide capacity and control result in the book is built from.
A queue is described by three processes on slots : an arrival process (new bits admitted at the end of slot ), a service process (the transmission rate offered during slot ), and the backlog , evolving by the queueing law
The queue is strongly stable if its expected backlog has a bounded time average, . An arrival process is admissible with rate if (i) its time-average expected rate is , (ii) its second moment conditioned on the history is uniformly bounded, and (iii) for every there is an averaging window over which the conditional average rate exceeds by at most , uniformly in the starting time — a robust substitute for "the rate is exactly " that holds for i.i.d., Markov-modulated, and burstiness-constrained arrivals alike. A service process is admissible with rate analogously, with a deterministic pointwise upper bound in place of the second-moment condition. Both notions are formalized here on a filtered probability space , with the history of slots exactly as the book's own .
This is the chapter's central single-queue result: it converts the purely structural notion of strong stability into the one comparison — arrival rate versus service rate — that every later capacity-region and control-algorithm argument in the book reduces to.
This is the elementary real-analysis fact — no admissibility, no probability beyond an already-given expectation sequence — that underlies the necessity half of Lemma 3.6's proof.
Strong stability and the admissibility framework are the load-bearing definitions of the entire book: every later chapter's algorithm-performance theorem (Chapter 4's backpressure throughput optimality, Chapter 5's utility-optimal Lyapunov drift bound, Chapter 6's energy-constrained control) is a theorem about when its induced queues are strongly stable, and every one of those proofs cites Lemma 3.6 (or its network generalization, Theorem 3.8's capacity region) as the final step converting a drift bound into a stability conclusion. Formalizing it fixes, once for the whole series, the precise real-analysis and conditional-expectation content of "arrival rate below service rate implies stability" that a Prove2Me solver would otherwise have to reconstruct from scratch for each downstream chapter.
Formalizing it. No result in this mission has a machine-checked proof anywhere; nothing adjacent exists on the platform (searched for strong stability, admissible arrival process, Lyapunov drift, network capacity region — the one hit, a Foster–Lyapunov hitting-time bound for a finite-state MDP, is a scalar drift-to-a-target-state object, not a queue-backlog vector with no absorbing state, and is not reused). This mission is the first formalization of either result.
The obvious first idea for the sufficiency half (b) is to try to bound directly by unrolling the queueing recursion and taking expectations termwise. This fails immediately: expectation does not commute with , so in general — the whole reason admissibility's second-moment and -slot averaging clauses exist is to control exactly this gap between the pathwise recursion and its expectation, via a genuine (non-elementary) drift argument. The necessity half (a) has the opposite trap: it is tempting to prove from a single-slot expectation inequality, but a queue can be strongly stable while oscillates on any finite window, so the argument has to go through the time-averaged (Lemma 3.3) quantity, not a slot-by-slot one.
Admissibility's conditional-expectation clauses are stated with Mathlib's Filtration ℕ and
condExp (P[f | 𝓕 t]), following this platform's established idiom for martingale-difference
hypotheses. Every conditional or plain expectation in a defining clause carries an explicit
Integrable guard, because Mathlib's Bochner integral and condExp both silently default to 0
on a non-integrable function — without the guard, a process with an undefined or infinite second
moment would satisfy admissibility vacuously, which is not the book's assumption (the book assumes
these moments are finite; it never derives it). Lemma 3.3 is formalized directly on the real
sequences representing , , —
exactly the content the book's own statement and proof use, with no further probabilistic
structure, since the lemma's hypotheses and conclusion never mention anything but these
expectations. Out of scope for this mission: the network-wide capacity region (Definition 3.7,
Theorem 3.8, Corollaries 3.9-3.10) and the graph-family construction /
of §3.2-3.3. Faithfully formalizing " is stably supportable by the network" requires
embedding admissible-process realizations into a full multi-queue routing model, which is
substantially heavier than either result formalized here and was left out entirely — per this
series' faithfulness-over-coverage rule — rather than approximated by, e.g., dropping the
second-moment or -slot clauses of admissibility, which would silently change what "admissible"
means. A trivializing formalization to rule out: defining AdmissibleArrival/AdmissibleService
without the Integrable guards above would make Lemma 3.6 provable by choosing a non-integrable
process, which is not the book's theorem.
Independent sums are a basic model for accumulated random fluctuation. A central limit theorem describes their distribution at one large time, and a functional limit theorem describes weak convergence of a rescaled path. Strong approximation asks for substantially more: construct the sums and a Brownian motion on one probability space so that their paths remain close, with an explicit error bound that holds simultaneously over all earlier integer times. Such a coupling turns Brownian path estimates into quantitative information about random walks and independent sums.
Chapter 7, Section 5 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence (Wiley, 1986) states this strong approximation result as Theorem 5.1. Its estimate has logarithmic deterministic error and a strictly exponential tail. The theorem is known as a Komlós–Major–Tusnády type approximation, but the mission follows the exact formulation and hypotheses printed by Ethier and Kurtz.
Let be a probability measure on . The hypothesis requires an such that
Thus the moment-generating integral is finite on a neighborhood of zero. No centering, symmetry, bounded-support, or positive-variance assumption is made.
The conclusion constructs one probability space carrying an iid sequence with common law and a Brownian motion . The Brownian motion has drift and variance chosen to match one summand:
Writing , both and are evaluated on this same space. The theorem does not require the iid sequence to be independent of the Brownian coordinate; their dependence is precisely what permits a close coupling.
There are positive constants , , and , depending only on , such that for every integer and every real ,
Both inequalities are strict: the discrepancy event uses and its probability is . The constants and the entire coupling are chosen before and . The logarithmic term is retained at , where .
The Lean statement uses sequence coordinates indexed from zero, so coordinate represents the source variable and Finset.range k is exactly the sum of the first variables. An existential index with expresses the finite maximum event without replacing either strict inequality.
Weak convergence compares distributions after rescaling and does not place a prelimit sum and its limiting process on the same sample point. This theorem instead supplies a simultaneous pathwise comparison through a common-space construction. The exponential tail quantifies the chance that the uniform error up to time exceeds the logarithmic scale by an additional amount .
The formal statement records the complete coupling rather than only its consequence for normalized terminal sums. It exposes the iid coordinate laws, mutual independence of those coordinates, the Brownian law, the moment-matched affine scaling, the positivity and quantifier order of the constants, and the exact maximal-error event. This is a statement-only formalization: the theorem remains an open Lean goal, and no proof claim is made.
Matching a single sum to a Gaussian random variable is not enough. The construction must coordinate every partial sum with one Brownian path, uniformly over all , while keeping the error logarithmic and the excess probability exponentially small. Independent coupling at each time would destroy consistency across times, while an ordinary invariance principle gives convergence in distribution without the stated finite- tail. The difficulty is therefore the joint construction with all of these quantitative requirements at once.
The common carrier is the product of a real sequence space with the subtype of continuous functions from nonnegative real time to . A probability measure on that carrier is the joint law. iIndepFun asserts mutual independence of all sequence coordinates, and HasLaw gives each coordinate the law . IsBrownianReal specifies the standard Brownian second coordinate.
The Brownian motion appearing in the estimate is defined from that standard coordinate by
This representation covers the zero-variance case: then the scaled Brownian fluctuation vanishes and is deterministic, while the auxiliary standard Brownian coordinate may still be present on the common carrier. The exponential-moment hypothesis supplies the intended finite first and second moments. Probabilities use extended nonnegative reals, and the finite positive real bound is embedded with ENNReal.ofReal.
No local auxiliary definition is expression-essential: all objects in the theorem are provided by Mathlib. The mission intentionally excludes the section's rescaling observations and Poisson corollaries, which do not form separate capstone goals in the accepted grouping. Useful future contributions include the proof of this exact common-space theorem and reusable coupling infrastructure that preserves strict tail estimates.
The group Steiner tree problem generalizes the ordinary Steiner tree problem: given a rooted tree and several groups of vertices, find a minimum-cost subtree that connects at least one vertex of each group to the root. It is a canonical instance of the generalized-connectivity family this survey studies in Chapter 11 — a family that also contains the online set-cover problem (Chapter 5 of this series) as a special case. Buchbinder and Naor's chapter shows how to convert the celebrated offline randomized-rounding algorithm of Garg, Konjevod and Ravi [56] into an online one, by imitating its per-edge coupling structure one iteration at a time as the online fractional solution (obtained from this survey's own Chapter 4 framework) evolves. This mission formalizes that online rounding scheme's three defining probabilistic guarantees and the resulting competitive-ratio theorem.
Fix a rooted tree T = (V, E, r) with non-negative edge costs c : E → ℝ, and k groups
g₁, …, g_k ⊆ V, each request (r, gᵢ) arriving online. An online covering algorithm (from
Chapter 4's framework, applied to the LP relaxation of this connectivity problem) maintains a
monotonically increasing fractional weight w : E → ℝ on the edges, reinterpreted so that wₑ
is the maximum flow that can be routed through e to any vertex of its subtree — a technical
substitution needed so weights are monotone non-increasing along any root-to-leaf path, the
property the rounding algorithm requires. At the end of each iteration in which some weights are
augmented from w to w' = w + δ, the rounding algorithm processes every edge e with
δₑ > 0, in topological order starting from the root, and randomly decides whether to add it to
a growing random edge-cover C ⊆ E: deterministically, if w'ₑ > 1; via a single coin flip, if
e is incident to the root or its parent edge's inclusion in C is already certain; via a coin
flip conditional on the parent edge already being in C, otherwise. Because a coin is only ever
flipped for a child once its parent is (or is already known to be) in C, C always induces a
connected subtree containing the root.
Theorem 11.4 (the goal, p. 231): there is a randomized online algorithm for the group Steiner
problem in trees with competitive ratio O(log²n log k), where n is the number of leaves. It
is built by running T independent trials of the rounding scheme in parallel and taking the
union of the resulting covers, for T chosen (this mission's own explicit derivation — the book
gives only the narrative "we run O(log k log N) independent trials... using simple
probabilistic analysis") so that every group fails to be covered with probability at most
1/(2k), while the union's expected cost stays at T · log(n) · OPT.
Three milestones, in attack order, each stated exactly as the book states it (p. 230-231), with
the book's own caveat "we state the main lemmas and omit the proofs" preserved — no in-source
proof exists for any of the three beyond the algorithm's own description, so each is left sorry
with no invented proof strategy:
ℙ[e ∈ C] = w'ₑ for every edge, and ℙ[e ∈ C] = 1
whenever wₑ > 1 already.C is at most ∑_{e∈T} cₑ w'ₑ (linearity of expectation
applied to Lemma 11.1).g of size at most N with total routable flow wg ≥ 1, the
probability some vertex of g is covered is Ω(1/log N).This is the survey's most involved application of the primal-dual framework: unlike Chapters 5, 9, 10 and 13, which round a single scalar decision per online step, the group Steiner algorithm must couple an entire iteration's worth of edge decisions so that the resulting random set stays a connected subtree — the coin-flip probabilities in the Algorithm box are exactly the minimal adjustment needed to keep marginal probabilities matching the fractional solution while preserving this connectivity invariant online. No formal development of the group Steiner problem (online or offline) was found on the platform as of 2026-09-20; this mission is the first.
Two distinct obstacles. First, faithfully representing "the probability that e ∈ C" for an
online, coupled random process without assuming its proof: the mission represents the
algorithm's random cover as an abstract finite probability distribution RandomCover E and
states each lemma as an implication from the Algorithm box's three coupling rules (transcribed as
hypotheses on marginal and conditional probabilities) to the claimed marginal or expected-value
conclusion — capturing exactly what the book asserts without proof, rather than either assuming
the conclusion trivially or constructing a full multi-iteration coupled process (which the
source's own "we omit the proofs" indicates is genuinely nontrivial, citing [56]). Second,
Theorem 11.4's own competitive ratio is stated in the book only asymptotically, with a purely
narrative derivation ("we run O(log k log N) independent trials... we get a competitive ratio
of O(log n log k log N)... probability at least 1 − 1/k") and no displayed formula anywhere
in the chapter. Per this series' explicit-constants rule, this mission supplies its own explicit
closed form for the number of trials T and the resulting bounds via a standard
Chernoff/union-bound argument applied to Lemma 11.3's constant α; this derivation is the
mission's own (documented below), not a transcription, since none exists in the source to
transcribe.
RandomCover E is a finite pmf p : Finset E → ℝ (Finset E itself finite since E is
Fintype), with marg, condProb and expectedCost/probHits derived from it by ordinary
Finset sums — no measure theory, since the sample space is always finite. RoundedTree E bundles
parent : E → Option E (e(p)) and a non-negative cost. Lemma 11.3's wg (the flow routable to
a group's vertices simultaneously) is left as hypothesis-supplied data rather than defined via an
explicit max-flow formalization, which this mission's scope does not require (welcome
contribution). Theorem 11.4's number of trials is the explicit closed form
T = ⌈(log N · log(2k)) / α⌉, α the (existentially quantified, uniform) constant from Lemma
11.3; its coverage guarantee is 1 − 1/(2k) per group (this mission's own union-bound
derivation), not the book's stated 1 − 1/k — the book reaches the stronger bound via an
additional shortest-path fallback mechanism for any group the trials miss, which is out of scope
here (welcome contribution, along with completing any of the four sorrys and formalizing
Theorem 11.5's extension to general graphs via HST embedding, out of scope since it depends on an
external embedding result not proved in this book).
Search-engine ad-auctions sell items (ad slots) to buyers who arrive with per-item bids and a fixed daily budget, online: each item must be allocated the moment it appears, with no ability to revisit past allocations, and no buyer may ever be charged more than its budget. Buchbinder and Naor's survey [1] models this as a generalization of online bipartite matching and derives an allocation algorithm through the same online primal-dual recipe formalized elsewhere in this series (Chapter 4's framework), applied to a genuinely different LP shape — a maximization (revenue) problem whose "packing" role and "covering" role are the reverse of Chapters 4, 5 and 7 — and to a different constraint structure (budget caps on a per-buyer accumulated sum, not a per-constraint 0/1 covering requirement). This mission covers Section 10.1, "The Basic Algorithm": the single-slot allocation algorithm and its -competitive analysis (Theorem 10.1). Sections 10.2-10.3 (multiple ad-slots via strong duality; stochastic per-buyer spending guarantees) are out of scope — see Formalization scope.
Fix a finite set of buyers, each with budget , and a finite set of items; buyer bids for item , revealed one item at a time in the order enumerated by . Let , carried as an explicit positive parameter. The Allocation algorithm (p. 212), upon each item 's arrival, allocates it to the buyer maximizing (where is buyer 's current primal value); if already, nothing happens (the buyer is "full"). Otherwise it charges buyer the minimum of and its remaining budget, sets the dual allocation variable , sets , and updates for a constant fixed by the analysis. The revenue actually collected from buyer is — the buyer is never charged more than its budget. Unlike Chapters 4/7, this LP's dual (the ad-auctions revenue objective, Fig. 10.1) is the maximization problem being solved online; the "primal" covering LP (, variables) exists only as a duality certificate.
Theorem 10.1 (the goal, p. 212), given the milestone's dual near-feasibility bound and the fact that each buyer's total accrued bids exceed its budget by at most a factor of (Claim (3)'s consequence):
with taken verbatim from the theorem's own statement — the exact formula, not an instantiation. Inequality (10.1) (p. 213), the milestone, is the book's own induction-proved lower bound on a buyer's primal value in terms of its accrued bids: .
Theorem 10.1 is the entry point to a short but influential sub-line of the online primal-dual method — Section 10.2 extends it to multiple ad-slots via strong duality for maximum-weight matching (rather than the weak duality this framework otherwise relies on throughout), and Section 10.3 incorporates stochastic per-buyer spending guarantees, both reusing this section's constant and its limit as (recovering the classic -competitive ratio for the unweighted, unbudgeted case). It is also the first mission in this series to apply the online primal-dual method to a genuine revenue-maximization problem rather than a covering/packing pair with matching roles. No formal development of ad-auctions, budgeted online matching, or this constant was found on the platform as of 2026-09-20 (searches below); this mission is the first.
As with 04-framework's Algorithm 3 and 07-generalized-caching's Fractional Caching algorithm,
the central obstacle is characterizing an online process by its own final output. Unlike those
two chapters, however, step (3)'s update increment varies per allocation (bd, the specific bid
of the item just won), so no closed-form solution of the recurrence exists in general; buyerX is
instead defined as an explicit List.foldl realizing the exact per-step update, over the
(temporally ordered) list of bids a buyer actually won — a faithful, if less immediately readable,
transcription of "the algorithm's output as a function of its own trajectory," in the same spirit
as this series' other closed-form definitions. A second difficulty specific to this chapter: the
book's derivation of inequality (10.1) is itself an induction on iterations (not a single algebraic
step, unlike Eq. (7.2) in 07-generalized-caching), and the theorem's final bound further combines
it with a separate "at most one undercharged iteration" argument (Claim (3)'s conclusion,
p. 214-215) turning the raw accrued-bid bound into one about the actually collected (budget-capped)
revenue — both are stated here as explicit hypotheses (the milestone, and
h_at_most_one_undercharge) rather than derived, since the goal is a faithful statement, not a
proof; both sorrys are documented, not silently discharged.
AdAuctionsInstance I M bundles b : I → M → ℝ, B : I → ℝ (hB_pos), and Rmax : ℝ with
hRmax_pos : 0 < Rmax and hRmax_bound : ∀ i j, b i j ≤ Rmax * B i — the last two as explicit
hypotheses, never derived via Finset.sup, matching 04-framework's d and
07-generalized-caching's k. cParam inst := (1+Rmax)^(1/Rmax) uses Real.rpow (ℝ^ℝ).
buyerX inst i bids folds step (3)'s update over a list of won bids; revenue/actualCharge
realize and its budget-capped charge. Reals throughout. Explicitly out of
scope: Section 10.2's multiple-slot generalization (Theorem 10.2), which requires strong duality
for maximum-weight bipartite matching as an explicit premise (the book: "our analysis... crucially
relies on strong duality") — a substantially different LP structure (an integral matching LP, not
this section's per-buyer budget LP) that this mission's AdAuctionsInstance does not model, and
whose applicability of PrimalDualOnline.LP.strong_duality_adapter (this book's own Theorem 2.2)
was not verified in the time available. Section 10.3's stochastic guarantee (Theorem 10.3) is
likewise out of scope, and its own BRIEF.md-flagged ambiguity (whether its scalar g is
or another aggregate of the per-buyer vector ) was not resolved. Both are natural
follow-on missions, not attempted here. Welcome contributions: completing the two sorrys, and the
Section 10.2-10.3 follow-on mission(s).