Probability

Motivation

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 $m$ of $n$ 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 $W$ paid whenever a bandit is passive, solve the resulting single-bandit average-reward problem, and read off, for each state, the least subsidy $W(x)$ at which the passive action becomes optimal. When the set of states where passivity is optimal grows monotonically with $W$, the bandit is indexable and $W(x)$ is its Whittle index; the Whittle index policy activates the $m$ bandits of largest index. It reduces to the Gittins index policy when the passive action freezes, it is asymptotically optimal as $n$ 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.

Setting

A restless bandit is a Markov decision process with two actions, active ($u = 1$) and passive ($u = 0$), each with its own transition kernel and reward. Under a deterministic stationary Markov policy $g$ with passive subsidy $W$ the reward in state $x$ is $r(x, g(x)) + W(1 - g(x))$, and the average reward from $x$ is the Cesàro limit of the expected rewards. The optimal average reward $g(W)$ is the supremum over such policies and initial states; a policy is optimal if it attains $g(W)$ from every initial state; $E_0(W)$ is the set of states in which some optimal policy is passive; the bandit is indexable if $E_0(W)$ is nondecreasing in $W$; and $W(x) = \inf\{W : x \in E_0(W)\}$.

The spinning plates asset lives on $\{1, \dots, k\}$: active moves $x \to x + 1$ at rate $\lambda(x)$, passive moves $x \to x - 1$ at rate $\mu(x)$, $\lambda(k) = \mu(1) = 0$, and $r(x)$ is earned under both actions, $r$ 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 $(y)$ is passive exactly on $\{x \ge y\}$; under it the asset alternates between $y - 1$ and $y$, spending the fraction $\phi(y) = \lambda(y-1)/(\lambda(y-1) + \mu(y))$ of its time at $y$, so its average reward is $W\phi(y) + R(y)$ with $R(y) = r(y)\phi(y) + r(y-1)(1 - \phi(y))$, and $W^*(x) = (R(x+1) - R(x))/(\phi(x) - \phi(x+1))$. The vigour bandit is the mirror image: active moves down at rate $\nu(x)$ and earns $r(x)$, passive moves up at rate $\rho(x)$ and earns nothing, $\psi(y) = \nu(y)/(\nu(y) + \rho(y-1))$, and $W^{**}(x) = (r(x)(1 - \psi(x)) - r(x+1)(1 - \psi(x+1)))/(\psi(x+1) - \psi(x))$.

Formalization targets

Goal: Theorem 6.4

For the spinning plates asset: (i) if $\phi$ is strictly decreasing over the thresholds $1 \le y \le k + 1$, the asset is indexable; (ii) if additionally $W^*$ is strictly decreasing over the states, the Whittle index is

$$W(x) = W^*(x) = \frac{R(x+1) - R(x)}{\phi(x) - \phi(x+1)}, \qquad 1 \le x \le k.$$

Milestones

Eqs. (6.9)–(6.10): the monotone policy $(y)$ earns $W\phi(y) + R(y)$ from every initial state and $g(W) = \max_y [W\phi(y) + R(y)]$, because a monotone policy always achieves $g(W)$; Theorem 6.5, the same two statements for the vigour bandit with $\psi$ increasing and $W^{**}$ increasing.

Significance

Theorem 6.4 is the chapter's template for proving indexability: the single-bandit value $g(W)$ is the upper envelope of finitely many lines $W\phi(y) + R(y)$ 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.

Difficulty

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 $\{z - 1, z\}$ whose average reward is that of the monotone policy $(z)$, so no policy beats the best monotone one and the passive set under an optimal-from-everywhere policy is exactly $\{x \ge x(W)\}$ 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 $\{0,1\}$-strings. The envelope argument then needs that the smallest maximizer of $\max_y [W\phi(y) + R(y)]$ is nonincreasing in $W$ when $\phi$ is strictly decreasing, and that with $W^*$ strictly decreasing the maximizer is $\le x$ exactly when $W \ge W^*(x)$. 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.

Formalization scope

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 $\phi$ and $\psi$ (the book's "convenient positive values") replaced by their values $1, 0$ and $0, 1$ at the two extreme thresholds; the model assumptions $\lambda(k) = \mu(1) = 0$, $\nu(1) = \rho(k) = 0$, rates in $[0, 1]$, and $r$ increasing and nonnegative are hypotheses. Theorem 6.5's "increasing" is read as strictly increasing, as in Theorem 6.4, since a nonstrict $\psi$ admits zero interior rates for which the monotone reduction fails. The milestone (6.9) requires $k \ge 1$ 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 $\{0,1\}$-policy to a monotone one, and the envelope lemma for lines with decreasing slopes.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 6. doi:10.1002/9780470980033
• P. Whittle, Restless bandits: activity allocation in a changing world, Journal of Applied Probability 25(A), 1988. doi:10.2307/3214163
• R. R. Weber, G. Weiss, On an index policy for restless bandits, Journal of Applied Probability 27(3), 1990. doi:10.2307/3214547
• K. D. Glazebrook, C. Kirkbride, D. Ruiz-Hernandez, Spinning plates and squad systems: policies for bi-directional restless bandits, Advances in Applied Probability 38(1), 2006. doi:10.1239/aap/1143936141
• J. Niño-Mora, Restless bandits, partial conservation laws and indexability, Advances in Applied Probability 33(1), 2001. doi:10.1017/S0001867800010661
• C. H. Papadimitriou, J. N. Tsitsiklis, The complexity of optimal queueing network control, Mathematics of Operations Research 24(2), 1999. doi:10.1287/moor.24.2.293

Motivation

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.

Setting

There are $N$ job types $E = \{1, \dots, N\}$. A policy $\pi$ has a performance $x^\pi \in \mathbb{R}^N_+$, a vector of expectations; a permutation $\sigma$ of $E$ defines the permutation policy giving $\sigma_N$ highest and $\sigma_1$ lowest priority, and $S_k = \{\sigma_1, \dots, \sigma_k\}$ is the set of the $k$ lowest-priority types. The system satisfies GCL(1) if there are a base function $b : 2^E \to \mathbb{R}_+$ and a matrix $A = (A_i^S)$, positive on $S$ and zero off it, such that for every policy

$$\sum_{i \in S} A_i^S x_i^\pi \ge b(S) \quad (S \subseteq E), \qquad \sum_{i \in E} A_i^E x_i^\pi = b(E),$$

with equality in the first for every permutation policy whose $|S|$ lowest-priority types are $S$. GCL(2) reverses the inequality. The adaptive greedy algorithm $AG(A, r)$ picks $i_N$ maximizing $r_i/A_i^E$, sets $\bar y_E$ to the maximum, removes $i_N$, and repeats with the adjusted rewards $r_i - \sum_{j \ge k} A_i^{S_j}\bar y_{S_j}$ divided by $A_i^{S_{k-1}}$; its outputs are the order $i_1, \dots, i_N$, the dual variables $\bar y_{S_k}$ and the indices $\nu_{i_k} = \sum_{j \ge k} \bar y_{S_j}$.

For the SFABP of Section 5.3, $n$ identical bandit processes on $E$ with kernel $P$ and discount factor $a$ in the model of the Bandit Algorithms series, $x_i^\pi = \mathbb{E}^\pi \sum_t a^t I_i(t)$ is the discounted number of continuations of a bandit in state $i$, $A_i^S = \mathbb{E}[1 + a + \cdots + a^{T_i^S - 1}]$ is the discounted return time to $S$ from $i \in S$, and $b(S)$ is the minimal cost $\sum_{i \in S} A_i^S x_i^\pi$, namely $(1-a)^{-1}\mathbb{E}[a^\tau]$ with $\tau$ the number of continuations needed to bring every bandit into $S$.

Formalization targets

Goal: Theorem 5.5

For a GCL(1) system whose achievable region is convex, and any reward vector $r$: the achievable region is the polytope

$$P(A, b) = \Big\{x \in \mathbb{R}_+^N : \sum_{i \in S} A_i^S x_i \ge b(S),\ S \subset E,\ \sum_{i \in E} A_i^E x_i = b(E)\Big\};$$

its extreme points are performances of permutation policies; $AG(A, r)$ has an output; and for every output the permutation policy in the order it finds, the Gittins index policy, maximizes $\sum_i r_i x_i^\pi$ over all policies.

Milestones

Lemma 5.1 (the SFABP satisfies the conservation laws, with equality for policies giving priority to states outside $S$); 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.

Significance

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.

Difficulty

The goal's optimality clause is weak LP duality once one shows that the greedy dual variables are nonpositive except $\bar y_E$ 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 $S$, and the observation that at most $\tau$ slots can be spent on bandits that have never been in $S$; 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 $b(S)$ 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 $\{i_1, \dots, i_{k-2}\}$, which lie between $\{\nu < \nu(i_{k-1})\}$ and $\{\nu \le \nu(i_{k-1})\}$; ties make the induction delicate, and the statement is claimed for every tie-breaking.

Formalization scope

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 $n$ identical bandits on Fin N in the Bandit Algorithms model, the coefficients $A_i^S$ through Mission I's stoppedTime at the return time, and $b(S)$ in the product form $(1-a)^{-1}\prod_{j : k_j \notin S}\mathbb{E}[a^{T^S_{k_j}}]$, which is the minimal cost the argument on p. 120 establishes; the book prints a sum, which is $0$ when all bandits start in $S$ where the minimal cost is $1/(1-a)$. Discount factors are in $(0, 1)$ throughout.

Trivializing readings are excluded: $A_i^S > 0$ for $i \in S$ 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.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 5. doi:10.1002/9780470980033
• D. Bertsimas, J. Niño-Mora, Conservation laws, extended polymatroids and multiarmed bandit problems; a polyhedral approach to indexable systems, Mathematics of Operations Research 21(2), 1996. doi:10.1287/moor.21.2.257
• P. Tsoucas, The region of achievable performance in a model of Klimov, IBM Research Report RC16543, 1991.
• E. G. Coffman, I. Mitrani, A characterization of waiting time performance realizable by single-server queues, Operations Research 28(3), 1980. doi:10.1287/opre.28.3.810
• K. D. Glazebrook, R. Garbe, Almost optimal policies for stochastic systems which almost satisfy conservation laws, Annals of Operations Research 92, 1999. doi:10.1023/A:1018992306696
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401

Motivation

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).

Setting

There are $K$ arms and $T$ rounds. A mean reward vector $\mu \in [0,1]^K$ is drawn from a known prior $P$, and each pull of arm $a$ yields a reward drawn from a known family $D_{\mu_a}$ with mean $\mu_a$. In round $t$ the principal recommends an arm $\mathrm{rec}_t$; agent $t$, who knows the prior, the family, the algorithm and the round but not the past, sees only $\mathrm{rec}_t$, chooses $a_t$, collects $r_t \sim D_{\mu_{a_t}}$ and leaves; the principal observes $(a_t, r_t)$. The chapter works with two arms, ordered so that the prior means satisfy $\mu^0_1 \ge \mu^0_2$, 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 $t$ and arms $a \ne a'$ with $\Pr[\mathrm{rec}_t = a, E_{t-1}] > 0$,

$$\mathbb{E}[\mu_a - \mu_{a'} \mid \mathrm{rec}_t = a,\ E_{t-1}] \ge 0, \tag{11.1}$$

where $E_{t-1}$ 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, $a_t \in \arg\max_a \mathbb{E}[\mu_a \mid H_t]$ (11.2); it is BIC and it fails. HiddenExploration (Algorithm 11.1) hides a little exploration in a lot of exploitation: on a signal $\mathrm{sig}$, with probability $\varepsilon$ it recommends a target arm $a_{\mathrm{trg}}(\mathrm{sig})$, otherwise the arm maximizing $\mathbb{E}[\mu_a \mid \mathrm{sig}]$, ties to arm 1. Its posterior gap is $G = \mathbb{E}[\mu_2 - \mu_1 \mid \mathrm{sig}]$. RepeatedHE (Algorithm 11.2) runs it round after round with an arbitrary bandit algorithm $\mathrm{ALG}$ as the target: $N_0$ initial rounds recommend arm 1; afterwards, with probability $\varepsilon$ the round is an exploration round in which $\mathrm{ALG}$ chooses (and is fed the reward), and otherwise the exploitation branch recommends $\min\arg\max_a \mathbb{E}[\mu_a \mid S_t]$, where $S_t$ is the data of all exploration rounds so far (11.10). The quantity that governs everything is $G_{1,n} = \mathbb{E}[\mu_2 - \mu_1 \mid S_{1,n}]$ (11.11), the posterior gap after $n$ samples of arm 1, and Property (11.12), that $\Pr[G_{1,n} > 0] > 0$ for some $n$: arm 2 can appear better after enough samples of arm 1.

Formalization targets

Goal: Theorem 11.15

RepeatedHE with exploration probability $\varepsilon > 0$ and $N_0$ initial samples of arm 1 is BIC as long as

$$\varepsilon < \tfrac13\,\mathbb{E}\big[G \cdot \mathbf 1\{G > 0\}\big], \qquad G = G_{N_0+1} = \mathbb{E}[\mu_2 - \mu_1 \mid S_{1,N_0}],$$

for any bandit algorithm $\mathrm{ALG}$ and any horizon. The threshold depends on the prior alone.

Milestones

Theorem 11.7 (GREEDY never chooses arm 2 with probability at least $\mu^0_1 - \mu^0_2$) and Corollary 11.8 (linear Bayesian regret of GREEDY under independent priors); Lemma 11.10 (HiddenExploration is BIC when $\varepsilon \le \frac13\mathbb{E}[G\mathbf 1\{G > 0\}]$) 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).

Significance

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 $T$, and Corollary 11.8 turns that into $\Omega(T)$ Bayesian regret. Theorem 11.15 shows that a recommendation-only principal can induce any amount of exploration it wants, with $\mathrm{ALG}$ arbitrary, at a per-round rate $\varepsilon$ fixed by the prior; Theorem 11.17 (stated with a proof sketch, and omitted here) then transfers $\mathrm{ALG}$'s regret to RepeatedHE up to the prior-dependent factors $N_0$ and $1/\varepsilon$, so $\tilde O(\sqrt T)$ 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 $K$-arm and the "explore all explorable arms" extensions of the literature review.

Difficulty

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 $\mathbb{E}[Z_\tau] = \mu^0_1 - \mu^0_2$; all of this has to be set up on the joint law of $(\mu, H_T)$ 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 $\mathrm{rec}$: it works with $F(E) = \mathbb{E}[G\mathbf 1_E]$, splits along the two branches, uses that the exploitation branch recommends arm 2 exactly when $G > 0$, and closes with $F(G > 0) + F(G < 0) = \mathbb{E}[\mu_2 - \mu_1] \le 0$; the only place where the analysis uses that both branches are functions of the signal is the step $\mathbb{E}[\mu_2 - \mu_1 \mid \mathrm{rec} = 2] = \mathbb{E}[G \mid \mathrm{rec} = 2]$, and a formalization has to make that step explicit. Theorem 11.15 requires seeing each later round of RepeatedHE as a HiddenExploration with signal $S_t$, where $\mathrm{ALG}$'s choice is a randomized function of $S_t$, and then the monotonicity of $\mathbb{E}[G_t\mathbf 1\{G_t > 0\}]$ in $t$, a two-line consequence of $S_{t+1}$ determining $S_t$ that presupposes the posterior given $S_t$ is the Bayes posterior of the exploration data alone, which is true because the exploration decisions do not depend on $\mu$ given that data. Corollary 11.8 needs the independence of the event "$\mu_1 < 1 - 2\alpha$ and arm 2 is never chosen" from $\mu_2$. Theorem 11.19 is an induction in which the inductive hypothesis is a probability-zero statement about all earlier rounds.

Formalization scope

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 $F \subseteq [0,1]^2$, with $\mu^0_1 \ge \mu^0_2$ as a hypothesis; the reward family is mission III's RewardFamily (finitely many values, mean $\nu$ for $\nu \in [0,1]$). BIC is defined on a joint law of $(\mu, \text{record})$ of the run in which every agent complies, with the recommendation of each round read off the record; the compliance event $E_{t-1}$ 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 $F$, so there are no integrals and no integrability side conditions; a posterior mean off the support is a junk $0$ 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, $\mu$ and record weighted by the prior times the product of the round probabilities (initial rounds forced to arm 1, then the $\varepsilon$-coin, $\mathrm{ALG}$'s kernel on its own history, or the exploitation arm, then $D_{\mu_{a_t}}$); it is written this way because $\mathrm{ALG}$ is fed a history of variable length. Two conditions are stated exactly as printed: Lemma 11.10 with $\varepsilon \le \frac13\mathbb{E}[G\mathbf 1\{G > 0\}]$ (non-strict, checked at equality) and Theorem 11.15 with the strict inequality.

Trivializations are excluded: $\varepsilon > 0$ 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.

Selected references

• A. Slivkins, Introduction to Multi-Armed Bandits, Foundations and Trends in Machine Learning 12(1-2), 2019, Chapter 11. arXiv:1904.07272, doi:10.1561/2200000068
• I. Kremer, Y. Mansour, M. Perry, Implementing the "Wisdom of the Crowd", Journal of Political Economy 122(5), 2014. doi:10.1086/676597
• Y. Mansour, A. Slivkins, V. Syrgkanis, Bayesian Incentive-Compatible Bandit Exploration, Operations Research 68(4), 2020 (EC 2015). doi:10.1287/opre.2019.1919
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. doi:10.1257/aer.101.6.2590
• M. Sellke, A. Slivkins, The Price of Incentivizing Exploration: A Characterization via Thompson Sampling and Sample Complexity, Operations Research 71(5), 2023. doi:10.1287/opre.2022.2401

Safety stock in a chain

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.

Setting

Installation 1 faces normally distributed period demand with mean $\mu$ and standard deviation $\sigma$, independent across periods, so the demand over $n$ periods, $D(n)$, is normal with mean $n\mu$ and standard deviation $\sqrt n\,\sigma$. Installation 1 replenishes from installation 2 with lead-time $L_1$ periods; installation 2 replenishes from an outside supplier with infinite supply and lead-time $L_2$. Demand that cannot be met is backordered. Costs per unit and period are echelon holding costs $e_1, e_2 \ge 0$, so the installation holding costs are $h_1 = e_1 + e_2$ and $h_2 = e_2$, and a shortage cost $b_1$ 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 $t$. After ordering, installation 2 has an echelon inventory position $y_2$, and by the standard argument its echelon stock in period $t + L_2$ is $y_2 - D(L_2)$. Installation 1 then orders, realizing an echelon position $y_1$ that cannot exceed what is available: $y_1 \le y_2 - D(L_2)$ (Eq. 10.1). Its inventory level after the demand in period $t + L_2 + L_1$ is $y_1 - D(L_1+1)$. The expected period costs are $C_2 = h_2\,\mathbb{E}(y_2 - D(L_2) - y_1)$ at installation 2 and $C_1 = h_1\,\mathbb{E}(y_1 - D(L_1+1))^{+} + b_1\,\mathbb{E}(y_1 - D(L_1+1))^{-}$ at installation 1, and the book reallocates the term $-h_2y_1$ to obtain

$$\tilde C_2(y_2) = h_2(y_2 - \mu_2'), \qquad \tilde C_1(y_1) = e_1y_1 - h_1\mu_1'' + (h_1 + b_1)\,\mathbb{E}\big(y_1 - D(L_1+1)\big)^{-},$$

with $\mu_2' = L_2\mu$ and $\mu_1'' = (L_1+1)\mu$. As a function of a free $\hat y_1$, $\tilde C_1$ is the newsboy-type function $\hat C_1$ of Eq. (10.6), minimized at the level $S_1 = \hat y_1^{*}$ given by the fractile equation (10.8). Passing everything available up to $S_1$ to installation 1, $y_1 = \min\{S_1, y_2 - D(L_2)\}$, gives the total cost $\hat C_2(y_2)$ of Eq. (10.9), whose minimizer $S_2 = y_2^{*}$ is the order-up-to level of installation 2.

Formalization targets

Goal — the decomposition

With $S_1$ from (10.8) and $S_2$ a minimizer of $\hat C_2$: for every $y_2$ and every allocation rule $a$ with $a(u) \le y_2 - u$ and finite expected cost,

$$\hat C_2(S_2) \;\le\; \mathbb{E}\big[\tilde C_2(y_2) + \tilde C_1(a(D(L_2)))\big],$$

and the order-up-to policy $(S_1, S_2)$ attains $\hat C_2(S_2)$.

Supporting targets

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 $\hat C_1$ through the loss function $G$; the convexity of $\hat C_1$, its derivative (10.7), and the fractile characterization (10.8) of its minimizers; the pointwise rule that $\min\{S_1, y_2 - u\}$ is the cheapest feasible $y_1$; the identity (10.9); and the convexity of $\hat C_2$ (Problem 10.1) with the existence of its minimizer when $e_2 > 0$.

Significance

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 $S_1$ is a newsboy solution with overage cost $e_1$, the value added, and underage cost $e_2 + b_1$, and it is independent of the upstream installation altogether; the upstream level $S_2$ 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.

Difficulty

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 $u = y_2 - S_1$, and the convexity of $\hat C_2$, which requires seeing that $x \mapsto \hat C_1(\min\{S_1, x\})$ is convex precisely because $S_1$ is a minimizer of the convex $\hat C_1$ (for any other cut-off the function is not convex), and that convexity is preserved by integrating against the law of $D(L_2)$, which needs the integrability of the linearly growing $\hat C_1$. Existence of $S_2$ then follows from the growth of $\hat C_2$ at both ends, which comes from the asymptotics of the loss function: $G(z) \to 0$ as $z \to \infty$ and $G(z) + z \to 0$ as $z \to -\infty$.

Formalization scope

$D(n)$ is csDemand mu sigma n, the Gaussian law newsboyDemand (n μ) (√n σ) from the newsboy mission, so the loss function $G$ and its closed form are reused as references. The costs are parametrized by $e_1, e_2, b_1$ with $h_1 = e_1 + e_2$ and $h_2 = e_2$ written out; $\tilde C_1$, $\tilde C_2$, the pre-reallocation period cost and $\hat C_2$ are Bochner integrals against these laws. Every statement assumes $\sigma > 0$; the goal and the convexity statements assume $e_1, e_2 \ge 0$ and $b_1 > 0$, the book's cost signs. $L_2 = 0$ is allowed and makes $D(L_2)$ a point mass, which is the setting of the book's Problem 10.2.

$S_1$ enters as any solution of the fractile equation (10.8) and $S_2$ as any minimizer of $\hat C_2$; the other items show that both exist when $e_1, e_2 > 0$. When $e_1 = 0$ the fractile is $1$, no $S_1$ exists, and the goal is vacuous, which is faithful: the book observes that then $S_1 \to \infty$ and installation 2 never carries stock. Symmetrically, when $e_2 = 0$ and $L_2 \ge 1$, $\hat C_2$ decreases towards its infimum without attaining it, so no $S_2$ exists and the goal is again vacuous: with free upstream holding the optimal $y_2$ is unbounded. Allocation rules are arbitrary functions of the realized $D(L_2)$ with an integrability hypothesis; without it Lean's integral of a non-integrable cost would be $0$ and could undercut $\hat C_2(S_2)$, 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 $y_2$ 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 ($L_2 = 0$) as a first step are welcome.

Selected references

• Sven Axsäter, Inventory Control, 3rd edition, International Series in Operations Research & Management Science 225, Springer, 2015, Sect. 10.1.1. DOI 10.1007/978-3-319-15729-0
• Andrew J. Clark and Herbert Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4), 1960, pp. 475-490. DOI 10.1287/mnsc.6.4.475
• Awi Federgruen and Paul Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4), 1984, pp. 818-836. DOI 10.1287/opre.32.4.818
• Kaj Rosling, Optimal Inventory Policies for Assembly Systems under Random Demands, Operations Research 37(4), 1989, pp. 565-579. DOI 10.1287/opre.37.4.565
• Geert-Jan van Houtum, Karl Inderfurth and Willem H. M. Zijm, Materials Coordination in Stochastic Multi-Echelon Systems, European Journal of Operational Research 95(1), 1996, pp. 1-23. DOI 10.1016/0377-2217(96)00080-8

One stage at a time

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.

Setting

Stages are numbered $1, \dots, N$ from the customer upward. Stage $j$ has a local holding cost $h'_j$ per unit per period; its echelon holding cost is $h_j = h'_j - h'_{j+1}$ with $h'_{N+1} = 0$, so that $h'_j = \sum_{i \ge j} h_i$ (localHolding, echelonHolding). Stage $j$'s echelon consists of stages $j, j-1, \dots, 1$, and its echelon on-hand inventory $I_j$ (echelonOnHand) is all on-hand and in-transit stock in that echelon. Stage 1 pays a stockout cost $p$ per unit per period. Orders placed by stage $j$ arrive after a lead time $L_j$ if stage $j+1$ can ship them; $D_j$ denotes the lead-time demand at stage $j$.

An echelon base-stock policy gives each stage a level $S_j$ and orders to keep its echelon inventory position at $S_j$. The chapter derives, from conservation of flow, a recursion that evaluates the expected cost of any echelon base-stock vector $S$ (csBar, csHat, csG):

$$\bar g_0(x) = (p + h'_1)x^-, \qquad \hat g_j(x) = h_j x + \bar g_{j-1}(x), \qquad g_j(y) = \mathbb{E}[\hat g_j(y - D_j)], \qquad \bar g_j(x) = g_j(\min\{S_j, x\}),$$

and the expected cost of the system under $S$ is $g_N(S_N)$. The term $\bar g_j$ is the implicit penalty function: it charges stage $j+1$ for the downstream consequences of running short. A vector is sequentially optimal (CSSequential) when each $S_j$ minimizes $g_j$, which depends only on $S_1, \dots, S_{j-1}$.

The Shang-Song bounds compare $g_j$ with the cost of the $j$-stage truncated system when all its local holding costs are set to one value, $h_j$ for the lower bound and $\sum_{k \le j} h_k$ 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 $\tilde D_j = D_1 + \dots + D_j$ over the cumulative lead time (tildeLaw) with stockout cost $p + h'_{j+1}$, plus the holding cost of the stock in transit to stages $1, \dots, j-1$, whose mean is $\mathbb{E}[D_1] + \dots + \mathbb{E}[D_{j-1}]$ (pipelineMean).

In the guaranteed-service model each stage $i$ has a processing time $T_i$, quotes a committed service time $S_i$ to its customer, and receives an inbound time $SI_i = S_{i+1}$ from its supplier (gsInbound), $SI_N$ being external. Demand is bounded, so the stage can meet every order within $S_i$ by holding safety stock $k\sqrt{SI_i + T_i - S_i}$ with $k = z_\alpha\sigma$, and the holding cost is $g(S) = \sum_i h_i k \sqrt{SI_i + T_i - S_i}$ (gsCost) over the feasible times $0 \le S_i \le SI_i + T_i$ (GSFeasible).

Formalization targets

Goal: Theorem 6.3

For echelon holding costs $h_j \ge 0$, stockout cost $p \ge 0$ and lead-time demands of finite mean, if $S^*$ is sequentially optimal then for every echelon base-stock vector $S$,

$$g_N(S^*_N \mid S^*) \;\le\; g_N(S_N \mid S),$$

and $g_N(S^*_N \mid S^*)$ is the optimal cost. This is clark_scarf_sequential.

Supporting targets

Proposition 6.1, $\sum_j h_j I_j = \sum_j h'_j (I'_j + IT_{j-1})$; the stage-1 identities (6.29) and (6.30), that $g_1$ is a newsvendor cost with penalty $p + h'_2$ and its minimizer solves $F_1(S^*_1) = (p + h'_2)/(h_1 + p + h'_2)$; convexity of every $g_j$ under sequential optimality; existence of a sequentially optimal vector when $h_j > 0$ and $p > 0$; Theorem 6.4, $g^l_j \le g_j \le g^u_j$, and $S^l_j \le S^*_j \le S^u_j$ where $S^u_j$ minimizes $g^l_j$ and $S^l_j$ minimizes $g^u_j$ (the book's pairing, p. 200); and Theorem 6.5, that in the guaranteed-service serial system with $s_1 = 0$ every optimal $S^*_i$ is $0$ or $S^*_{i+1} + T_i$.

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.

Significance

Theorem 6.3 is what Zipkin calls the fundamental equations of supply chain theory. It reduces a joint optimization over $N$ coupled levels to $N$ 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.

Difficulty

The obvious attack on Theorem 6.3, differentiating the system cost in each $S_j$, fails immediately: the cost depends on $S_j$ through $\min\{S_j, x\}$ inside nested expectations and is not convex in $S$ jointly. The argument that works is an induction along the recursion, comparing $g_j(\cdot \mid S)$ with $g_j(\cdot \mid S^*)$ pointwise. Its key step is that, for the convex $g_j(\cdot \mid S^*)$ minimized at $S^*_j$, the value $g_j(\min\{S^*_j, x\})$ is the least value of $g_j$ on $(-\infty, x]$, so that any other truncation point can only cost more. That step needs convexity of $g_j(\cdot \mid S^*)$, which needs $\bar g_{j-1}(\cdot \mid S^*)$ convex, which needs $S^*_{j-1}$ to be a minimizer; for an arbitrary $S$ the functions $\bar g_j(\cdot \mid S)$ are not convex, and the induction must carry both vectors at once.

Integrability is a second, silent obstacle. Each $g_j$ is an expectation of translates of $\hat g_j$; 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 $\tilde D_j$, 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.

Formalization scope

Stages are indexed by natural numbers $1, \dots, N$; the cost functions take total functions on $\mathbb{N}$ and never read values outside that range. The recursion is defined for every vector $S$, so the theorem compares values of one family of functions rather than a separately defined system cost; the identification of $g_N(S_N \mid S)$ 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 $\mathbb{R}$ with finite means. Sequential optimality is a hypothesis of the goal; a separate target shows it is satisfiable when $h_j > 0$ and $p > 0$, 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 $S^*_j$; when the fractiles of $\tilde D_j$ 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 $IT_0 = 0$ 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.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 6. https://doi.org/10.1002/9781119584445
• A. J. Clark and H. Scarf, Optimal policies for a multi-echelon inventory problem, Management Science 6(4), 1960. https://doi.org/10.1287/mnsc.6.4.475
• F. Chen and Y.-S. Zheng, Lower bounds for multi-echelon stochastic inventory systems, Management Science 40(11), 1994. https://doi.org/10.1287/mnsc.40.11.1426
• K. H. Shang and J.-S. Song, Newsvendor bounds and heuristic for optimal policies in serial supply chains, Management Science 49(5), 2003. https://doi.org/10.1287/mnsc.49.5.618.15147
• S. C. Graves and S. P. Willems, Optimizing strategic safety stock placement in supply chains, Manufacturing & Service Operations Management 2(1), 2000. https://doi.org/10.1287/msom.2.1.68.23267

Why orders swing more than sales

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.

Setting

Demand signal processing. A retailer faces a demand process $D_t$, $t \in \mathbb{Z}$, that follows the stationary first-order autoregressive model

$$D_t = d + \rho D_{t-1} + \epsilon_t,$$

with a constant $d \ge 0$, a correlation constant $-1 < \rho < 1$, and errors $\epsilon_t$ that are independent $N(0, \sigma^2)$ variables, each independent of the demands before period $t$. In steady state every $D_t$ has the law $N\big(d/(1-\rho),\ \sigma^2/(1-\rho^2)\big)$. The retailer replenishes with a lead time of $L$ 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 $m \ge 1$ demands:

$$\hat\mu^L_t = \frac{L}{m}\sum_{i=1}^m D_{t-i}, \qquad \hat\sigma^L_{et} = C\sqrt{\frac{1}{m}\sum_{i=1}^m e_{t-i}^2}, \qquad e_t = D_t - \hat\mu^1_t,$$

and sets the base-stock level $S_t = \hat\mu^L_t + z_\alpha \hat\sigma^L_{et}$, where $z_\alpha$ is a safety factor. The book writes the constant in $\hat\sigma^L_{et}$ as $C_{L\rho}$ and does not give its form; here it is a free parameter $C$. Each period the retailer orders $Q_t = S_t - S_{t-1} + D_{t-1}$, 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. $N$ retailers face independent $N(\mu, \sigma^2)$ demands in every period and each orders once every $R \ge 1$ periods, the order being its demand over the previous $R$ 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 $R$ days, so the number $X$ of retailers ordering on a given day is binomial$(N, 1/R)$; positively correlated ordering, in which all retailers order on the same day, so $X = N$ with probability $1/R$ and $0$ otherwise; and balanced ordering, in which the retailers are spread as evenly as possible, so with $N = MR + k$, $0 \le k < R$, $X$ is $M+1$ with probability $k/R$ and $M$ otherwise. The structure BatchOrders P N R mu sigma carries the demands, the ordering count $X$ independent of them, and supplierOrder, the sum of the last $R$ demands of retailers $1, \dots, X$; each pattern enters a theorem as a hypothesis on the law of $X$.

Rationing game. Two identical retailers face single-period demand with distribution function $F$, holding cost $h$ and stockout penalty $p$, so the newsvendor quantity $Q^*$ satisfies $F(Q^*) = p/(h+p)$. With probability $r$ the supplier can deliver only $A_1 < 2Q^*$ units in total and allocates them pro rata to the orders, retailer 1 receiving $A_1 Q_1/(Q_1 + Q_2)$; with probability $1 - r$ supply is unlimited. Retailer 1's expected cost when the retailers order $Q_1$ and $Q_2$ is

$$g_1(Q_1) = (1-r)\,\mathrm{nv}(Q_1) + r\,\mathrm{nv}\!\Big(\frac{A_1 Q_1}{Q_1 + Q_2}\Big),$$

with $\mathrm{nv}$ the newsvendor cost; this is rationingCost.

Formalization targets

Goal: Theorem 13.2, demand signal processing

$$\frac{\mathrm{Var}[Q_t]}{\mathrm{Var}[D_t]} \;\ge\; 1 + \Big(\frac{2L}{m} + \frac{2L^2}{m^2}\Big)(1 - \rho^m),$$

with equality when $z_\alpha = 0$. This is bullwhip_signal_processing. The bound exceeds $1$ whenever $L > 0$, whatever the value of $\rho$: a lead time and a moving-average forecast are enough to produce the effect.

Supporting targets

The chapter's own route to the goal, each a milestone: the steady-state moments (13.2) to (13.4), $\mathbb{E}[D_t] = d/(1-\rho)$, $\mathrm{Var}[D_t] = \sigma^2/(1-\rho^2)$ and $\mathrm{Cov}[D_t, D_{t-k}] = \rho^k \mathrm{Var}[D_t]$; the identity $Q_t = (1 + L/m) D_{t-1} - (L/m) D_{t-m-1} + z_\alpha(\hat\sigma^L_{et} - \hat\sigma^L_{e,t-1})$; Lemma 13.1, $\mathrm{Cov}[D_{t-i}, \hat\sigma^L_{et}] = 0$ for $1 \le i \le m$; the vanishing of the cross term (13.12); and the variance of the demand part, $\big(1 + (2L/m + 2L^2/m^2)(1 - \rho^m)\big)\mathrm{Var}[D_t]$.

Order batching, Theorem 13.4: under the three patterns the supplier's order has mean $N\mu$ and

$$\mathrm{Var}[Q^c_t] \ge \mathrm{Var}[Q^r_t] \ge \mathrm{Var}[Q^b_t] \ge N\sigma^2,$$

through the three variance formulas $N\sigma^2 + \mu^2 N(R-1)$, $N\sigma^2 + \mu^2 N^2 (R-1)$ and $N\sigma^2 + \mu^2 k(R-k)$.

The rationing game, Theorem 13.3: if $Q > 0$ is a symmetric Nash equilibrium, that is, $Q$ minimizes $g_1$ over positive order quantities when the other retailer orders $Q$, then $Q > Q^*$.

Significance

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 $k$; its comparative statics, the bound decreasing in $m$ and increasing in $L$, 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 $Q_t$ 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.

Difficulty

The obvious computation of $\mathrm{Var}[Q_t]$ 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: $\hat\sigma^L_{et}$ is a square root of a sum of squares of forecast errors, a nonlinear function of $m + m$ demands, and its covariance with a single demand is zero only because the errors are jointly Gaussian with mean zero and $\hat\sigma$ 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, $\mathrm{Cov}[D_{t-1}, \hat\sigma^L_{e,t-1}]$ and $\mathrm{Cov}[D_{t-m-1}, \hat\sigma^L_{et}]$, which the book reduces to the lemma through the recursion (the second reduction divides by $\rho$) but which hold for every $\rho$ 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 $D_t$ and the independence of $\epsilon_t$ from the past, and the autocovariance $\rho^k \mathrm{Var}[D_t]$ 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 $X$: given $X = x$ the supplier's order is a sum of $xR$ independent normals, so its conditional mean is $xR\mu$ and conditional variance $xR\sigma^2$, and the total variance is $\mathbb{E}[\mathrm{Var}[Q \mid X]] + \mathrm{Var}[\mathbb{E}[Q \mid X]]$. The order is defined by a sum over retailers $i < X$, so the independence of $X$ 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 $(h+p)F(y) - p$, which holds when $F$ is continuous, and that the symmetric equilibrium be an interior minimizer, which is why $Q > 0$ and the minimization over $Q_1 > 0$ are hypotheses.

Formalization scope

Time is indexed by $\mathbb{Z}$ so that $D_{t-m-1}$ exists for every $t$. AR1Demand asserts the recursion for every outcome, the independence of the whole error family, the independence of $\epsilon_t$ from $(D_s)_{s < t}$, and the stationary law of every $D_t$; 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 $C_{L\rho}$ is a free real parameter $C$; no theorem depends on its value.

The goal divides by $\mathrm{Var}[D_t]$, which is $\sigma^2/(1-\rho^2) > 0$ under the structure's hypotheses $\sigma > 0$ and $|\rho| < 1$, 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, $\hat\sigma^L_{et}$ included.

In BatchOrders the demands are indexed by Fin N × Fin R, the count $X$ is a natural-valued random variable bounded by $N$ and independent of the demand family, and supplierOrder sums the $R$ demands of retailers $1, \dots, X$, the book's "without loss of generality" choice. The laws of $X$ are hypotheses on point probabilities P.real {ω | X ω = j}; with $R \ge 1$ each of the three families of hypotheses is satisfiable by a structure with the corresponding law. The subtractions $R - 1$ and $R - k$ are real.

In the rationing game the demand law is a probability measure on $\mathbb{R}$ whose distribution function is continuous and strictly increasing on $[0, \infty)$; the newsvendor loss is assumed integrable at every order quantity. The pro-rata allocation uses Lean's total division, which is never at $0$ in the theorem since $Q_1 + Q_2 > 0$.

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.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 13. https://doi.org/10.1002/9781119584445
• H. L. Lee, V. Padmanabhan and S. Whang, Information distortion in a supply chain: the bullwhip effect, Management Science 43(4), 1997. https://doi.org/10.1287/mnsc.43.4.546
• F. Chen, Z. Drezner, J. K. Ryan and D. Simchi-Levi, Quantifying the bullwhip effect in a simple supply chain: the impact of forecasting, lead times, and information, Management Science 46(3), 2000. https://doi.org/10.1287/mnsc.46.3.436.12069
• G. P. Cachon, Managing supply chain demand variability with scheduled ordering policies, Management Science 45(6), 1999. https://doi.org/10.1287/mnsc.45.6.843
• Y. Rong, Z.-J. M. Shen and L. V. Snyder, The impact of ordering behavior on order-quantity variability: a study of forward and reverse bullwhip effects, Naval Research Logistics 64(1), 2017. https://doi.org/10.1002/nav.21757

Motivation

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 $0=\max_{a\in A_s}\{r(s,a)-g+\sum_jp(j\mid s,a)h(j)-h(s)\}$, whose unknowns are a scalar gain $g$ and a bias function $h$. 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.

Setting

The model is stationary (Assumption 8.0.1): a finite set $S$ of states, for each $s$ a finite nonempty set $A_s$ of actions, a reward $r(s,a)$ and transition probabilities $p(j\mid s,a)$, none depending on the decision epoch. A policy $\pi\in\Pi^{HR}$ may randomize and may depend on the whole history; the deterministic stationary policy $d^\infty$ applies the decision rule $d:S\to A$ at every epoch. Its transition matrix is $P_d(i,j)=p(j\mid i,d(i))$.

For a policy $\pi$, $v^\pi_{N+1}(s)=\mathbb E^\pi_s[\sum_{t=1}^Nr(X_t,Y_t)]$ is the expected reward over $N$ epochs. Since the limit of $N^{-1}v^\pi_{N+1}(s)$ need not exist (Example 8.1.1), the chapter works with the lim sup and lim inf average rewards $g^\pi_+(s)$ and $g^\pi_-(s)$, and with $g^*_\pm(s)=\sup_{\pi}g^\pi_\pm(s)$. A policy $\pi^*$ is average optimal when $g^{\pi^*}_-(s)\ge g^\pi_+(s)$ for all $s$ and $\pi$, the strongest of the three criteria of Section 8.1.2.

The optimality residual is $B(g,h)(s)=\max_{a\in A_s}\{r(s,a)-g+\sum_jp(j\mid s,a)h(j)-h(s)\}$, and the optimality equation is $B(g,h)=0$. A decision rule is $h$-improving when it attains $\max_{a\in A_s}\{r(s,a)+\sum_jp(j\mid s,a)h(j)\}$ 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 $P_d$ is unichain for every deterministic decision rule.

Formalization targets

Goal — Theorem 8.4.5 (printed p. 361)

For a finite unichain model: (a) some deterministic stationary policy is average optimal; (b) the optimality equation $B(g^*,h^*)=0$ has a solution, and (d) its scalar satisfies $g^*_+(s)=g^*_-(s)=g^*$ for every $s$; (c) for every solution, every $h^*$-improving decision rule gives an average optimal stationary policy.

Theorem 8.4.1 (printed p. 356)

If $B(g,h)\le 0$ then $g\ge g^*_+$; if $B(g,h)\ge 0$ then $g\le\sup_{d}g^{d^\infty}_-\le g^*_-$; if $B(g,h)=0$ then $g^*_+=g^*_-=g$.

Theorem 8.4.3 (printed p. 358)

In a finite unichain model $B(g,h)=0$ has a solution, and every solution has the same $g$.

Theorem 8.4.4 (printed p. 361)

If $B(g^*,h^*)=0$ and $d^*$ is $h^*$-improving, then $(d^*)^\infty$ is average optimal.

Significance

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 $g$ 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 $(g,h)$, 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.

Difficulty

The obvious argument for Theorem 8.4.3 is to take the discounted optimal value $v^*_\lambda$ of mission II and let $\lambda\uparrow 1$. It fails as stated because $v^*_\lambda$ blows up like $(1-\lambda)^{-1}$; what converges is the Laurent expansion $v^{d^\infty}_\lambda=(1-\lambda)^{-1}ge+h+o(1)$ of the value of a fixed stationary policy, Corollary 8.2.4, and that expansion needs the limiting matrix $P_d^*$ and the deviation matrix $H_{P_d}$ 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 $D^{MD}$ 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 $ge\ge r_d+(P_d-I)h$ along an arbitrary history-dependent policy and dividing by $N$ requires the telescoping term $N^{-1}(P^\pi_N-I)h$ to vanish, which uses boundedness of $h$, 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 $r_d-ge+(P_d-I)h=0$ forces the gain of $d^\infty$ to be $g$, which is the multiplication by $P_d^*$ that annihilates $(P_d-I)$.

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 $a_{1,1}$ has the absorbing state $s_2$ 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.

Formalization scope

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 $N^{-1}v^\pi_{N+1}(s)$ on $\mathbb R$; these are the source's because the sequence is bounded by $\max|r|$, and the suprema $g^*_\pm$ over the nonempty family of policies are genuine real suprema for the same reason. The residual $B(g,h)$ is a Finset.sup' over the admissible actions. Recurrence is "every state reachable from $i$ reaches $i$" and unichain is "any two recurrent states communicate", the definitions of Appendix A for finite chains, applied to $P_d$ 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 $S$ where the source says countable, since the chapter's standing assumption and the model are finite; the gain $g^{d^\infty}$ of a stationary policy in (8.4.5) is written as its lim inf gain, which equals it; and the chain $ge=g^*=g^*_+=g^*_-$ of (8.4.6) is stated through $g^*_+$ and $g^*_-$, since $g^*$ presupposes existing limits. Nothing is trivialized: the existential in Theorem 8.4.5(a) has to produce a decision rule, and $B(g,h)=0$ with a junk maximum is impossible since every $A_s$ 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.

Selected references

• Martin L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, Chapter 8. doi:10.1002/9780470316887
• Ronald A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• David Blackwell, Discrete dynamic programming, Annals of Mathematical Statistics 33 (1962). doi:10.1214/aoms/1177704593
• Cyrus Derman, Finite State Markovian Decision Processes, Academic Press, 1970.
• Paul J. Schweitzer and Awi Federgruen, The functional equations of undiscounted Markov renewal programming, Mathematics of Operations Research 3 (1978). doi:10.1287/moor.3.4.308