Dynamic Programming

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

Why accelerate value computation

Value iteration and its policy-evaluation special case, value computation, are the basic algorithms of dynamic programming for Markov decision processes (MDPs). Both are fixed-point iterations of a $\lambda$-contraction, so they converge at the geometric rate $\lambda$, the discount factor. When $\lambda$ is close to $1$, which is the regime of long effective horizons in reinforcement learning ($\lambda = 0.99$ or $0.999$) and in healthcare and operations applications, the number of iterations grows like $1/(1-\lambda)$.

Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) observe that $v \mapsto v - T(v)$ behaves like the gradient of a function with smoothness constant $1+\lambda$ and strong-convexity constant $1-\lambda$. This suggests importing the accelerated schemes of convex optimization: Nesterov's acceleration and Polyak's momentum (heavy-ball) method (Polyak 1964; Ghadimi, Feyzmahdavian, Johansson 2015). For the affine operator $T_\pi$ of a fixed policy, they prove that both schemes converge at a rate governed by $\sqrt{\kappa}$ rather than $\kappa$, with $\kappa = (1+\lambda)/(1-\lambda)$, provided the Markov chain of the policy is irreducible and reversible. This mission poses the momentum result, Theorem 5.5.

Setting

A finite MDP has a state set $S$ with $|S| = n$, a finite action set $A$, transition probabilities $P_{iaj}$ (from state $i$ to state $j$ under action $a$; each $P_{ia}$ is a probability vector), rewards $r_{ia} \in \mathbb{R}$, and a discount factor $\lambda \in (0,1)$. A policy $\pi = (\pi_{ia})$ is a matrix with nonnegative rows summing to $1$; it induces

$$r_{\pi,i} = \sum_a \pi_{ia} r_{ia}, \qquad L_{\pi,ij} = \sum_a \pi_{ia} P_{iaj}, \qquad T_\pi(v) = r_\pi + \lambda L_\pi v .$$

The value function of $\pi$ is $v^\pi = \sum_{t \ge 0} \lambda^t L_\pi^t r_\pi$, the expected discounted reward from each starting state; it is the unique fixed point of $T_\pi$.

Reversibility (Definition 2.1): the chain with transition matrix $L$ is irreducible, and it has a stationary probability distribution $\nu$ with $\nu_i L_{ij} = \nu_j L_{ji}$ for all $i,j$.

Momentum Value Computation (M-VC) starts from arbitrary $v_0, v_1 \in \mathbb{R}^n$ and iterates

$$v_{s+1} = v_s - \alpha\,(v_s - T_\pi(v_s)) + \beta\,(v_s - v_{s-1}), \qquad s \ge 1,$$

with the constant step sizes (4.2)

$$\alpha = \frac{2}{1+\sqrt{1-\lambda^2}}, \qquad \beta = \frac{1-\sqrt{1-\lambda^2}}{1+\sqrt{1-\lambda^2}} .$$

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

$$B_\pi = \begin{pmatrix} \lambda(\beta+1)L_\pi & -\beta I \\ I & 0 \end{pmatrix},$$

which propagates the error of the pair $x_s = (v_s, v_{s-1})$, and its spectral radius $\rho(B_\pi)$, the largest modulus of a complex eigenvalue.

Formalization targets

Goal: Theorem 5.5

For a valid MDP and a policy $\pi$ whose chain $L_\pi$ is irreducible and reversible, the M-VC iterates with step sizes (4.2) converge to $v^\pi$, and for every $\eta > 0$

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

The goal states the paper's three clauses as printed: convergence, the little-o rate for every $\eta > 0$, and the comparison with $\lambda$.

Milestones

1. The step-size identity $\alpha = 1 + \beta$ (proof of Lemma B.1).
2. Lemma B.1: $x_s = x^\pi + B_\pi^{s-1}(x_1 - x^\pi)$ for all $s \ge 1$, with $x^\pi = (v^\pi, v^\pi)$.
3. The eigenvalues of an irreducible, reversible transition matrix are real (§2).
4. (B.1): every eigenvalue $\omega$ of $B_\pi$ satisfies $\omega^2 - \frac{2\lambda\mu}{1+\sqrt{1-\lambda^2}}\omega + \frac{1-\sqrt{1-\lambda^2}}{1+\sqrt{1-\lambda^2}} = 0$ for an eigenvalue $\mu$ of $L_\pi$.
5. For $\mu \in [-1,1]$, the roots $\omega^\pm(\mu)$ of (B.1) have modulus $\lambda/(1+\sqrt{1-\lambda^2})$.
6. The identity $\frac{\lambda}{1+\sqrt{1-\lambda^2}} = \frac{\sqrt{1+\lambda}-\sqrt{1-\lambda}}{\sqrt{1+\lambda}+\sqrt{1-\lambda}} = \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}}$.
7. Lemma B.2: for a reversible chain, $\rho(B_\pi) = \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}}$.
8. $0 < \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}} < \lambda$ for $\lambda \in (0,1)$.

Significance

The rate $(1-\sqrt{1/\kappa})/(1+\sqrt{1/\kappa})$ is the optimal rate of the heavy-ball method on strongly convex quadratics with condition number $\kappa$. Theorem 5.5 shows that policy evaluation for reversible chains enjoys the same improvement over $\lambda$, so that an $\epsilon$-approximation of $v^\pi$ needs a number of iterations scaling like $1/\sqrt{1-\lambda}$ rather than $1/(1-\lambda)$. The paper also shows that the reversibility assumption cannot simply be dropped: on a cyclic chain both accelerated schemes may diverge. Lemma B.2 is an exact spectral computation for a structured block matrix that reappears in any heavy-ball analysis driven by a matrix with real spectrum in $[-1,1]$.

The paper is a sibling series of four missions. This one poses Theorem 5.5; the others pose Theorem 5.1 (Accelerated Value Computation), Theorem 6.3 (a lower bound for first-order methods on a chain MDP) and Theorem 7.1 (Safe Accelerated Value Iteration). The results are proved on paper; none of them has a machine-checked proof. The work here is to formalize the known argument: the linear-recursion representation, the spectrum of $B_\pi$, and the passage from spectral radius to a little-o rate.

Difficulty

The obvious argument bounds $\|B_\pi\|$ in some norm and iterates. No such bound by the rate holds in general: $B_\pi$ is not normal, and for eigenvalues $\mu = \pm 1$ of $L_\pi$ the two roots of (B.1) coincide, producing Jordan blocks. The rate must come from the spectral radius, and the gap between $\rho(B_\pi)$ and $\|B_\pi^s\|^{1/s}$ is exactly what the $+\eta$ absorbs. Computing $\rho(B_\pi)$ needs two separate facts: the eigenvalues of $B_\pi$ are tied to those of $L_\pi$ through the quadratic (B.1), which needs a determinant identity for block matrices with commuting blocks; and the eigenvalues of $L_\pi$ are real and lie in $[-1,1]$, which needs reversibility together with irreducibility, used to make the stationary distribution positive. For non-real $\mu$ the modulus computation fails, which is why the hypothesis cannot be dropped.

Formalization scope

States and actions are finite types. The MDP data $(P, r, \lambda)$ is a plain structure, with validity (stochastic $P_{ia}$, $0 < \lambda < 1$) a separate hypothesis; the paper's initial distribution $p_0$ plays no role and is omitted. The value function is the Neumann series $\sum_t \lambda^t L_\pi^t r_\pi$. The norm on $\mathbb{R}^n$ is the sup norm, and $o(\cdot)$ is with respect to it as $s \to \infty$. Spectra and spectral radii are those of the complexified matrices, so that the non-real eigenvalues of $B_\pi$ are seen. Reversibility uses the published mm_basic notions: irreducibility, a stationary probability distribution, and detailed balance with respect to it; detailed balance alone would be trivially satisfied by $\nu = 0$ and is not used.

Three printed slips are corrected, and each milestone keeps the printed text verbatim. Lemma B.1 is printed with $x_0 - x^\pi$, but $x_0 = (v_0, v_{-1})$ is undefined; the statement uses $x_1 = (v_1, v_0)$. Lemma B.2 prints $\rho(B_\pi) = (1-\sqrt\kappa)/(1+\sqrt\kappa)$, a negative number; its proof computes $(1-\sqrt{1/\kappa})/(1+\sqrt{1/\kappa})$, the rate of Theorem 5.5, which is stated. On p. 22 the constant $\lambda/(1+\sqrt{1-\lambda^2})$ is printed as $\lambda/(1+\sqrt{1-\lambda})^2$. The second step size, printed $\gamma$ in (4.2), is the $\beta$ of (M-VC) and App. B.

A statement that holds only vacuously, for example one in which reversibility is replaced by detailed balance with an arbitrary vector or in which $\lambda$ is unconstrained, is ruled out by the hypotheses above. Lemma B.2 is an equality and must not be weakened to an upper bound.

A complete development needs the determinant of a $2\times 2$ block matrix with commuting blocks, the reality of the spectrum of a reversible chain (implied by the published MarkovMixing.spectral_representation once the stationary distribution is shown positive), Gelfand's formula for matrices, and the convergence of the Neumann series. The spectral facts about reversible chains and the block-matrix spectrum are reusable beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• V. Goyal and J. Grand-Clément, A First-Order Approach to Accelerated Value Iteration, Operations Research, 2023; arXiv:1905.09963v7 (2021). https://arxiv.org/abs/1905.09963
• B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Computational Mathematics and Mathematical Physics 4(5), 1964. https://doi.org/10.1016/0041-5553(64)90137-5
• E. Ghadimi, H. R. Feyzmahdavian, M. Johansson, Global convergence of the Heavy-ball method for convex optimization, European Control Conference, 2015. https://arxiv.org/abs/1412.7457
• P. Brémaud, Markov Chains: Gibbs Fields, Monte Carlo Simulation, and Queues, Springer, 2nd ed. 2020 (cited in the paper as 2013), Chapter 6. https://doi.org/10.1007/978-3-030-45982-6
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 2014. https://doi.org/10.1002/9780470316887

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

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

A firm with one product may face several customer classes in each selling interval. When stock is scarce, it must decide which outstanding demands to satisfy and how much inventory to carry into later intervals. When new stock can be bought at several dates, the rationing choice also changes the value of future purchasing opportunities. Topkis studied these linked decisions in a nonstationary model with class-dependent shortage penalties and a finite number of ordering periods. His Theorem 4 identifies conditions under which a policy computed from each period's myopic cost is optimal in the full multiperiod problem Topkis 1968.

The result belongs to a line of work on critical-level policies: choose a stock target and order up to it if current stock is lower. Here the target can be computed one period at a time despite the possibility of future purchases and the separate question of how to ration stock among demand classes. The paper attributes a related myopic policy result to Veinott and explains that its own setting allows a more general rationing policy than the special zero-rationing-level case discussed there Topkis 1968, pp. 175–176. This mission formalizes Topkis's multiperiod statement, including its ordering and rationing conclusions.

Setting

There are $N$ ordering periods, numbered $1$ through $N$. Period $m$ has a unit purchase cost $c_m$. It contains $k_m$ selling intervals, numbered backward: interval $k_m$ is first and interval $1$ is last. Within an interval, a random nonnegative demand vector has one component for each of $n$ customer classes. The vectors in distinct intervals and periods are independent and each class has a finite mean. At the start of an interval the demand is observed. A decision then selects how much of each class's outstanding demand to leave unsatisfied. The remaining physical stock incurs a holding cost, and each unsatisfied unit incurs a class-specific penalty. Unsatisfied demand is either carried entirely to the next interval or lost entirely, according to the interval. Penalties are nonnegative and rise with class index, so class $n$ has the highest shortage penalty Topkis 1968, pp. 162–163, 174.

Let $w$ be net stock before ordering at the start of period $m$: physical stock minus outstanding backlogs. The order must clear the backlog, so the post-order stock $z$ satisfies $z\ge w^+=\max(w,0)$. After period $N$, a further unit can be purchased for $c_{N+1}\ge0$, while unused stock can be salvaged for revenue $v\le c_{N+1}$. The terminal cost is $C_{N+1}(w)=(c_{N+1}-v)w^+$. Working backward, $C_m(w)$ is the optimal continuation cost, including the period-$m$ ordering decision. The actual period cost $\widetilde g^m(z)$ includes the later continuation value $C_{m+1}$, and equation (19) reads

$$C_m(w)=\inf_{z\ge w^+}\widetilde g^m(z).$$

The single-period cost $g^m(z)$ uses the same demand, holding costs and rationing choices in period $m$, but replaces the later continuation value by the linear terminal charge $-c_{m+1}y$. A myopic level $\bar y_m$ is any minimum of $g^m$ on $[0,\infty)$; it is $+\infty$ if no such minimum exists. Thus the level need not be the smallest minimum when several stock levels tie Topkis 1968, pp. 174–175.

Formalization targets

Theorem 4: myopic ordering and rationing

Suppose $v=c_{N+1}$ and the selected myopic levels are nondecreasing from period $m$ onward:

$$\bar y_m\le\bar y_{m+1}\le\cdots\le\bar y_N.$$

Then $\bar y_m<+\infty$, and ordering to $w\vee\bar y_m$ minimizes $\widetilde g^m$ over all feasible post-order levels $z\ge w^+$. If $m<N$ and the stock at the start of period $m$ is at most $\bar y_{m+1}$, the optimal rationing policy during that period is the optimal policy for its single-period problem, calculated with terminal costs $v_1\equiv0$ and $v_2(y)=-c_{m+1}y$ Topkis 1968, Theorem 4.

The milestones are the paper's regularity claim for $C_m$ and $\widetilde g^m$, existence of an actual optimal order-up-to level, finiteness of $\bar y_N$, the shape of $C_m$ around an optimal level, and the comparison in equation (20). Together these specify the route from the general dynamic program to the myopic target.

Significance

Theorem 4 gives a checkable sufficient condition for replacing a multiperiod ordering computation with a sequence of single-period cost minimizations. It also identifies when the rationing decisions can be obtained from the same single-period model. The stock bound in its rationing clause matters: outside that range, future costs may alter which class demands should be filled now. The result therefore describes both the simplification and its operational domain Topkis 1968, pp. 175–176.

Topkis proved the theorem in 1968; the task here is to produce machine-checked definitions and proofs of that known result. The definitions of feasible rationing, backward value functions, myopic costs and order-up-to levels will also support comparisons with other finite-horizon inventory models. The §1 model is duplicated locally while the four missions for this paper are drafted in parallel, then intended for consolidation into a shared interface.

Difficulty

Convexity alone gives an order-up-to form for the actual cost $\widetilde g^m$, but it does not identify its minimizing level with a minimum of the simpler cost $g^m$. The continuation value $C_{m+1}$ depends on all later ordering and rationing decisions. When some unsatisfied demand is lost, the end-of-period net stock can depend on the within-period rationing choice as well. The core issue is therefore to control the difference between the actual and myopic objectives in the stock range relevant to period $m$ Topkis 1968, pp. 174–176. A statement restricted to a preselected rationing rule would miss the theorem's claim about optimality among all feasible decisions.

Formalization scope

Classes are indexed by Fin n; the largest index is the highest penalty class. Intervals and ordering periods use natural numbers with explicit bounds, and intervals retain the paper's backward numbering. Stock, penalties and costs are real. A period's demand vector has a probability law on real vectors supported on the nonnegative orthant, with every coordinate integrable. The §1 dynamic program uses real infima for feasible rationing choices and Bochner integrals for demand expectations. The multiperiod value $C_m$ uses the nonnegative post-order domain $z\ge w^+$ in (19). Its defining infimum is intended to be finite under the paper's assumptions; the regularity and attainment milestones expose the facts that rule out Lean's default value for an unbounded infimum. These functions are used only at $1\le m\le N+1$, with period costs at $1\le m\le N$.

The multiperiod standing assumptions require $n>0$, $N>0$, and at least one interval per period, matching the paper’s positive counts.

Holding costs and the appropriate terminal costs satisfy the convexity and continuity assumptions of §1. Within each period, backlog multipliers equal $0$ or $1$. The terminal procurement cost is nonnegative and salvage revenue does not exceed it. Assumption (D′) is encoded as an eventually positive lower bound on the extended-real right derivative of $c_mw+\sum_{i=m}^N\sum_t h_{t,i}(w)-vw$. The §1 terminal functions used in the period assumptions are the linear functions required by the single-period comparison; their regularity adds no independent restriction. Independence across intervals and periods is built into successive expectations. The goal separately assumes $v=c_{N+1}$ and monotonicity of the selected myopic levels only from $m$ through $N$.

The formal target compares the actual and single-period sets of optimal rationing decisions at every interval and at every nonnegative state with stock at most $\bar y_{m+1}$. The stock bound and the full feasible set prevent the claim from becoming a result about a handpicked policy. Contributions to the backward recursion, convexity and attainment facts, and the comparison of these two decision sets are all part of this mission.

Selected references

• Donald M. Topkis, Optimal Ordering and Rationing Policies in a Nonstationary Dynamic Inventory Model with n Demand Classes, Management Science 15(3), 160–176, 1968. DOI: 10.1287/mnsc.15.3.160.

Motivation

Controlled queues are the standard testing ground for Markov decision processes with infinitely many states: the state is a queue length, which is unbounded, and the holding cost grows with it. The classical theory of the average cost criterion (Ross, Applied Probability Models with Optimization Applications, 1970) produces an optimal stationary policy only when the relative discounted values are uniformly bounded, a condition that fails for almost every queue with unbounded holding costs. Linn I. Sennott's paper Average Cost Optimal Stationary Policies in Infinite State Markov Decision Processes with Unbounded Costs (Operations Research 37(4):626–633, 1989, doi:10.1287/opre.37.4.626) replaced that boundedness by one-sided conditions that are checked in practice by a monotonicity argument and a single test function. Her conditions became the standard tool for queueing control and are the basis of Chapter 7 of her book Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999).

Timeline:

• 1962–1970. Derman and Ross obtain average cost optimal stationary policies from the vanishing discount approach when the relative values $h_\alpha$ are bounded.
• 1986. Sennott treats the queue with variable service rates under bounded costs and gives a first discrete-time Tauberian argument (Operations Research 34, 1986a; 1986b).
• 1989. This paper: Assumptions 1–3, the Theorem, the Markov chain test of Propositions 4–5, and applications to a packet system and to the queue with variable service rates (Proposition 8).

Setting

A Markov decision chain has states $i=0,1,2,\dots$; in state $i$ a finite nonempty set $A_i$ of actions; a cost $0\le C(i,a)<\infty$; and transition probabilities $P_{ij}(a)$. A policy $\theta$ may depend on the whole history and may randomize; a stationary policy $f$ chooses $f(i)\in A_i$ in state $i$. For $0<\alpha<1$, $V_{\theta,\alpha}(i)$ is the expected total $\alpha$-discounted cost from $i$ and $V_\alpha(i)=\inf_\theta V_{\theta,\alpha}(i)$, possibly infinite. The average cost of $\theta$ is

$$g_\theta(i)=\limsup_{N\to\infty}\frac1N\,E_\theta\Big[\sum_{t=0}^{N-1}C(X_t,a_t)\,\Big|\,X_0=i\Big].$$

A stationary policy $f$ is average cost optimal if there is a finite constant $g$ with $g=g_f(i)\le g_\theta(i)$ for every policy $\theta$ and every state $i$.

The queue with variable service rates (Example 2). Time is slotted; $p_i$ is the probability of $i$ arrivals in a slot, independently across slots. The state is the number of customers at the beginning of a slot. When the queue is nonempty the server chooses one of finitely many decision variables $a$ and serves at rate $a\beta\in(0,1)$, so that the customer in service leaves during the slot with probability $a\beta$; there is no decision in state $0$. From state $i\ge1$ the next state is $i-1+k$ with probability $a\beta p_k+(1-a\beta)p_{k-1}$ ($p_{-1}=0$), and from $0$ it is $j$ with probability $p_j$. The cost structure: $B(a)>0$; $Q$ a polynomial of degree $n\ge0$, nonnegative and increasing on $i\ge0$; $C(0)=Q(0)$ and $C(i,a)=Q(i)+B(a)$ for $i\ge1$. The arrival moments are $\lambda^{(k)}=\sum_i i^kp_i$ and $\lambda=\lambda^{(1)}$.

Formalization targets

Goal: Proposition 8

If $\lambda^{(n+1)}<\infty$, then

$$\lambda<\max_a(a\beta)\ \Longrightarrow\ \text{there is an average cost optimal stationary policy},$$

and

$$\lambda<\min_a(a\beta)\ \Longrightarrow\ g+h(i)=\min_a\Big\{C(i,a)+\sum_jP_{ij}(a)h(j)\Big\},\quad i\ge0,$$

with $g$ the optimal average cost, $g=\lim_{\alpha\uparrow1}(1-\alpha)V_\alpha(i)$, and $h$ bounded below.

Milestones

1. Propositions 1–3 (p. 627): $V_\alpha$ solves the discount optimality equation, is its minimal nonnegative solution, and is the limit of value iteration (already proved on the platform, referenced).
2. The Lemma (p. 628): discount optimal stationary policies along $\alpha_n\to1$ have a stationary limit point.
3. Lemmas A1 and A2 (p. 632): the comparison between solutions of the optimality inequality and average costs, and $\limsup_{\alpha\uparrow1}(1-\alpha)V_\alpha(i)\le g_\theta(i)$.
4. The Theorem (p. 628): under Assumptions 1–3, any limit point $f$ from the Lemma is average cost optimal, with the optimality inequalities (5); under Assumption 3*, the optimality equation (6).
5. Propositions 4, 5 and the Corollary (pp. 629–630): the Markov chain criteria that yield Assumptions 1, 3 and 3* from one well-behaved stationary policy.
6. Two steps of the proof of Proposition 8 (p. 631): $V_\alpha(i)$ is increasing in $i$ (hence Assumption 2), and the drift of $r(i)=Ai^{n+1}$ is a polynomial of degree at most $n$ with leading coefficient $A(n+1)(\lambda-a\beta)$, display (14).

Significance

Proposition 8 states that a queue in which at least one service rate exceeds the mean arrival rate has an average cost optimal stationary policy for holding costs of any polynomial growth, as long as the matching moment of the arrival distribution is finite. Bounded-cost results do not cover this case, which is the one used in practice. The general Theorem behind it is the standard vanishing discount theorem for countable-state models with unbounded costs; the Markov chain test of Propositions 4–5 and the Corollary reduces its hypotheses to a drift inequality for one policy.

All results of the paper are proved on paper. None is formalized: the platform has Sennott's discounted theory (Propositions 1–3, proved) and, as open statements, the book version of the Theorem (SennottDP.SEN.thm_7_2_3_sen_acoi), its existence part in a compact-action model (ArapostathisAC.SennottACOI.theorem_5_9), and the first half of Lemma A1 (SennottDP.SEN.lemma_7_2_1_acoi_bound). This mission states the paper's own version, with all conclusions of the Theorem, and its application to a concrete queue, which no platform item states.

Difficulty

The obvious route takes a limit of $h_\alpha=V_\alpha-V_\alpha(0)$ along a sequence $\alpha_n\to1$ and passes to the limit in the discount optimality equation. With unbounded costs and unbounded $h_\alpha$ the sum $\sum_jP_{ij}(a)h_\alpha(j)$ is an infinite series of terms that need not converge uniformly, so the limit of the sums is not the sum of the limits. Only an inequality survives (Fatou's lemma, which needs the lower bound of Assumption 2), and the equation needs the integrable upper bound of Assumption 3*. For the queue, the hypotheses are not visible from the model: they come from a monotonicity property of $V_\alpha$ and a Lyapunov drift computation whose leading term, $A(n+1)(\lambda-a\beta)i^n$, has to dominate a cost polynomial of the same degree.

Formalization scope

The model is the published Markov decision chain of Sennott (1999), SennottDP.Discounted.MDC ℕ Act, with its policies, discounted costs and value functions, and the published average cost SennottDP.SEN.avgCost; Markov chains, steady state probabilities and first passage costs are the published SennottDP.MarkovCost objects. Conventions:

• costs, discounted values and average costs lie in $[0,\infty]$; $V_\alpha$ may be infinite unless Assumption 1 is assumed;
• $h_\alpha$ is a real number, used only together with Assumption 1;
• the constants $N$ and $M_i$ of Assumptions 2–3 are explicit and chosen before $i$ and $\alpha$; Assumption 3* uses the same $M$;
• "average cost optimal" always carries a finite constant $g\ge0$ and compares with all policies, not only stationary ones;
• sums $\sum_jP_{ij}(a)h(j)$ against a real function are extended reals (positive part minus negative part);
• "ergodic" means positive recurrent (no aperiodicity);
• in the queue, every decision is formally available in state $0$ with identical cost $Q(0)$ and identical transitions, which represents "no decision in state 0"; $\lambda<\max_a(a\beta)$ is "for some $a$" and $\lambda<\min_a(a\beta)$ "for every $a$".

The second half of the goal is not "there exist $g$ and $h$ satisfying (6)": a pair solving (6) alone carries no optimality content, so the goal ties $g$ to the optimal average cost and $\lim_{\alpha\uparrow1}(1-\alpha)V_\alpha$ and requires $h$ bounded below. The Theorem's milestones are stated for every limit point given by the Lemma, not for some stationary policy. The hypotheses of the goal are satisfiable (two-point arrivals $p_0=3/4$, $p_1=1/4$, one rate $a\beta=1/2$, $Q(i)=i+1$, $B=1$), so the goal is not vacuous.

A complete development needs a discrete Tauberian inequality (already proved on the platform), Fatou's lemma for series, a compactness argument on $\prod_iA_i$, first passage identities and a Foster–Lyapunov criterion for positive recurrence. The Markov chain criteria (Proposition 4, the Corollary) and the Theorem are reusable for every countable-state queueing control model. Proofs of any milestone, and alternative arguments, are welcome.

Selected references

• L. I. Sennott, Average Cost Optimal Stationary Policies in Infinite State Markov Decision Processes with Unbounded Costs, Operations Research 37(4):626–633, 1989. https://doi.org/10.1287/opre.37.4.626
• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999. https://doi.org/10.1002/9780470317037
• S. M. Ross, Applied Probability Models with Optimization Applications, Holden-Day, 1970.
• A. G. Pakes, Some Conditions for Ergodicity and Recurrence of Markov Chains, Operations Research 17(6):1058–1061, 1969. https://doi.org/10.1287/opre.17.6.1058
• A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh, S. I. Marcus, Discrete-Time Controlled Markov Processes with Average Cost Criterion: A Survey, SIAM J. Control Optim. 31(2):282–344, 1993. https://doi.org/10.1137/0331018