Dynamic Programming

Motivation

Value iteration is the standard method for solving a discounted Markov decision process (MDP), and its policy-evaluation variant, value computation (VC), computes the value of a fixed policy by iterating an affine contraction. Both converge geometrically at rate $\lambda$, the discount factor. When $\lambda$ is close to one, as in long-horizon reinforcement-learning benchmarks ($\lambda = 0.99$ or $0.999$), the number of iterations grows like $1/(1-\lambda)$, and each iteration costs a full sweep over states and actions.

In convex optimization, gradient descent on a $\mu$-strongly convex, $L$-smooth function has the same kind of rate, and Nesterov's acceleration improves the dependence on the condition number $\kappa = L/\mu$ from $\kappa$ to $\sqrt\kappa$. Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) read $v - T(v)$ as a gradient with "strong convexity" $1-\lambda$ and "smoothness" $1+\lambda$, transfer Nesterov's and Polyak's step sizes to value iteration, and ask when the transferred methods are actually faster. This mission covers the first answer they give: for policy evaluation on a reversible chain, the accelerated scheme converges at a rate of order $1-\sqrt{1-\lambda}$ instead of $\lambda$.

Setting

An MDP has a finite set of states $\mathbb S$ with $|\mathbb S| = n$, a finite set of actions $\mathbb A$, transition probabilities $P_{iaj}$ (from state $i$ to state $j$ under action $a$; each $P_{ia\cdot}$ is a probability distribution), real rewards $r_{ia}$, and a discount factor $\lambda \in (0,1)$. A policy $\pi$ assigns to every state $i$ a probability distribution $\pi_{i\cdot}$ over actions. It induces the reward vector $r_{\pi,i} = \sum_a \pi_{ia} r_{ia}$, the transition matrix $L_{\pi,ij} = \sum_a \pi_{ia}P_{iaj}$, the policy operator $T_\pi(v) = r_\pi + \lambda L_\pi v$, and the value function

$$v^\pi = \sum_{t\ge0}\lambda^t L_\pi^t r_\pi,$$

the expected discounted reward when actions are drawn from $\pi$. VC iterates $v_{s+1} = T_\pi(v_s)$.

Accelerated Value Computation (A-VC) starts from arbitrary $v_0, v_1 \in \mathbb R^n$ and sets, for $s \ge 1$,

$$h_s = v_s + \gamma\,(v_s - v_{s-1}),\qquad v_{s+1} = h_s - \alpha\,\big(h_s - T_\pi(h_s)\big),$$

with the constant step sizes $\alpha = 1/(1+\lambda)$ and $\gamma = (1-\sqrt{1-\lambda^2})/\lambda$. Write $\kappa = (1+\lambda)/(1-\lambda)$.

A transition matrix $L$ is reversible if it is irreducible (every state reaches every other with positive probability in some number of steps) and has a stationary probability distribution $\nu$ satisfying detailed balance, $\nu_iL_{ij} = \nu_jL_{ji}$ for all $i, j$.

The analysis runs through the $2n\times2n$ matrix

$$B_\pi = \begin{bmatrix}(1-\sqrt{1/\kappa})(I+L_\pi) & -\tfrac12(1-\sqrt{1/\kappa})^2(I+L_\pi)\\ I & 0\end{bmatrix},$$

whose powers propagate the stacked error $x_s - x^\pi$, where $x_s = (v_s, v_{s-1})$ and $x^\pi = (v^\pi, v^\pi)$. Its spectral radius $\rho(B_\pi)$ is the largest modulus of a complex eigenvalue.

Formalization targets

Goal: Theorem 5.1

If $L_\pi$ is irreducible and reversible, then $v_s \to v^\pi$, and for every $\eta > 0$

$$v_s = v^\pi + o\Big(\big(1-\sqrt{1/\kappa}+\eta\big)^s\Big),\qquad 0 < 1-\sqrt{1/\kappa} < \lambda.$$

The goal is stated with the $\eta$ slack because the iteration matrix has a defective leading eigenvalue: the error is of exact order $s\,(1-\sqrt{1/\kappa})^s$ in general, so a clean $O\big((1-\sqrt{1/\kappa})^s\big)$ bound is false.

Milestones

1. The step-size identities of the proof of Lemma 5.2: $1+1/\kappa-2\alpha=0$, $(1-\alpha)(1+\gamma)=\alpha\lambda(1+\gamma)=1-\sqrt{1/\kappa}$, $\alpha\gamma\lambda=(1-\alpha)\gamma=\alpha-\sqrt{1/\kappa}=\tfrac12(1-\sqrt{1/\kappa})^2$.
2. Lemma 5.2: $x_s = x^\pi + B_\pi^{s-1}(x_1-x^\pi)$ for all $s\ge1$.
3. The eigenvalues of a reversible transition matrix are real (§2, p. 4).
4. $\operatorname{Sp}(L_\pi)\subset[-1,1]$ for a reversible policy chain.
5. (5.3): each eigenvalue $\omega$ of $B_\pi$ solves $\omega^2-(\mu+1)(1-\sqrt{1/\kappa})\omega+\tfrac12(\mu+1)(1-\sqrt{1/\kappa})^2=0$ for some $\mu\in\operatorname{Sp}(L_\pi)$.
6. For $\mu\in[-1,1]$: $\tfrac12|\mu+1\pm\sqrt{\mu^2-1}|\le1$.
7. Lemma 5.3: $\rho(B_\pi) = 1-\sqrt{1/\kappa}$.
8. (5.6): $\lambda = 1-\sqrt{1/\kappa}+\sqrt{1-\lambda}\,(1-\sqrt{1-\lambda^2})/\sqrt{1+\lambda}$, with a positive last term.

Significance

The result. Since $1-\sqrt{1/\kappa} = 1-\sqrt{(1-\lambda)/(1+\lambda)}$, A-VC reaches an $\epsilon$-approximation of $v^\pi$ in $O\big((1-\lambda)^{-1/2}\log(1/(\epsilon(1-\lambda)))\big)$ iterations against $O\big((1-\lambda)^{-1}\log(1/(\epsilon(1-\lambda)))\big)$ for VC, at the same per-iteration cost. This matches the rate of Nesterov's method for strongly convex functions with the paper's identification of the constants. The same paper shows that this improvement does not extend to arbitrary MDPs: Theorem 6.3 gives a lower bound $\lambda^s/(1+\lambda)$ for every first-order method on a chain MDP, which is why reversibility (or a real spectrum, Remark 5.4) is needed here.

Formalizing it. The result is proved in the paper; no machine-checked proof exists. A formal proof needs the reality of the spectrum of reversible chains, the localization of the spectrum of a structured block matrix, and the passage from the spectral radius to a little-o rate for a matrix with a nontrivial Jordan block. The paper's printed statement puts $\eta$ under the square root, $o\big((1-\sqrt{1/\kappa+\eta})^s\big)$. That rate is faster than $\rho(B_\pi)$ and is false (a one-state chain is a counterexample). The mission poses the rate $(1-\sqrt{1/\kappa}+\eta)^s$ that the paper's own proof concludes on p. 9. This is one of four missions from this paper; the other three pose Theorem 5.5 (momentum value computation), Theorem 6.3 (the first-order lower bound) and Theorem 7.1 (safe accelerated value iteration).

Difficulty

The obvious argument says "$\rho(B_\pi)<1$, so $B_\pi^s\to0$ at rate $\rho(B_\pi)$". That argument breaks twice. First, computing $\rho(B_\pi)$ requires knowing where the eigenvalues of $L_\pi$ lie. For a general stochastic matrix they fill the unit disk, and then the roots of (5.3) can exceed $1-\sqrt{1/\kappa}$ in modulus. Reversibility is what confines them to $[-1,1]$, and the reality of the spectrum of a reversible chain is not in Mathlib. Second, the eigenvalue $1-\sqrt{1/\kappa}$ of $B_\pi$ (coming from $\mu=1$) is a double root of (5.3) with a single eigenvector, so $\|B_\pi^s\|$ is not $O(\rho^s)$; only the $\eta$-relaxed little-o holds. The eigenvalues of $B_\pi$ are non-real for $\mu\in(-1,1)$, so the whole computation must be done over $\mathbb C$.

Formalization scope

• Data. $\mathbb S$ and $\mathbb A$ are finite types. The MDP is the data $(P, r, \lambda)$. Validity (stochastic $P_{ia\cdot}$, $\lambda\in(0,1)$) and the policy property are hypotheses. Rewards are arbitrary reals. The initial-state distribution $p_0$ of the paper's tuple is omitted, since nothing here uses it.
• Reused definitions. $r_\pi$, $L_\pi$, $v^\pi$, policies and the kernel condition are the published FoundationsML.ReinforcementLearning definitions; irreducibility, stationarity and detailed balance are the published mm_basic. $v^\pi$ is the discounted reward series, not an arbitrary fixed point of $T_\pi$.
• Reversibility is irreducibility plus a stationary probability vector in detailed balance. Detailed balance alone would be satisfied by $\nu=0$ and is not used.
• Norms and rates. Vectors are functions $\mathbb S\to\mathbb R$ with the sup norm $\|\cdot\|_\infty$; "$o(\cdot)$" is Mathlib's little-o along $s\to\infty$.
• Spectra are complex: $\rho(B_\pi)$ is the spectral radius of the complexified matrix, valued in $[0,\infty]$. Using the real spectrum would make Lemma 5.3 a different, weaker statement.
• Indexing. A-VC is a sequence on $\mathbb N$ with $v_0, v_1$ given; $x_s = (v_s, v_{s-1})$ is used only for $s\ge1$.
• Pinned relative to the page. In the goal, $\eta$ is outside the square root, as in the proof. In milestone 6, $\sqrt{\mu^2-1}$ is written as $i\sqrt{1-\mu^2}$, its value for $\mu\in[-1,1]$.

Ruling out trivial readings: the hypotheses are satisfiable (a two-state chain with $P_{iaj}=1/2$ is valid, reversible and has a policy), the rate is stated with $\forall\eta>0$ rather than for some $\eta$, and $v^\pi$ is a fixed object rather than a variable constrained by hypotheses.

Needed infrastructure, reusable beyond this mission: the reality and location of the spectrum of reversible stochastic matrices (also used by the sibling mission on momentum value computation); spectra of $2\times2$ block matrices with commuting blocks; and the bound $\|M^s\| = o((\rho(M)+\eta)^s)$ from Gelfand's formula. Contributions of any of these as stand-alone lemmas are welcome.

Selected references

• V. Goyal, J. Grand-Clément, A First-Order Approach to Accelerated Value Iteration, Operations Research 71(2), 2023; arXiv:1905.09963v7 (2021). https://arxiv.org/abs/1905.09963
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Springer, 2004 (reprint 2013). https://doi.org/10.1007/978-1-4419-8853-9
• P. Brémaud, Markov Chains: Gibbs Fields, Monte Carlo Simulation, and Queues, Springer, 1999 (reprint 2013), Ch. 6. https://doi.org/10.1007/978-1-4757-3124-8
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994 (reprint 2014). https://doi.org/10.1002/9780470316887

Motivation

An insurance company's surplus grows with premiums and falls with claims. In the Cramér–Lundberg model with a positive safety loading, the surplus drifts to $+\infty$ with probability one. De Finetti (1957) objected that a company does not accumulate capital indefinitely: surplus above some level is paid out to shareholders. He proposed choosing the payout policy to maximize the expected discounted dividends paid before ruin. This is the optimal dividend problem. It is one of the basic stochastic control problems of actuarial mathematics and corporate finance, and it serves as a test case for singular control of processes with jumps.

The classical answer is a barrier strategy: pay out whatever lifts the surplus above a level $a$ and nothing else. Jeanblanc and Shiryaev (1995) proved this optimal when the surplus is a Brownian motion with drift, and Gerber and Shiu studied the same Brownian setting. Azcue and Muler (2005) showed that it can fail in the Cramér–Lundberg model, where the optimal policy may be a band strategy. Avram, Palmowski and Pistorius (Ann. Appl. Probab. 17 (2007) 156–180) treated a general spectrally negative Lévy process, a process with stationary independent increments and only downward jumps. They found the value of every barrier strategy in closed form through the scale function of the process and identified the best barrier level $c^*$. They also gave a verification condition under which the barrier at $c^*$ is optimal among all strategies. Loeffen (2008) later showed that the condition holds whenever the Lévy measure has a completely monotone density.

Setting

Let $X=(X_t)_{t\ge0}$ be a spectrally negative Lévy process on a filtered probability space $(\Omega,\mathcal F,\mathbb F,P)$ with $X_0=0$ and Lévy triplet $(c,\sigma,\nu)$. Its Laplace exponent is $\psi(\theta)=\log\mathbf E[e^{\theta X_1}]$, finite for $\theta\ge0$:

$$\psi(\theta)=c\theta+\tfrac{\sigma^2}{2}\theta^2+\int_{(-\infty,0)}\bigl(e^{\theta y}-1-\theta y\mathbf 1_{\{|y|<1\}}\bigr)\nu(dy).$$

Increments after time $s$ are independent of $\mathcal F_s$. Initial capital $x$ is added to $X$. The standing assumptions are the following: $X$ does not have monotone paths, $\mathbf E[X_1]>-\infty$, and either $\sigma>0$, $\int_{(-1,0)}|y|\,\nu(dy)=\infty$, or $\nu$ has a density.

A dividend strategy is a nondecreasing, left-continuous, adapted process $L$ with $L_0=0$. The risk process is $U_t=x+X_t-L_t$ and the ruin time is $\sigma^L=\inf\{t\ge0:U_t<0\}$. The strategy is admissible ($L\in\Pi$) if no lump sum exceeds the current reserves. Its value is

$$v_L(x)=\mathbf E\Bigl[\int_0^{\sigma^L}e^{-qt}\,dL_t\Bigr],\qquad v_*(x)=\sup_{L\in\Pi}v_L(x),$$

with discount rate $q>0$. For $C\in[0,\infty]$, $\Pi_{\le C}$ consists of the admissible strategies that keep $U_t\le C$ for $t>0$.

The $q$-scale function $W=W^{(q)}$ is the unique continuous nondecreasing function on $[0,\infty)$ with $\int_0^\infty e^{-\theta y}W(y)\,dy=1/(\psi(\theta)-q)$ for large $\theta$. It is extended by $W=0$ on $(-\infty,0)$. The barrier strategy $\pi_a$ reflects $x+X$ at the level $a$, paying $(x-a)^+$ at time $0$. The paper computes its value

$$v_a(x)=\frac{W(x)}{W'(a)}\ (0\le x\le a),\qquad v_a(x)=x-a+\frac{W(a)}{W'(a)}\ (x>a),$$

and the optimal barrier level is $c^*=\inf\{a>0: W'(a)\le W'(x)\ \forall x>0\}$, read as $0$ when this set is empty and $W'(0+)\le W'(x)$ for all $x>0$. The generator is

$$\Gamma f(x)=\tfrac{\sigma^2}{2}f''(x)+cf'(x)+\int_{(-\infty,0)}[f(x+y)-f(x)-f'(x)y\mathbf 1_{\{|y|<1\}}]\,\nu(dy).$$

Formalization targets

Goal: Theorem 2 (p. 14)

Assume $\sigma>0$, or $X$ has bounded variation, or $v_{c^*}\in C^2(0,\infty)$. Then $c^*<\infty$ and:

$$\text{(i)}\quad \pi_{c^*}\in\Pi_{\le c^*},\qquad v_{\pi_{c^*}}(x)=v_{c^*}(x)=\sup_{\pi\in\Pi_{\le c^*}}v_\pi(x)\quad(x\ge0);$$ $$\text{(ii)}\quad (\Gamma v_{c^*}-qv_{c^*})(x)\le0\ \ \forall x>c^*\ \Longrightarrow\ v_*(x)=v_{c^*}(x)\ (x\ge0),\ \ \pi_*=\pi_{c^*}.$$

The goal fixes no constants: the barrier level and the value function are both given by the scale function of the given process.

Milestones

• Proposition 1 (p. 7): $v_{\pi_a}(x)=W(x)/W'(a)$ for $a>0$, $x\in[0,a]$.
• Lemma 2(i) (p. 15): $c^*<\infty$.
• Proposition 3(i) (p. 15): $v_a(x)\le v_{c^*}(x)$ for $x\in[0,c^*]$, $a\ge0$.
• Lemma 3(i) (p. 16): $v_{c^*}'(x)\ge1$ for $x>0$.
• Proposition 4(i) (p. 18): a $C^2$ (unbounded variation) or $C^1$ (bounded variation) solution $w$ of $\max\{\Gamma w-qw,1-w'\}=0$ on $(0,C)$ dominates $\sup_{\Pi_{\le C}}v_\pi$.
• Lemma 4 (p. 20): $(\Gamma v_{c^*}-qv_{c^*})(x)=0$ on $(0,c^*)$ when $c^*>0$.

Significance

The theorem gives an explicit solution to a singular control problem for a general Lévy model. The candidate value function and barrier level are expressed through one special function, $W^{(q)}$, and optimality over all strategies reduces to one inequality on $(c^*,\infty)$. It is the basis of the later literature on scale-function methods in dividend problems (Loeffen 2008, Kyprianou–Rivero–Song 2010, and the refracted and Parisian variants). Part (i) holds with no condition on the Lévy measure. Part (ii) shows exactly where barrier optimality can fail.

The paper's proofs use fluctuation identities (exit problems, excursion theory) and Itô's formula for semimartingales with jumps. None of these is in Mathlib. As far as is known, none of these results has been machine-checked. A formalization would produce a Lévy-process and scale-function layer, a formal model of singular control with jumps and lump-sum payments, and a checked verification argument. Each of these can be reused beyond this paper.

Difficulty

The analytic part is elementary once the value formula (5.1) is available: the choice of $c^*$, Proposition 3(i) and Lemma 3(i) follow from the shape of $W'$. The difficulty lies in the two probabilistic steps. Proposition 1 identifies the value of a reflected process through exit identities for $X$. Those identities rest on excursion theory, or on the martingale property of $e^{-qt}W(X_t)$ up to exit. The verification step, Proposition 4(i), needs Itô's formula for $w(U_t)$. Here $U$ is a jump process controlled by a left-continuous finite-variation process that may itself jump. The change-of-variables formula must also run under only $C^1$ regularity when $X$ has bounded variation. Just proving that $\Gamma w-qw\le0$ and $w'\ge1$ imply a supermartingale inequality does not settle the question: the lump-sum payments and the jumps of $X$ enter the Itô expansion separately and must each be bounded.

Formalization scope

Time is $[0,\infty)$ (ℝ≥0). $X$ is a structure carrying the triplet $(c,\sigma,\nu)$ and pathwise càdlàg paths with only downward jumps. It also carries independence of increments from the filtration and stationarity. Its law is fixed by the Laplace transform $\mathbf E[e^{\theta X_t}]=e^{t\psi(\theta)}$ for $\theta\ge0$. The standing assumptions of §2 and (3.3) are bundled as one predicate. The scale function is a hypothesis on a function argument $W$ (it is unique). $W'(0+)$ is an extended real, since it is $+\infty$ for unbounded variation without a Gaussian part.

Values of strategies and value functions lie in $[0,\infty]$. The dividend integral is a Lebesgue–Stieltjes integral over $[0,\sigma^L)\cup\{0\}$: it counts the lump sum at time $0$ and excludes a payment at the ruin instant.

Several conventions are fixed, and each is disclosed in the item it affects:

• Admissibility. The paper requires $L_{t+}-L_t<U_t$. The formalization uses $\le$, because the paper's own strategy of paying out everything at once needs it.
• Barrier level (5.2). Printed over $a>0$ and "all $x$", the defining set is empty for Brownian motion with nonpositive drift. The printed set (with $x>0$) is kept whenever it is nonempty; when it is empty and $W'(0+)\le W'(x)$ for all $x>0$ — the second alternative in the proof of Lemma 2(i) — $c^*=0$, and otherwise $c^*=\infty$.
• Printed slips. The integral $\int_{-1}^0 x\,\nu(dx)$ in (3.3) is read as $\int|x|\,\nu(dx)$. In (3.4), $e^{-\theta x}$ is read as $e^{-\theta y}$, and in Theorem 2(i), $\pi^*_c$ is read as $\pi_{c^*}$.
• Proposition 4(i) is stated for initial capital $x\le C$. Beyond $C$, $w$ is unconstrained and the printed claim fails.
• Lemma 4 carries the smoothness proviso of Theorem 2 on $(0,c^*)$.

A trivializing encoding is ruled out: the value is not a real supremum, the barrier strategy is constructed rather than assumed, and $c^*<\infty$ is a conclusion.

A complete development needs:

• Lévy processes and their Laplace exponents;
• scale functions and the exit identity $\mathbf E_x[e^{-qT}\mathbf 1_{\{X_T=a\}}]=W(x)/W(a)$;
• reflected processes;
• Itô's formula for jump semimartingales with finite-variation controls.

The Lévy and scale-function layer is shared with the companion mission on the bail-out problem. Contributions of general lemmas (Stieltjes integration by parts, optional stopping for càdlàg martingales) are welcome.

Selected references

• F. Avram, Z. Palmowski, M. R. Pistorius, On the optimal dividend problem for a spectrally negative Lévy process, Ann. Appl. Probab. 17 (2007) 156–180. https://arxiv.org/abs/math/0702893
• P. Azcue, N. Muler, Optimal reinsurance and dividend distribution policies in the Cramér–Lundberg model, Math. Finance 15 (2005) 261–308.
• M. Jeanblanc-Picqué, A. N. Shiryaev, Optimization of the flow of dividends, Russian Math. Surveys 50 (1995) 257–277.
• R. L. Loeffen, On optimality of the barrier strategy in de Finetti's dividend problem for spectrally negative Lévy processes, Ann. Appl. Probab. 18 (2008) 1669–1680.
• A. E. Kyprianou, Introductory Lectures on Fluctuations of Lévy Processes with Applications, Springer, 2006. https://doi.org/10.1007/978-3-540-31343-4

Motivation

Gittins index policies are optimal for a single server choosing among alternative bandit processes, and the achievable region method of Bertsimas and Niño-Mora (Math. Oper. Res. 1996) explains why: when the performance vectors of a scheduling system satisfy generalized conservation laws, the region they fill is a polytope whose optimal vertex is an index priority. Most real systems have several servers working in parallel, and for them the conservation laws fail. Glazebrook and Wilkinson (Ann. Appl. Probab. 2000) observed that $M$ parallel machines are close to a single machine working at $M$ times the speed, where the laws do hold, and turned that closeness into explicit bounds on how much an index policy can lose. Section 5.7 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., Wiley 2011, doi:10.1002/9780470980033), presents that analysis for the simple family of alternative bandit processes (SFABP). Its first quantitative output is an upper bound on the optimal return, Corollary 5.20. This bound is the reference point against which the index heuristics of the rest of the section are measured.

This mission continues the public series Multi-armed Bandit Allocation Indices I–VI. Mission IV of that series formalized the single-machine achievable region theory of Chapter 5: Lemma 5.1, Theorems 5.5 and 5.10, and the identity of the adaptive greedy indices with Gittins indices.

Setting

There are $n$ arms. Arm $b$ has a finite state space $E_b$; the $E_b$ are disjoint, and their union $E = \{1, \dots, N\}$ is the set of job types. One transition kernel $P$ on $E$ moves an arm when it is processed. Each $E_b$ is closed under $P$, and $P$ is irreducible on each $E_b$. Time is discrete, rewards are discounted by $a^t$ with $0 < a < 1$, and processing a job of type $i$ earns $r_i$. There are $M$ identical machines, $1 \le M \le n$. At each time $t = 0, 1, 2, \dots$ a policy $\pi$ chooses, on the basis of the history, a set of exactly $M$ arms. Each chosen arm makes one transition and the others are frozen. From the initial state-vector $k$, the performance $x_i^\pi(k)$ is the expected total discounted number of times a job of type $i$ is processed. The return is $R^\pi(k) = \sum_{i \in E} r_i x_i^\pi(k)$, and $R^{\mathrm{opt}}(k) = \sup_\pi R^\pi(k)$.

The matrix $A = (A_i^S)$ is the single-arm matrix of §5.3, published in the series as conservationCoeff: for $i \in S$, $A_i^S = E[1 + a + \cdots + a^{T_i^S - 1}]$, where $T_i^S \ge 1$ is the number of transitions the chain started at $i$ needs to return to $S$, and $A_i^S = 0$ otherwise. Job types are numbered in ascending order $\nu_1 \le \cdots \le \nu_N$ of the indices produced by the adaptive greedy algorithm $\mathrm{AG}(A, r)$ (IsAdaptiveGreedy, greedyIndex), and $S_i = \{1, \dots, i\}$. Write

$$A^\pi(S, k) = \sum_{i \in E} A_i^S x_i^\pi(k), \qquad A(S, k) = \inf_\pi A^\pi(S, k).$$

Let $\psi_i$ be the number of arms with no job type in $S_i$, let $i_b = \min E_b$, and number the arms so that $i_1 \le \cdots \le i_n$. For each other arm, $T_{k_b}^{S_i}$ is the processing needed to bring it from $k_b$ into $S_i$ for the first time, and $T_k^{S_i}$ is the sum of these over the other arms, which evolve independently.

Formalization targets

Goal: Corollary 5.20 (p. 142)

$$R^{\mathrm{opt}}(k) \le \nu_N \Big(\frac{M}{1-a}\Big) - \Big(\frac{1}{1-a}\Big) \sum_{i = i_{n-M+1}}^{N-1} (\nu_{i+1} - \nu_i)(M - \psi_i)\, E\Big[a^{T_k^{S_i}/(M - \psi_i)}\Big].$$

Milestones

• Eq. (5.21) in the form of p. 139: $r_j = \nu_N - \sum_{i=j}^{N-1} (\nu_{i+1} - \nu_i) A_j^{S_i}$.
• Eq. (5.25): for every policy, $R^\pi(k) = \nu_N \frac{M}{1-a} - \sum_{i=1}^{N-1} (\nu_{i+1} - \nu_i) A^\pi(S_i, k)$.
• Lemma 5.19(ii): if $\psi_i \ge M$ then $A(S_i, k) = 0$.
• Lemma 5.19(i): if $M - 1 \ge \psi_i$ then $A(S_i, k) \ge \frac{M - \psi_i}{1 - a} E\big[a^{T_k^{S_i}/(M - \psi_i)}\big]$.
• Eq. (5.27): $R^{\mathrm{opt}}(k) - R^\pi(k) \le \sum_{i=1}^{N-1} (\nu_{i+1} - \nu_i)\big[A^\pi(S_i, k) - A(S_i, k)\big]$.

The goal keeps the book's constants. Eq. (5.27) is a companion bound from the same identity.

Significance

The bound is explicit and computable from single-arm quantities: the AG indices and the laws of first-entry times. Subtracting from it the exact return of a concrete policy gives a certified suboptimality gap without solving the parallel-machine dynamic program, which has no index solution. The book uses it in exactly this way. With the exact return (5.30)–(5.31) of the heuristic $\pi_G^*$, it shows that $\pi_G^*$ loses $O(1-a)$, and in the limit $a \to 1$ that $\pi_G^*$ is average-overtaking optimal (Theorem 5.25).

All of these results are proved in the book and in Glazebrook and Wilkinson (2000). None is machine-checked. The series so far covers only the single-machine theory, and there is no parallel-machine bandit model on Prove2Me. This mission supplies that model and states the first link of the chain: from conservation-law algebra to a bound for a system that does not satisfy the conservation laws.

Difficulty

The identity (5.25) is algebra once the policy processes exactly $M$ arms in every period. The difficulty is the lower bound on $A(S_i, k)$. The obvious idea, which works for one machine, is to minimize $A^\pi(S_i, k)$ by giving priority to job types outside $S_i$. On $M$ machines such a policy cannot keep every machine busy outside $S_i$, and the minimizing policy is not known, so $A(S_i, k)$ has no closed form and must be bounded below over all history-dependent policies at once. The bound has to hold uniformly: it must account for each arm's processing both before and after its first visit to $S_i$, with arms frozen for random lengths of time in between. The printed proof also contains a step whose last inequality goes the wrong way (finding F2). The lemma is true, but the printed chain of inequalities cannot be followed literally.

Formalization scope

Job types are Fin (N + 1), so the book's $N$ is Lean's N + 1 and the book's type $i$ is the Lean index i - 1. Sums over $i = 1, \dots, N - 1$ run over i : Fin N, with $\nu_{i+1}$ = ν i.succ, $\nu_i$ = ν i.castSucc and $S_i$ = Finset.Iic i.castSucc. The arms are Fin n, and arm : Fin (N + 1) → Fin n assigns job types to arms. One kernel on the disjoint union replaces the book's per-arm matrices $P^b$, and IsArmFamily states closedness and irreducibility. A policy (ParallelPolicy n N M) is a sequence of Markov kernels from histories to Boolean selection vectors with exactly $M$ true entries. The law of the history is built by composition, and the performance is a discounted sum of expected per-period occupation counts. $R^{\mathrm{opt}}$ and $A(S, k)$ are a real supremum and infimum over all policies. The class is nonempty because $1 \le M \le n$, and both families are bounded, so neither takes a junk value. $E[a^{T/m}]$ is an integral against the product of the single-arm chain laws, with a real exponent and $a^\infty = 0$. The numbering by AG indices is two hypotheses: the identity permutation is an output of $\mathrm{AG}(A, r)$, and $\nu$ is monotone. The arm numbering is a function lowest with lowest b $= i_b$ and lowest monotone.

Unit conversions: none. Section 5.7 is written in discrete time with discount factor $a$, the convention of the series' published definitions, so every constant is the book's.

Correction of the setup: the book assumes "the number of parallel servers $M$ exceeds the number of arms $n$" (p. 139). The rest of the section needs the opposite (finding F1): for instance, the arm index $n - M + 1$ in Corollary 5.20 is not positive when $M > n$. Every item assumes $1 \le M \le n$.

Trivializing formalizations ruled out: $A(S_i, k)$ is not a hypothesis or an abstract GCL quantity. It is the infimum over an explicitly constructed, nonempty class of parallel-machine policies, so the goal cannot be discharged by assuming the conservation laws for the $M$-machine system (which fail). The theorems do not allow $M > n$, where the policy class is empty and the supremum would take the junk value $0$.

Out of scope: the branching-bandit bounds of §5.5 (Theorems 5.12 and 5.13). They need a continuous-time branching-bandit model whose GCL property the book only cites. Also out of scope are Theorem 5.11 (priority classes) and the $O(\cdot)$ results 5.21–5.23 and Theorem 5.25.

Reusable infrastructure: the parallel-machine SFABP model (Def_AllocationIndices_Branching_Parallel) serves the remaining results of §5.7. Lemmas on the law of a frozen arm's trajectory under an arbitrary policy are welcome contributions.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, §5.3 and §5.7. https://doi.org/10.1002/9780470980033
• K. D. Glazebrook, D. J. Wilkinson, Index-based policies for discounted multi-armed bandits on parallel machines, Annals of Applied Probability 10 (2000), 877–896. https://doi.org/10.1214/aoap/1019487512
• 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 (1996), 257–306. https://doi.org/10.1287/moor.21.2.257

Motivation

The multi-armed bandit problem asks how to share effort sequentially among several independent projects, each of which evolves only while it is worked on. It models the scheduling of jobs on a single machine, the order in which to explore candidate sites, sequential clinical trials and the allocation of research effort among competing projects. Before 1972 the problem had no general solution: dynamic programming over the joint state of all projects is intractable as soon as there are more than a few of them.

J. C. Gittins and D. M. Jones (1974) announced, and Gittins (1979) set out in full, a solution of a striking form: each project can be assigned a number depending only on its own current state, its dynamic allocation index (DAI, now the Gittins index), and it is optimal to work on a project whose index is largest.

Timeline. Gittins and Jones presented the index result at the European Meeting of Statisticians in 1972 (proceedings 1974). Gittins (1979) gave the general discrete-time formulation, stated the Forwards Induction Theorem and the DAI Theorem without proof, and proved the attainment Lemma of its Section 4. Whittle (1980) gave a dynamic-programming proof through the retirement formulation, Weber (1992) the prevailing-charge interchange argument, and Tsitsiklis (1994) a short inductive proof. Gittins, Glazebrook and Weber (2011) is the standard monograph; Lattimore and Szepesvári (2020, Chapter 35) give a measure-theoretic treatment on general state spaces.

Setting

A bandit process $D$ is a Markov chain $x(0), x(1), \dots$ on a measurable state space $\Theta$ with transition kernel $P$. Applying the continuation control at process time $t$ earns the discounted reward $a^t R(x(t))$, with $0<a<1$, and moves the chain one step; the freezing control leaves the state unchanged and earns nothing. For a stopping time $\tau$ of the chain (possibly infinite) write

$$R_\tau(D,x)=E\Big\{\sum_{t=0}^{\tau-1}a^tR(x(t))\,\Big|\,x(0)=x\Big\},\qquad W_\tau(D,x)=E\Big\{\sum_{t=0}^{\tau-1}a^t\,\Big|\,x(0)=x\Big\}.$$

The dynamic allocation index of $D$ in state $x$ is the largest reward per unit of discounted time obtainable by continuing for at least one step:

$$\nu(D,x)=\sup_{\tau>0}\nu_\tau(D,x),\qquad \nu_\tau(D,x)=\frac{R_\tau(D,x)}{W_\tau(D,x)}. \tag{2}$$

A simple family of alternative bandit processes consists of $k$ bandit processes. At each stage $n=0,1,2,\dots$ a policy chooses exactly one of them to continue, possibly at random and as a function of the whole past; the others are frozen. A policy is optimal if it attains the supremum of the total expected discounted reward over all policies.

The Lean development uses the published objects markovChainMeasure P x (the chain law), IsPositiveStoppingTime, stoppedRatio P r α τ x ($\nu_\tau$), gittinsIndex P r α x ($\nu$), MarkovBanditPolicy k S, markovBanditMeasure P π x n (the law of the first $n$ stages) and markovBanditDiscountedValue P r α π x (the total expected discounted reward), with $a$ written α and $R$ written r.

Formalization targets

Goal: the DAI Theorem (Section 3, p. 154)

For every policy $\pi$ and initial state vector $x$,

$$V_\pi(x)=\sup_{\pi'}V_{\pi'}(x)\iff \forall n,\ \text{a.s. under the play of }\pi\text{ from }x:\ \ \pi_n\Big(\big\{i:\nu(x_i(n))=\max_j\nu(x_j(n))\big\}\Big)=1 .$$

Milestones

1. Section 4, Lemma (p. 154). For $\Theta_0=\{y:\nu(D,y)<\nu(D,x)\}$ and $\tau$ the first $t\ge1$ with $x(t)\in\Theta_0$,

$$\nu_\tau(D,x)=\nu(D,x).$$

2. The "if" half of the DAI Theorem. A policy that selects a process of maximal index on every history is optimal: the published BanditAlgorithm.gittins_index_theorem, already Proved.
3. Section 4, Corollary 1 (p. 155). For the $M$-horizon index $\nu^M(D,x)=\sup_{0<\tau\le M}\nu_\tau(D,x)$ (5), the rule that stops at the first $t\in\{1,\dots,M-1\}$ with $\nu^{M-t}(D,x(t))<\nu^M(D,x)$, and at $M$ otherwise, attains $\nu^M(D,x)$.

Significance

The result. The DAI Theorem replaces a dynamic program on the product of $k$ state spaces by $k$ one-dimensional optimal stopping problems. The "only if" half says more than that the index rule is one optimal policy: it characterizes every optimal policy, so any rule that departs from the index on a set of positive probability loses reward. The Lemma identifies the stopping rule that attains the index, which is how indices are computed in practice, and Corollary 1 is the finite-horizon version on which the paper's numerical algorithm (Section 7) rests.

Formalizing it. The sufficiency half is formalized: BanditAlgorithm.gittins_index_theorem (Lattimore–Szepesvári Theorem 35.9) is Proved on the platform, together with gittins_index_policy_dominates, gittins_stopping_ratio_le_index and gittins_epsilon_optimal_stopping. The attainment Lemma is Proved only for countable state spaces with bounded rewards (AllocationIndices.optimal_stopping_set, Gittins–Glazebrook–Weber Lemma 2.2), and the necessity half is on no platform item. This mission asks for the Lemma on general standard Borel state spaces with integrable rewards, the finite-horizon Corollary 1, and the full equivalence. The Forwards Induction Theorem of p. 153, which needs superprocesses and forwards induction policies, is outside its scope.

Difficulty

The "only if" direction is the new content, and it does not follow from the sufficiency theorem: knowing that one index policy is optimal says nothing about a policy that sometimes plays a lower-index process. The deviation must be shown to cost a strictly positive amount whenever it happens with positive probability, which requires a strict comparison that survives discounting, ties in the index and infinite stopping times. A second obstacle is measure-theoretic. On a general state space the index is a supremum over uncountably many stopping times, its measurability is not available, and the Lemma's stopping rule is a stopping time only if $\{y:\nu(D,y)<\nu(D,x)\}$ is measurable; the arguments of the countable case, which treat each state separately, do not transfer.

Formalization scope

All objects are the published discounted $k$-armed Markov bandit of Def_GittinsIndex and the stopping-time quantities of Def_AllocationIndices_Index; time is indexed from $0$, stopping times are $\mathbb N\cup\{\infty\}$-valued and adapted to the coordinate filtration, and the index is the real supremum over stopping times $\tau\ge1$. The explicit readings committed to are:

• "Optimal" means attaining $\sup_{\pi'}V_{\pi'}(x)$ from the given initial state vector, over all randomized history-dependent policies; this supremum is finite because the values are bounded uniformly in the policy under the integrability hypothesis.
• "At each stage … almost always" means: for every stage $n$, almost surely under the law of the first $n$ stages of $\pi$ from $x$, the selection kernel puts mass one on the processes of maximal current index. Requiring the index rule on every history would make "only if" false.
• "The supremum of the total expected reward is finite" (p. 151) is read as $E_x\sum_t a^t|R(x(t))|<\infty$ for every state $x$.
• "$\nu(D,\cdot)$ is an $\mathcal X$-measurable function" (p. 151) is an explicit hypothesis of the Lemma and of the goal; the measurability of every $\nu^m(D,\cdot)$ is a hypothesis of Corollary 1.
• "The supremum is attained by setting $\Theta_0$" means that the first hitting time of $\Theta_0$ from time $1$ on is a positive stopping time whose ratio equals the index.
• The state space is standard Borel (the paper asks only for measurable singletons), and all processes share one kernel and one reward function; a family of different processes is encoded on the disjoint union of their state spaces.

A trivializing formalization is ruled out: the goal is not stated for index policies on every history (which would only restate the referenced theorem), the index is the published supremum over stopping times rather than a one-step reward or a finite-horizon quantity, competitors are not restricted to Markov or deterministic policies, and the Lemma's stopping rule starts at time $1$, so it never stops at once. A one-point state space satisfies all hypotheses together and admits a policy.

Useful infrastructure, reusable beyond this mission: measurability of the Gittins index on standard Borel spaces, a measurable selection of a maximal-index arm, and an interchange argument for $k$-armed Markov bandits on general state spaces. Proofs of any milestone, and of either half of the goal, are welcome.

Selected references

• J. C. Gittins, Bandit Processes and Dynamic Allocation Indices, J. R. Statist. Soc. B 41(2), 148–177, 1979. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
• J. C. Gittins and D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani et al., eds.), North-Holland, 241–266, 1974.
• P. Whittle, Multi-armed bandits and the Gittins index, J. R. Statist. Soc. B 42(2), 143–149, 1980. https://doi.org/10.1111/j.2517-6161.1980.tb01111.x
• R. Weber, On the Gittins index for multiarmed bandits, Ann. Appl. Probab. 2(4), 1024–1033, 1992. https://doi.org/10.1214/aoap/1177005588
• J. N. Tsitsiklis, A short proof of the Gittins index theorem, Ann. Appl. Probab. 4(1), 194–199, 1994. https://doi.org/10.1214/aoap/1177005207
• J. C. Gittins, K. D. Glazebrook and R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9780470980033
• T. Lattimore and C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. https://doi.org/10.1017/9781108571401

Motivation

The periodic-review inventory problem asks how much stock to order in each of $T$ periods when demand is random, unmet demand is backlogged, and both leftover stock and shortages are charged. When the demand distributions are known, a backward dynamic program computes an optimal policy, and the optimal policy is a base-stock policy: in each period, order up to a fixed target level (Zipkin, Foundations of Inventory Management, 2000). In practice the distributions are rarely known; what is available is data, or a simulator that produces demand scenarios.

Levi, Roundy and Shmoys (Math. Oper. Res. 32(4), 2007) asked how many sampled demand scenarios suffice to compute a policy whose expected cost is provably within a factor $1+\varepsilon$ of optimal, with a sample size that depends on $\varepsilon$, the confidence $\delta$, the horizon and the cost parameters, but not on the demand distributions. For the single-period newsvendor problem they proved such a bound for sample average approximation (their Theorem 2.2). For the multiperiod model they designed a new algorithm and proved the bound that this mission targets (Theorem 3.5 of §3.3).

Setting

Periods are indexed $t = 0, \dots, T-1$ (the paper counts from $1$). The demand $D_t$ of period $t$ is a real random variable with law $\mu_t$ and finite mean, possibly negative. Demands of different periods are independent but need not be identically distributed. Orders arrive immediately, there is no ordering cost, and unmet demand is backlogged. Raising the inventory to $y$ in period $t$ costs, at the end of the period, $h(y - D_t)^+ + b(D_t - y)^+$ with $h, b > 0$.

• The newsvendor cost is $C_t(y) = \mathbb E[h(y-D_t)^+ + b(D_t-y)^+]$.
• The optimal dynamic program (eqs. (1)–(2)) is $U_t(y) = C_t(y) + \mathbb E[V_{t+1}(y - D_t)]$ and $V_t(x) = \min_{y \ge x} U_t(y)$, with $V_T \equiv 0$. The optimal expected cost is $\mathrm{OPT} = \min_y U_0(y)$.
• For levels $L = (L_t)$, the base-stock policy raises the inventory $x$ to $\max(x, L_t)$ in period $t$. The shadow cost $\tilde U_t(y)$ is the expected cost over periods $t, \dots, T-1$ of ordering up to $y$ in period $t$ and then following $L_{t+1}, \dots, L_{T-1}$.
• $L_s, \dots, L_{T-1}$ is an upper base-stock policy (Definition 3.2) if for each $j \ge s$ the shadow cost $\tilde U_j$ is convex with smallest minimizer $\bar R_j$, and $L_j \ge \bar R_j$.
• A point $y$ is an $\alpha$-point of $f$ (Definition 3.3) if $f$ has a subgradient $r$ at $y$ with $|r| \le \alpha$.
• The sample right-derivative estimator $\hat U^r_t(y)$ averages, over $N$ sampled demand paths, an explicit bounded path variable whose mean is the right derivative of $\tilde U_t$ (Lemma 3.4, Corollary 3.1).

The algorithm (§3.3, p. 835). Given $0 < \varepsilon \le 1$ and $0 < \delta < 1$, put $\varepsilon_t = \varepsilon/2T$, $\delta_t = \delta/T$ and $\alpha_t = (\varepsilon_t/3)\min(b, h)$. The paper states:

In stage $t = T, \dots, 1$, consider the function $\tilde U_t$ defined above with respect to the previously computed base-stock levels $\tilde R_{t+1}, \dots, \tilde R_T$ (where $\tilde U_T = C_T$). Use the black box to generate $N_t = 2((b + h)(T - t + 1))^2(1/\alpha_t^2)\log(2/\delta_t)$ independent samples of the demands $D_t, \dots, D_T$ and compute $\tilde R_t = \inf\{y : \hat U^r_t(y) \ge \alpha_t/2\}$. Note that in each stage, the algorithm is using an additional $N_t$ samples that are independent of the samples used in previous stages.

Formalization targets

Goal: Theorem 3.5 (§3.3)

For $T \ge 1$, $h, b > 0$, independent demand laws with finite mean, $0 < \varepsilon \le 1$ and $0 < \delta < 1$, the levels $\tilde R_0, \dots, \tilde R_{T-1}$ computed by the algorithm satisfy

$$\Pr\Big[\ \tilde U_0(\tilde R_0) \le (1+\varepsilon)\,\min_y U_0(y)\ \Big] \;\ge\; 1-\delta .$$

Here $\tilde U_0(\tilde R_0)$ is the expected cost of the computed policy and $\min_y U_0(y)$ is the optimal expected cost. The constants are those of the paper; the goal fixes the algorithm, not a class of algorithms.

Milestones (proof order)

1. Fact 3.1: $w(x) = \min_{y\ge x} f(y)$ is convex for convex $f$ with a minimizer $r$, and $w(x) = f(\max(x, r))$.
2. Lemma 3.1: following an upper base-stock policy keeps $\tilde U_j$ and $\tilde V_j$ convex, so $\bar R_j$ exists.
3. Lemma 3.2: if each tail policy is $\beta_j$-optimal, ordering up to $\bar R_t$ is $\max_j \beta_j$-optimal.
4. Claim after Lemma 3.2 (p. 832): per-stage factors $(1+\varepsilon_t)$ multiply to $\prod_j(1+\varepsilon_j)$.
5. Lemma 3.3: an $\alpha$-point of a convex $f \ge h(y-d)^+ + b(d-y)^+$, with $\alpha = (\varepsilon/3)\min(b,h)$, is $(1+\varepsilon)$-optimal.
6. Lemma 3.4: the path variable $\tilde M^r_{tj}(y)$ has the mean of $\mathbb 1(\tilde A_{jt}(y))C^r_j(y - D_{[t,j)})$.
7. Corollary 3.1: the right derivative of $\tilde U_t$ is the mean of the path value.
8. Lemma 3.5: one stage with $N_t$ samples produces an $\alpha_t$-point $\tilde R_t \ge \bar R_t$ with probability at least $1 - \delta_t$.

Hoeffding's inequality (Theorem 3.4) enters through Lemma 3.5; Concentration.hoeffding_two_sided is included as a reference item.

Significance

The theorem gives sample sizes $N_t$ that grow polynomially in $T$, $1/\varepsilon$, $\log(1/\delta)$ and $(b+h)/\min(b,h)$, and are uniform over all demand distributions with finite mean. The analysis shows that a sampled dynamic program need not lose control of convexity: the upper base-stock invariant keeps every stage a convex problem, and relative errors made in later stages multiply rather than compound through the recursion.

The result has been proved on paper since 2007. As far as a search of the platform shows (October 2026), none of its lemmas has a machine-checked proof; the platform has single-period newsvendor material from other papers, and a two-sided Hoeffding inequality. A formalization would supply a finite-horizon stochastic inventory dynamic program and its shadow version as reusable objects, a one-dimensional bridge from approximate first-order optimality to relative error (Lemma 3.3), and an end-to-end checked sample-complexity bound for a multistage stochastic model.

Difficulty

The naive argument estimates each stage's minimizer by sampling and adds up the per-stage errors. It fails twice. First, once a later stage uses an approximate level, the earlier stage's cost-to-go is no longer that of an optimal policy and need not be convex, so "the minimizer" may not exist and its sampled estimate has no guarantee. Second, an additive error in a later stage's cost can be amplified by the earlier stages. The paper's invariant, which requires each computed level to lie above the true shadow minimizer, controls both, and the formalization has to establish this invariant from samples with high probability. Measure-theoretically, the costs are nested expectations of infima, a one-sided derivative must pass through an expectation over a demand path, and stage-wise events must be combined although earlier levels are random.

Formalization scope

• Conventions. Periods are $0$-based natural numbers, so the paper's factor $T - t + 1$ is $T - t$, and the paper's $\tilde R_1$ is $\tilde R_0$. Laws $\mu_t$ and costs are given for every $t \in \mathbb N$; only $t < T$ matter. Demands are real valued. Expectations are Bochner integrals, and every theorem that evaluates a cost function assumes $\mathbb E|D_t| < \infty$, the paper's standing assumption. $\min_{y \ge x}$ and $\min_y$ are real infima of nonnegative functions. "$\bar R_j$ exists" means "$\tilde U_j$ is convex and has a smallest minimizer". The paper's real $N_t$ is rounded up with $\lceil\cdot\rceil$; Lemma 3.5 only needs $N_t$ to be at least the bound. The right derivative is HasDerivWithinAt on $[y, \infty)$. Probabilities of events are measures of sets, which are outer measures on non-measurable sets.
• Sample space. For each stage $t < T$, $N_t$ demand paths in $\mathbb R^T$; all paths are independent with law $\mu_0 \otimes \dots \otimes \mu_{T-1}$. A stage-$t$ path also has coordinates for periods before $t$, which are never read. $\tilde R_t$ is a deterministic function of the outcome, defined by backward recursion from the paper's infimum rule.
• No trivialization. The optimum is defined from the true dynamic program (1)–(2) and does not depend on the algorithm. The algorithm is fixed, with the paper's $N_t$, $\alpha_t$ and $\delta_t$. Samples are independent across stages. The demand laws are arbitrary probability measures on $\mathbb R$ with finite mean, not restricted to bounded, continuous or nonnegative demand.
• Infrastructure needed. Convexity of parametric infima, interchange of one-sided derivatives with expectations, conditioning on products of independent coordinates, and Hoeffding's inequality (one-sided, in Mathlib in sub-Gaussian form). The model, shadow program and estimator definitions are reusable for other inventory and sampled dynamic-programming results. Proofs of any milestone, including partial results such as the single-stage case $T = 1$, are welcome.

Selected references

• R. Levi, R. O. Roundy, D. B. Shmoys, Provably Near-Optimal Sampling-Based Policies for Stochastic Inventory Control Models, Mathematics of Operations Research 32(4):821–839, 2007. https://doi.org/10.1287/moor.1070.0272
• P. H. Zipkin, Foundations of Inventory Management, McGraw-Hill, 2000.
• W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58(301):13–30, 1963. https://doi.org/10.1080/01621459.1963.10500830

Motivation

A Markov decision process (MDP) with the average cost per unit time criterion models a controller who runs a stochastic system indefinitely and cares about long-run cost rather than any finite horizon: inventory control, queueing control, and maintenance are standard examples. The basic questions are whether an optimal policy exists, whether it can be taken stationary (a fixed measurable rule $\phi(x)$), and whether it is characterized by an average cost optimality inequality (ACOI).

For uncountable state spaces the classical answer is Schäl's (Math. Oper. Res. 18, 1993), under weak continuity of the transition probabilities, compact action sets, and a uniform bound on the relative discounted values. Hernández-Lerma replaced compactness by inf-compactness of the cost in the action, but under setwise continuity; Feinberg and Lewis (Math. Oper. Res. 32, 2007) allowed noncompact actions under weak continuity, at the price of inf-compactness of the cost in state and action jointly plus a local boundedness condition. That joint inf-compactness excludes bounded costs on unbounded state spaces, the setting of Ross and of Dynkin and Yushkevich. Feinberg, Kasyanov and Zadoianchuk (Math. Oper. Res. 37(4), 2012) remove both restrictions.

Setting

The state space $\mathbb X$ and action space $\mathbb A$ are Borel subsets of Polish spaces. Each state $x$ has a nonempty Borel set $A(x)\subseteq\mathbb A$ of available actions; the graph $\mathrm{Gr}(A)=\{(x,a):a\in A(x)\}$ is Borel and has a measurable selector. Choosing $a$ at $x$ costs $c(x,a)\in(-\infty,+\infty]$ (bounded below, measurable) and moves the system according to a transition probability $q(\cdot\mid x,a)$. A policy $\pi$ is a sequence of randomized, history-dependent decision rules concentrated on $A(x_n)$; the set of stationary policies $\mathbb F$ consists of Borel maps $\phi$ with $\phi(x)\in A(x)$.

For $\alpha\in[0,1)$ the discounted cost is $v^\pi_\alpha(x)=\mathbb E^\pi_x\sum_{n\ge0}\alpha^n c(x_n,a_n)$ and the average cost is $w^\pi(x)=\limsup_{N\to\infty}\frac1N\mathbb E^\pi_x\sum_{n<N}c(x_n,a_n)$. Optimal values are infima over all policies: $v_\alpha(x)$, $w(x)$, and $w^*=\inf_x w(x)$. Put $m_\alpha=\inf_x v_\alpha(x)$, the relative discounted value $u_\alpha=v_\alpha-m_\alpha$, and $\bar w=\limsup_{\alpha\uparrow1}(1-\alpha)m_\alpha$.

The assumptions are:

• (W*): (i) $c$ is lower semicontinuous on $\mathrm{Gr}(A)$; (ii) if $x_n\to x$ in $\mathbb X$, $a_n\in A(x_n)$ and $c(x_n,a_n)$ is bounded above, then $(a_n)$ has a limit point in $A(x)$; (iii) $q(\cdot\mid x,a)$ is weakly continuous in $(x,a)\in\mathrm{Gr}(A)$.
• (B̲): $w^*<\infty$, and $\liminf_{\alpha\uparrow1}u_\alpha(x)<\infty$ for every $x$.
• (Wu): $c$ is inf-compact on $\mathrm{Gr}(A)$, and (W*)(iii) holds.

The candidate relative value function is the joint lower limit

$$u(x)=\liminf_{\alpha\uparrow1,\;y\to x}u_\alpha(y),$$

and the candidate optimal actions are $A^*(x)=\{a\in A(x):\ \bar w+u(x)\ge c(x,a)+\int_{\mathbb X}u(y)\,q(dy\mid x,a)\}$.

Formalization targets

Goal: Theorem 3

Under (W*) and (B̲) there is $\phi\in\mathbb F$ with

$$\bar w+u(x)\ \ge\ c(x,\phi(x))+\int_{\mathbb X}u(y)\,q(dy\mid x,\phi(x)),\qquad x\in\mathbb X,$$

and for it $w(x)=w^\phi(x)=\limsup_{\alpha\uparrow1}(1-\alpha)v_\alpha(x)=\bar w=w^*$ for all $x$. Moreover (a) $u$ is finite and lower semicontinuous; (b) each $A^*(x)$ is nonempty and compact and $\mathrm{Gr}(A^*)$ is Borel; (c) every $\phi\in\mathbb F$ selecting from $A^*$ is average cost optimal and satisfies the inequality; (d) some $\phi\in\mathbb F$ selects from the minimizer sets $A_*(x)\subseteq A^*(x)$ of $a\mapsto c(x,a)+\int u\,dq$; (e) under (Wu), $u$ is inf-compact.

Milestones

In the paper's order: Theorem 1 (the inequality with $\bar w$ implies optimality), Lemma 2 (inf-compactness in the action), Lemma 3 (lower semicontinuity of the minimal value and a Borel minimizer), Lemma 4 (a Fatou lemma for weakly converging measures, already on the platform as Schäl's Lemma 2.3(ii)), Theorem 2 (i), (iv)–(vi) (the discounted problem under (W*)), Lemma 6 (semicontinuity of $u$, $u_\alpha$ and the auxiliary $\underline u_\alpha$), Corollary 1, and Lemma 7, the ACOI itself. Schäl's inequality $\underline w\le\bar w\le w^*<\infty$ is referenced as an existing platform item.

Significance

Theorem 3 gives stationary average-cost optimal policies for weakly continuous MDPs with noncompact action sets and costs that need not be inf-compact in the state, which covers bounded costs on unbounded state spaces and inventory models whose holding costs do not grow without bound. Assumption (B̲) asks only for a finite lower limit of $u_\alpha(x)$ as $\alpha\uparrow1$, weaker than Schäl's uniform bound. The approach was extended to partially observable MDPs and to later work on the average cost optimality equation, which builds on exactly these objects.

The theorem is proved in the literature; nothing here is open mathematically. What the mission adds is a machine-checked proof of the full chain from measurable selection and semicontinuity through the vanishing-discount limit, for Borel spaces and history-dependent randomized policies. Reading the proofs closely has turned up three printed statements that are false as written (see Beyond the paper); a formal development settles exactly which hypotheses each step needs.

Difficulty

The obvious route takes a limit of discount-optimal policies $\phi_{\alpha_n}$ as $\alpha_n\uparrow1$. With noncompact $A(x)$ such a sequence need not have any limit point; (W*)(ii) supplies one only when the costs along it stay bounded, and that has to be extracted from the relative values. The second obstacle is that $u_\alpha$ is controlled only through its lower limit at each point, so $u$ is a joint lower limit in $(\alpha,y)$ and passing it under $\int\cdot\,dq$ requires a Fatou-type lemma for weakly converging measures rather than dominated convergence. Finally, selecting a Borel $\phi$ from the sets $A^*(x)$ requires a uniformization theorem for Borel sets with $\sigma$-compact sections (Arsenin–Kunugui), which Mathlib does not have.

Formalization scope

The spaces are types with a separable metrizable topology whose Borel $\sigma$-algebra is standard Borel (by Lusin–Souslin, exactly the Borel subsets of Polish spaces up to homeomorphism). The model reuses the published definitions FeinbergLiang_ACOE_MDP (policies, path measures via Ionescu–Tulcea, discounted and average costs) and SchalAvg_AvgOpt_Model (action sets, admissible policies, $v_\alpha$, $m_\alpha$, $u_\alpha$, $\bar w$, $w^*$, Assumption (G)). Conventions:

• the cost takes values in $[0,+\infty]$; the paper's bounded-below cost reduces to this by adding a constant, which changes none of the statements (p. 595);
• $q$ is a Markov kernel on all of $\mathbb X\times\mathbb A$; only its values on $\mathrm{Gr}(A)$ enter;
• functions such as $u$ are $[0,+\infty]$-valued, and the paper's "$u:\mathbb X\to\mathbb R_+$" is stated as $u(x)\neq+\infty$ for every $x$;
• $\alpha\uparrow1$ is the left neighbourhood filter of $1$; $u$ is the lower limit along $\mathcal N_{<}(1)\times\mathcal N(x)$, with $y=x$ allowed;
• "min" is stated as an attained infimum;
• the existence of a measurable selector of $A$ is the hypothesis HasSelector.

Optimal values are infima over all admissible (randomized, history-dependent) policies, not over stationary ones. $u$ is the fixed function (21), never a free parameter. All four equalities of (10) are stated for every $x$. (W*), (Wu) and (B̲) constrain $c$ and $q$ on $\mathrm{Gr}(A)$ only. A statement that ranged over a smaller policy class, left $u$ free, kept a single equality, or imposed continuity on all of $\mathbb X\times\mathbb A$ would be a different and easier theorem.

A complete development needs: semicontinuity and inf-compactness calculus for $[0,\infty]$-valued functions; lower semicontinuity of $\mu\mapsto\int f\,d\mu$ under weak convergence for lower semicontinuous $f$; the Arsenin–Kunugui uniformization theorem; discounted dynamic programming on Borel spaces; and an Abelian/Tauberian comparison of $\limsup(1-\alpha)v_\alpha$ with Cesàro averages. The first three are reusable well beyond MDPs. Contributions to any milestone, or to these libraries, are welcome.

Beyond the paper. Three corrected variants are posed beside the faithful statements, which stay as printed. Lemma 2, corrected: as printed it assumes only (W*)(ii) (and (iii)), but without lower semicontinuity of $c$ a level set such as $(0,1]$ need not be compact; the variant adds (W*)(i). Lemma 3, corrected: $u^*\in L(\mathbb X)$ can fail because $u^*$ may be identically $+\infty$ for some $u\in L(\mathbb X)$; the variant asserts lower semicontinuity only. Corollary 1, corrected: the joint limit $\lim_{n\to\infty,\,y\to x}\underline u_{\alpha_n}(y)$ need not exist (a one-action example with an indicator cost); the variant uses the lower limit, which is what the proof computes and what Lemma 7 uses. A misprint in the proof of Lemma 3 (p. 598, $\mathrm{Gr}(A)$ for $\mathrm{Gr}(A_*)$) does not affect its statement.

Selected references

• E. A. Feinberg, P. O. Kasyanov, N. V. Zadoianchuk, Average cost Markov decision processes with weakly continuous transition probabilities, Mathematics of Operations Research 37(4):591–607, 2012. https://doi.org/10.1287/moor.1120.0555
• M. Schäl, Average optimality in dynamic programming with general state space, Mathematics of Operations Research 18(1):163–172, 1993. https://doi.org/10.1287/moor.18.1.163
• E. A. Feinberg, M. E. Lewis, Optimality inequalities for average cost Markov decision processes and the stochastic cash balance problem, Mathematics of Operations Research 32(4):769–783, 2007. https://doi.org/10.1287/moor.1070.0269
• O. Hernández-Lerma, J. B. Lasserre, Discrete-Time Markov Control Processes: Basic Optimality Criteria, Springer, 1996. https://doi.org/10.1007/978-1-4612-0729-0
• A. S. Kechris, Classical Descriptive Set Theory, Springer, 1995 (Arsenin–Kunugui theorem, p. 297). https://doi.org/10.1007/978-1-4612-4190-4