Dynamic Programming

Motivation

Infinite-horizon sequential decision problems (deterministic optimal control, Markov decision processes, minimax control) share one computational question: does the dynamic programming (DP) algorithm, which starts from a terminal cost and repeatedly applies the Bellman operator, converge to the optimal cost? For discounted problems with bounded costs the answer is yes, by the contraction mapping theorem (Blackwell 1965; Denardo 1967). Without discounting and boundedness the answer depends on the sign structure of the problem. Strauch's negative programming model (Strauch 1966) and Blackwell's positive programming model behave differently, and in the former the DP algorithm can fail to converge to the optimal cost even for simple deterministic problems.

Bertsekas (1977) recast these models in one abstract framework: a monotone mapping $H$ that encodes the one-stage problem, with no probabilistic or additive structure assumed. Two sign conditions organise the theory: uniform increase (Assumption I, containing Strauch's model) and uniform decrease (Assumption D, containing the deterministic version of Blackwell's positive model, e.g. deterministic problems with nonpositive stage costs). This mission formalizes the uniform-decrease half of Section 5: under D, the finite-horizon problems are solved by the DP algorithm, $J^*$ is the limit of the finite-horizon values, Bellman's equation holds, and the DP algorithm converges to $J^*$. The same framework became the basis of Bertsekas–Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978) and of Bertsekas's Abstract Dynamic Programming (2013, 3rd ed. 2022).

Setting

States, controls, policies. $S$ (nonempty) and $C$ are sets. Each $x\in S$ has a nonempty constraint set $U(x)\subseteq C$. $M$ is the set of selectors $\mu:S\to C$ with $\mu(x)\in U(x)$ for all $x$, and a policy is a sequence $\pi=\{\mu_0,\mu_1,\dots\}$ of selectors. The policy is stationary if $\mu_k=\mu$ for all $k$.

Functions and the mapping $H$. $F$ is the set of functions $J:S\to[-\infty,\infty]$, ordered pointwise, and $e$ is the constant function $1$. A mapping $H:S\times C\times F\to[-\infty,\infty]$ is given, and it is monotone: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$ for every $x$ and $u\in U(x)$. It defines

$$T_\mu(J)(x)=H(x,\mu(x),J),\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J).$$

$T^k$ is the $k$-fold composition, with $T^0$ the identity, and $(T_{\mu_0}\cdots T_{\mu_{N-1}})$ applies $T_{\mu_{N-1}}$ first.

Costs. A terminal function $\bar J\in F$ with $\bar J(x)>-\infty$ is given. The cost of a policy, the optimal cost, the $N$-stage optimal cost and the limit of the DP algorithm are

$$J_\pi=\lim_{N\to\infty}(T_{\mu_0}\cdots T_{\mu_{N-1}})(\bar J),\quad J^*=\inf_{\pi}J_\pi,\quad J_N=\inf_{\pi}(T_{\mu_0}\cdots T_{\mu_{N-1}})(\bar J),\quad J_\infty=\lim_{N\to\infty}T^N(\bar J),$$

all pointwise. $J_\mu$ denotes the cost of the stationary policy $\{\mu,\mu,\dots\}$.

Assumptions. D: $H(x,u,\bar J)\le\bar J(x)$ for all $x$, $u\in U(x)$. Under D every sequence above is nonincreasing, so the limits exist in $[-\infty,\infty]$. D.1: for every sequence with $J_{k+1}\le J_k\le\bar J$, $\lim_k H(x,u,J_k)=H(x,u,\lim_k J_k)$. D.2: there is $\alpha>0$ such that $H(x,u,J)-\alpha r\le H(x,u,J-re)\le H(x,u,J)$ for all $r>0$ and $J\le\bar J$.

Formalization targets

Goal: convergence of the DP algorithm (Proposition 9)

If D holds, and either D.1 holds or $J_N=T^N(\bar J)$ for every $N\ge1$, then

$$J_\infty=J^*.$$

Milestones

1. Lemma 1. Under D, $J^*(x)=\lim_{N\to\infty}J_N(x)$ for every $x$.
2. Proposition 3. Under D, and either D.1 or (D.2 and $T^N(\bar J)>-\infty$ everywhere), $J_N=T^N(\bar J)$ for a given $N\ge1$.
3. Proposition 6. Under D and D.1, $J^*=T(J^*)$, and every $J'\le\bar J$ with $J'\le T(J')$ satisfies $J'\le J^*$.
4. Corollary 6.2. Under D and D.1, $J_\mu=T_\mu(J_\mu)$ for every stationary policy, and every $J'\le\bar J$ with $J'\le T_\mu(J')$ satisfies $J'\le J_\mu$.
5. Proposition 8. Under D and D.1, a stationary policy $\{\mu^*,\mu^*,\dots\}$ is optimal if and only if $T_{\mu^*}(J_{\mu^*})=T(J_{\mu^*})$.

The goal is the paper's answer, in the uniform-decrease case, to the question it poses in the introduction: when is $\lim_N T^N(\bar J)=J^*$?

Significance

The result. Proposition 9 justifies value iteration from $\bar J$ for every problem that fits Assumption D, including deterministic and stochastic control with nonpositive costs (reward maximization with nonnegative rewards) and minimax problems satisfying D.1. Propositions 6 and 8 characterise $J^*$ as the largest solution of Bellman's equation below $\bar J$ and give a verification test for stationary policies. The hypotheses are sharp in the sense the paper documents: its Counterexamples 2 and 3 show $J_N\ne T^N(\bar J)$ when D.1 is dropped together with D.2 or with the finiteness condition $T^N(\bar J)>-\infty$. Under the mirror assumption I, $J_\infty=J^*$ can fail, so the asymmetry between the two sign conditions is part of the content.

Formalizing it. All results are proved in the 1977 paper and reappear in later monographs. No machine-checked version of this abstract framework is known. The platform's existing dynamic programming items are finite-state, real-valued and contraction-based, so this mission would add the first formal treatment of extended-real-valued, non-contractive dynamic programming, and a model definition that other results of the same theory can reuse.

Difficulty

The obvious argument for Proposition 9, "$J_N=T^N(\bar J)$ and $J_N\to J^*$", hides two separate interchanges of limits and infima. Lemma 1 interchanges $\inf_\pi$ with $\lim_N$, which works only because every sequence is monotone in the right direction under D. Proposition 3 is where the work is: the $N$-stage infimum over policies must be matched by the iterated infimum $T^N$, which requires building near-optimal selectors stage by stage and passing a limit through $H$ $N$ times, using D.1, or controlling accumulated errors through D.2. The latter breaks down when values reach $-\infty$, which is why that branch needs $T^N(\bar J)>-\infty$. All arithmetic is in $[-\infty,\infty]$, where expressions such as $\infty-\infty$ are not defined, and $J^*$, $J_N$, $T^N(\bar J)$ may equal $-\infty$ even though $\bar J$ does not.

Formalization scope

The model is a Lean structure MonotoneDP.Decrease.Model S C with fields U, U_nonempty, H, mono, Jbar, Jbar_ne_bot and S_nonempty; $F$ is S → EReal. Policies are ℕ → Selector, where a selector is a function with values in the constraint sets. $T$ is an infimum over U x only, and $J^*$, $J_N$ are infima over admissible policies. $J_\pi$ and $J_\infty$ are limUnder atTop; every theorem assumes D, under which both sequences are nonincreasing and converge, so these are the paper's limits. In D.1 both limits are limUnder. D.2 carries its scalar as a parameter, and "D.2 holds" is ∃ α, AssumptionD2 α. Only real scalars are ever subtracted from extended reals.

$J_N$ is defined for every $N$, and Propositions 3 and 9 quantify over $N\ge1$ as the paper does. In Proposition 3 the condition $T^N(\bar J)>-\infty$ belongs to the D.2 branch only. No hypothesis beyond the page is added. Nonempty constraint sets and $\bar J>-\infty$ are the paper's standing assumptions, stated in the model, not in the theorems. Without nonempty constraint sets there would be no policies, $J^*$ and $J_N$ would be $+\infty$, and several statements would hold trivially; the model rules this out.

Useful contributions: general lemmas about monotone sequences in EReal (interchanging ⨅ and limits), the monotonicity facts (25) and $T^{N+1}(\bar J)\le T^N(\bar J)$ under D, and reusable constructions of near-optimal selectors. Corollary 6.1 (the finite-state D.2 variant) is not included.

Selected references

• D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15(3), 438–464, 1977. https://doi.org/10.1137/0315031
• E. V. Denardo, Contraction mappings in the theory underlying dynamic programming, SIAM Review 9(2), 165–177, 1967. https://doi.org/10.1137/1009030
• R. E. Strauch, Negative dynamic programming, Ann. Math. Statist. 37(4), 871–890, 1966. https://doi.org/10.1214/aoms/1177699147
• D. Blackwell, Discounted dynamic programming, Ann. Math. Statist. 36(1), 226–235, 1965. https://doi.org/10.1214/aoms/1177700285
• D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific, 2022. https://www.mit.edu/~dimitrib/abstractdp_MIT.html

Motivation

Firms that can buy the same item from two suppliers, a cheap slow one and a fast expensive one, face the dual-sourcing inventory problem: how much to order from each source in every period when demand is random and unmet demand is backlogged. Global sourcing (offshore regular supply plus a near-shore express supply) is the standard example (Allon and Van Mieghem 2010). When the two lead times differ by more than one period, the optimal policy depends on the whole pipeline of outstanding orders. No simple optimal policy is known, and dynamic programming is intractable for long lead times.

The tailored base-surge (TBS) policy orders a constant amount from the slow source and uses the fast source to bring the expedited inventory position up to a fixed level. It is simple, and it is used in practice. Janakiraman, Seshadri and Sheopuri (JSS, Management Science 2015) showed that its best parameters solve a convex program that does not depend on the regular lead time, and they conjectured, with numerical support, that TBS is near-optimal when that lead time is long.

Timeline:

• Karlin and Scarf (1958), Scarf (1960): structure of optimal single-source backlog policies with a lead time.
• Sheopuri, Janakiraman and Seshadri (2010): reduction of dual-sourcing policies to the truncated regular pipeline and the expedited inventory position (Lemma 1 here).
• Allon and Van Mieghem (2010): the TBS policy, with conjectures and numerical evidence.
• JSS (2015): the TBS cost formula and a convex program for its parameters.
• Xin and Goldberg (2018): proof of the conjecture with an explicit rate (Management Science 64(1), 2018). This mission formalizes that result.

Setting

Let $D$ be a nonnegative random variable with finite mean $\mathbb E[D]$ that is not almost surely constant. Demands $D_1, D_2, \dots$ are i.i.d. copies of $D$. The regular source has lead time $L$, the express source has lead time $L_0 \ge 0$, and $L > L_0 + 1$. In period $t$ the controller orders $q^R_t \ge 0$ and $q^E_t \ge 0$; then $q^R_{t-L} + q^E_{t-L_0}$ arrives and $D_t$ is realized, so the on-hand inventory evolves as $I_{t+1} = I_t + q^R_{t-L} + q^E_{t-L_0} - D_t$ and may be negative. Initially nothing is on order and $I_1 = -\sum_{i=1}^{\hat G} D'_{-i}$, where the $D'_{-i}$ are further i.i.d. copies of $D$ and $\mathbb P(\hat G = k) = 2^{-k}$, $k \ge 1$.

The per-period cost is $c\,q^E_{t-L_0} + G(I_{t+1})$ with $G(y) = h y^+ + b y^-$, where $b, h > 0$ and $c > 0$ is the express premium (the regular unit cost is normalized to $0$). An admissible policy $\pi \in \Pi$ chooses the two orders in period $t$ as deterministic measurable functions of $(q^R_{t-L}, \dots, q^R_{t-1}, q^E_{t-L_0}, \dots, q^E_{t-1}, I_t)$. Its long-run average cost is

$$C(\pi) = \limsup_{T\to\infty}\frac1T\sum_{t=L_0+1}^T \mathbb E[C^\pi_t], \qquad \mathrm{OPT}(L) = \inf_{\pi\in\Pi}C(\pi).$$

With the expedited inventory position $\hat I_t = I_t + \sum_{k=t-L_0}^{t-1}q^E_k + \sum_{k=t-L}^{t-L+L_0}q^R_k$, the TBS policy $\pi_{r,S}$ orders $q^R_t = r$ and $q^E_t = \max(0, S - \hat I_t)$. A best TBS pair $(r^*, S^*)$ minimizes $C(\pi_{r,S})$ over $0 \le r \le \mathbb E[D]$ and $S \in \mathbb R$ (first in $r$ through $F^\infty(r) = \inf_S C(\pi_{r,S})$, then in $S$).

The constants $\epsilon_0$ and $Y_0$ are explicit functionals of the law of $D$ and of $L_0, b, h, c$. They are built from $g = \inf_x\mathbb E[G(x - \sum_{i=1}^{L_0+1}D'_i)]$, $U = c\,\mathbb E[D] + \mathbb E[G(-\sum_{i=1}^{L_0+1}D'_i)]$, $p_0 = \mathbb P(D < \mathbb E[D])$, the mean absolute deviation $\eta_0$, and the large-deviation quantities $\gamma_\epsilon, \vartheta_\epsilon$ of $\phi_\epsilon(\theta) = e^{\theta(\mathbb E[D]-\epsilon)}\mathbb E[e^{-\theta D}]$ (p. 441).

Formalization targets

Goal: Theorem 1 (p. 441)

For all $L_0 \ge 0$, $\epsilon \in (0,1)$ and $L > \epsilon_0^{-2} + Y_0\epsilon^{-2}$,

$$\frac{C(\pi_{r^*,S^*})}{\mathrm{OPT}(L)} < 1 + \epsilon.$$

The threshold does not depend on $L$, so the statement gives an explicit, inverse-polynomial rate. Its limit form $C(\pi_{r^*,S^*})/\mathrm{OPT}(L) \to 1$ is Corollary 1 of the paper.

Milestones

In the order the proof uses them:

• the bound $g \le \mathrm{OPT}(L) \le U$;
• Lemma 1, the reduction to $\hat\Pi$ (quoted from Sheopuri et al.);
• Eq. (3), the TBS cost formula $C(\pi_{r,S}) = c(\mathbb E[D]-r) + \mathbb E[G(I^r_\infty + S - \sum_{i=1}^{L_0+1}D'_i)]$ (quoted from JSS);
• Theorem 2, the existence of a stationary-like vector $(\chi^{*,L}, q^{*,L}, \mathcal I^{*,L})$ with $r_L = \mathbb E[\chi^{*,L}_1]$;
• Corollary 2 and Lemma 2, the lower bound $\mathrm{OPT}(L) \ge c(\mathbb E[D]-r_L) + (1-\alpha)V^{L-L_0}_\alpha(r_L,-\infty)$ through a discounted single-source problem;
• Lemma 3, the Bellman equation and structure of that problem (quoted from JSS and Scarf 1960);
• Lemma 4 (8) and (9), and Corollary 3, the passage to the infinite horizon and to base-stock policies;
• Lemma 5, the random-walk maxima $M^r_k$ (proof omitted in the paper);
• Lemmas 8–9 and Corollary 4: $r_L < \mathbb E[D] - \epsilon_0$ once $L > \epsilon_0^{-2} + L_0 + 1$.

Significance

The theorem shows that one of the simplest dual-sourcing heuristics is asymptotically optimal as the regular lead time grows. This is the regime where exact dynamic programming is hopeless. The best TBS parameters come from a convex program independent of $L$, so the result yields an algorithm whose running time does not grow with $L$ and whose optimality gap is bounded explicitly for every finite $L$. It extends the lower-bounding technique of Xin and Goldberg's lost-sales work (Operations Research 2016) from a static to a dynamic relaxation.

Formalization adds the following. To the best of available knowledge, none of the objects involved (average-cost inventory control with backlog, TBS policies, Lindley-type maxima of random walks with their Spitzer identity) exists in Mathlib or on the platform. The paper's proof defers several ingredients to the literature or omits them: Lemma 1, Eq. (3), Lemma 3, and the details of Lemmas 5 and 7. A complete formal proof must supply them. The result is proved on paper but not formalized anywhere.

Difficulty

An optimal dual-sourcing policy need not be stationary, its induced Markov chain need not have a stationary distribution, and the inventory is unbounded below. The natural argument would compare the optimal policy's steady state with the TBS steady state, and it fails at its first step. Theorem 2 replaces the steady state by a vector with a few distributional properties, built from time averages. That construction, and the independence structure it must carry, is the central technical step. The conditional Jensen step then leads to a single-source problem with possibly negative demand, where textbook interchange-of-limits theorems do not apply directly. Finally, bounding $r_L$ away from $\mathbb E[D]$ requires a quantitative lower bound on the growth of random-walk maxima under only a first-moment assumption.

Formalization scope

Conventions of the Lean development (namespace XinGoldbergTBS.Asymptotic):

• The law of $D$ is a probability measure on $\mathbb R$ with no mass on $(-\infty,0)$, finite mean, and no atom of mass $1$. The paper's "strictly positive (possibly infinite) variance" is read as "not almost surely constant".
• $c_R = 0$, $b > 0$, $h > 0$, $c > 0$, and $L, L_0$ are natural numbers. The paper's standing assumption $L > L_0 + 1$ is a hypothesis wherever the paper states it; in Theorem 1 it follows from the threshold.
• Costs, expectations, $C(\pi)$, $\mathrm{OPT}(L)$, $V^n_\alpha$ and $V^\infty_\alpha$ take values in $[0,\infty]$, so infinite costs are never truncated. The ratio in Theorem 1 is stated as $C(\pi_{r^*,S^*}) < (1+\epsilon)\mathrm{OPT}(L)$, which is equivalent because $0 < g \le \mathrm{OPT}(L) \le U < \infty$.
• $\Pi$ is exactly the paper's class: deterministic, time-dependent, measurable, nonnegative orders that depend on the pipeline and inventory. It is neither restricted to stationary policies nor enlarged to randomized ones. TBS policies are members, so $C(\pi_{r,S}) \ge \mathrm{OPT}(L)$ by construction.
• $\vartheta_\epsilon \in [0,\infty]$ is the supremum of the minimizers of $\phi_\epsilon$ on $[0,\infty)$, and it is $\infty$ if the infimum is not attained; $1/\infty = 0$.
• The existence of a best TBS pair is asserted in the paper via JSS. The goal therefore also asserts that some TBS policy with $0 \le r \le \mathbb E[D]$ meets the bound, so it cannot hold vacuously when no minimizer exists.
• $r_L$ belongs to a witness of Theorem 2, and the results that use it hold for every witness.
• The single-source class $\bar\Pi$ ("feasible nonanticipative policies, as typically defined") is read as nonnegative orders that are measurable functions of past demands. In Lemma 3 "increasing" is read as nondecreasing, and convexity in $x$ includes finiteness.
• The paper states Eq. (3) without a range for $r$; it is stated here for $0 \le r \le \mathbb E[D]$, the TBS parameters over which the paper optimizes. At $r = \mathbb E[D]$ both sides are $+\infty$. In Lemma 8, the range's upper end is $+\infty$ when $\epsilon = 0$.
• Differences such as $V^\infty_\alpha - V^n_\alpha$ and $M^r_\infty - M^r_n$ are stated additively, and the negative terms of (9) and Corollary 3 are moved to the other side.

Lemma 1, Eq. (3) and Lemma 3 are results the paper quotes from Sheopuri et al. (2010), JSS and Scarf (1960). Proposition 1 (conditional-expectation form of the bound) is not included.

A trivializing formalization is ruled out: $\mathrm{OPT}(L)$ ranges over the full admissible class, the constants are definitions rather than hypotheses, and the goal includes an existence clause.

Reusable beyond this mission: average-cost inventory models with lead times, discounted single-source backlog value functions, and Spitzer-type identities for random-walk maxima. Contributions to any milestone are welcome.

Selected references

• L. Xin and D. A. Goldberg, Asymptotic Optimality of Tailored Base-Surge Policies in Dual-Sourcing Inventory Systems, Management Science 64(1):437–452, 2018. https://doi.org/10.1287/mnsc.2016.2607
• G. Janakiraman, S. Seshadri and A. Sheopuri, Analysis of Tailored Base-Surge Policies in Dual Sourcing Inventory Systems, Management Science 61(7):1547–1561, 2015.
• G. Allon and J. A. Van Mieghem, Global Dual Sourcing: Tailored Base-Surge Allocation to Near- and Offshore Production, Management Science 56(1):110–124, 2010.
• A. Sheopuri, G. Janakiraman and S. Seshadri, New Policies for the Stochastic Inventory Control Problem with Two Supply Sources, Operations Research 58(3):734–745, 2010.
• H. Scarf, The Optimality of (s, S) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960, pp. 196–202.
• L. Xin and D. A. Goldberg, Optimality Gap of Constant-Order Policies Decays Exponentially in the Lead Time for Lost Sales Models, Operations Research 64(6):1556–1565, 2016.

Motivation

A Markovian decision process (Howard, 1960) models a controller who, in each of finitely many states, picks a decision, earns a reward and moves to a random next state according to known transition probabilities. In applications (inventory control, equipment replacement, quality control) those probabilities are estimated, not known. Satia and Lave (Operations Research 21(3), 1973) treat the uncertainty in two ways: a game-theoretic formulation, in which each unknown row only lies in a given set, and a Bayesian formulation, going back to Silver (1963) and Martin (1967), in which the controller holds a prior on the unknown matrix and learns from observed transitions.

The Bayesian problem is the natural one but its state includes the whole prior, so it cannot be solved exactly beyond small cases. The paper's contribution in the Bayesian part is a pair of computable bounds on the Bayesian optimal return in terms of the two game-theoretic values (max-max and max-min). This mission formalizes those bounds and the chain of facts they rest on.

Setting

There are $N$ states $i$ and, in state $i$, a finite nonempty set $K_i$ of decisions. A transition $i \to j$ under decision $k$ earns $r^k_{ij}$ and rewards are discounted by $\beta$, $0 \le \beta < 1$. The row $p_i^k = (p^k_{ij})_j$ of transition probabilities is unknown; it is known to lie in a closed convex nonempty set $S_i^k$ of probability vectors, and $S = \{P : p_i^k \in S_i^k \text{ for all } i, k\}$.

A prior $g$ is a probability distribution on matrices $P = (p_i^k)$ whose rows are all probability vectors. Its means are $\bar p^k_{ij} = E(p^k_{ij})$. After a transition $l \to j$ under decision $m$ the prior is replaced by the Bayes transformation $T^m_{lj} g(P) = C\,p^m_{lj}\,g(P)$ (Eq. (8)), with $C$ the normalizing constant. The Bayesian optimal return $f(i,g)$ solves the recursion

$$f(i, g) = \max_{k \in K_i} \Big\{ \sum_j \bar p^k_{ij} r^k_{ij} + \beta \sum_j \bar p^k_{ij} f(j, T^k_{ij} g) \Big\}. \qquad (10)$$

The max-max and max-min values $V^+$, $V^-$ solve

$$V_i^\pm = \max_{k \in K_i} \operatorname*{max/min}_{p_i^k \in S_i^k} \Big\{ \sum_j p^k_{ij} r^k_{ij} + \beta \sum_j p^k_{ij} V_j^\pm \Big\},$$

with max for $V^+$ and min for $V^-$. Finally $\alpha = \operatorname{prob}(P \in S \mid g)$, the prior probability that the true matrix lies in $S$.

The Lean development lives in the namespace SatiaLave.Bayes: UncertainMDP, IsPrior, pbar, bayes, SolvesEq10, SolvesVplus, SolvesVminus, alpha, rmax, rmin, policyValue.

Formalization targets

Goal: Propositions 9 and 10

For every bounded solution $f$ of (10), all solutions $V^+$, $V^-$, every prior $g$ and every state $i$,

$$\alpha V_i^- + (1-\alpha)\min_{i,j,k}\frac{r^k_{ij}}{1-\beta} \;\le\; f(i,g) \;\le\; \alpha V_i^+ + (1-\alpha)\max_{i,j,k}\frac{r^k_{ij}}{1-\beta},$$

together with the existence of $f$, $V^+$ and $V^-$. Both halves are the paper's printed statements.

Milestones

1. Proposition 6 (Martin): (9)/(10) has a unique bounded solution (unique at priors).
2. No learning (p. 733): at a point-mass prior $\delta_P$, $f(\cdot,\delta_P)$ solves the optimality equations of the process with known $P$.
3. Proposition 8: $f(i,g)$ is convex in $g$.
4. Jensen step (proof of Proposition 9): $f(i,g) \le \int f(i,\delta_P)\,dg(P)$.
5. Policy step (proof of Proposition 10): $f(i,g) \ge \int [q + \beta P^A q + \beta^2 [P^A]^2 q + \cdots]_i\,dg(P)$ for every pure stationary policy $A$.

Significance

The result. The bounds sandwich an intractable quantity between two quantities computable by finite algorithms (the max-max and max-min policy-iteration procedures of the same paper), weighted by a single prior probability $\alpha$. When the prior concentrates on $S$ ($\alpha \to 1$) the bounds become $V_i^- \le f(i,g) \le V_i^+$: the Bayesian return lies between the pessimistic and optimistic robust values. They are the upper and lower bounds on the return that the paper's implicit-enumeration method (the decision tree of its Fig. 2 and Proposition 12) uses to compare decisions. The Jensen step is a value-of-information inequality (Bayesian optimal return is at most the expected full-information optimal return), which recurs throughout Bayesian control and bandit theory.

Formalizing it. The results are proved on paper (Propositions 6 and 8 by reference to Martin's book and Satia's thesis, Propositions 9 and 10 in the text); none is machine-checked. The mission produces a Lean model of Bayes-adaptive Markov decision processes with priors as measures, the Bayes transformation and its fixed-point recursion, and the link between the Bayesian and the robust (rectangular) formulations. Martin's existence-uniqueness theorem and the convexity of the Bayesian value are reusable for any Bayes-adaptive model.

Difficulty

The prior space is infinite-dimensional and not a vector space, so the recursion (10) lives on a space of measures, and the usual finite-state arguments do not apply verbatim. Proposition 8 gives convexity only along finite mixtures, while the proof of Proposition 9 applies Jensen's inequality to the integral mixture $g = \int \delta_P\,dg(P)$ of point masses; bridging the two, or proving the value-of-information inequality directly, is the central step. The paper also restricts the point masses to $x_i^k \in S_i^k$, which cannot represent a prior with mass outside $S$; the formal statement integrates over every transition matrix, as the next line of the paper's display requires. Measurability of $P \mapsto f(i,\delta_P)$ is not automatic, since $f$ is only characterized by a functional equation.

Formalization scope

• States are a nonempty Fintype S; decisions a dependent family D i of nonempty finite types. A matrix is P : (i : S) → D i → S → ℝ with the product Borel $\sigma$-algebra.
• Priors are measures: a probability measure giving full mass to matrices whose rows are probability vectors. This generalizes the paper's densities $g(P)$ and includes the point masses $a_x$ its proof uses.
• Bayes transformation at $\bar p = 0$: the normalizing constant does not exist; bayes then returns $g$. That posterior is always multiplied by $\bar p = 0$ in (10), so the choice is immaterial.
• Readings of informal words. "The problem reduces to a Markovian decision process" = at a point-mass prior, fixed by every Bayes transformation, $f$ solves the known-$P$ optimality equations. "Convex in $g$" = convex along mixtures of priors. "Unique set of bounded functions" = two bounded solutions agree at every prior (values at non-priors are unconstrained). "Satisfy (9)" is formalized as (10), which the paper derives from (9) by linearity of $E$. $\max_{P\in S}$/$\min_{P\in S}$ in $V^\pm$ is taken over the row $p_i^k \in S_i^k$ (the only row that enters; $S$ is a product), as ⨆/⨅ over a nonempty bounded set. "Obviously $f(i,g)\ge V_i^A$" is stated for every pure stationary policy $A$, not only a max-min optimal one. The policy return is the componentwise series $\sum_n \beta^n (P^A)^n q$.
• Added hypotheses, not printed: $0 \le \beta < 1$; $S_i^k \ne \emptyset$; $N \ge 1$. Printed and kept: $S_i^k$ closed and convex.
• $f$, $V^+$, $V^-$ are quantified as solutions of their equations; $\alpha$ is computed from $g$, never a free parameter; $\max_{i,j,k}[r^k_{ij}/(1-\beta)]$ ranges over all states $i,j$ and $k \in K_i$. Integrability of the integrands in milestones 4 and 5 is part of their conclusions.
• Trivializations ruled out. A free $\alpha \in [0,1]$, or $f$ defined off priors, would make the goal false or vacuous; the goal also asserts that bounded $f$ and $V^\pm$ exist, so its universal part is not vacuous.
• Not in scope: Proposition 7 (matrix-beta conjugacy, which needs a Dirichlet distribution), Propositions 11–13 and the numerical example.

Welcome contributions: the Banach fixed-point argument for (10) on bounded functions of priors; lemmas that bayes maps priors to priors and that point masses are fixed; continuity of the known-$P$ optimal value in $P$; a general Jensen inequality for functions convex along mixtures of probability measures.

Selected references

• J. K. Satia and R. E. Lave, Jr., Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3), 728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• J. J. Martin, Bayesian Decision Problems and Markov Chains, Wiley, New York, 1967.
• E. A. Silver, Markovian Decision Processes with Uncertain Transition Probabilities or Rewards, Interim Technical Report No. 1, Operations Research Center, Massachusetts Institute of Technology, August 1963.
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• J. K. Satia, Markovian Decision Process with Uncertain Transition Matrices or/and Probabilistic Observation of States, Ph.D. dissertation, Stanford University, 1968.

Motivation

Many operational systems move between a finite number of states at random times: a machine alternates between working and repair, a queue between occupancy levels, an inventory between stock positions. When the time spent in a state is not exponential and not a fixed period, neither discrete-time Markov decision processes nor continuous-time Markov chains describe the system faithfully. William S. Jewell's 1963 paper Markov-Renewal Programming. I extends Howard's Markov decision processes to Markov-renewal processes (also called semi-Markov processes), in which the time between transitions is a random variable whose law depends on the current state, the next state, and the decision taken. The resulting model, now called a semi-Markov decision process, is standard in maintenance, queueing control and reliability.

Timeline:

• 1954: Lévy, Smith and Takács independently introduce Markov-renewal and semi-Markov processes; Pyke later surveys them.
• 1960: Howard, Dynamic Programming and Markov Processes, introduces policy iteration for finite discrete-time Markov decision processes.
• 1962: Blackwell, Discrete Dynamic Programming, shows that for the discounted discrete-time problem a stationary policy is optimal among all policies.
• 1963: Jewell formulates Markov-renewal programming, with a continuous discount factor α, and carries Howard's algorithm and Blackwell's stationarity result over to it. Part II of the paper treats the undiscounted (infinite-return) models.

Setting

A Markov-renewal program has a finite set of states $S$ (the paper's $i = 1, \dots, N$) and a finite, nonempty set of alternatives (the paper's $z = 1, \dots, Z$), each available in every state. For each alternative $z$ and states $i, j$ it specifies:

• a transition probability $p^z_{ij} \ge 0$, with $\sum_j p^z_{ij} = 1$;
• a sojourn-time distribution $F^z_{ij}$, the law of the time $\tau$ between entering $i$ and moving to $j$, with $\tau \ge 0$ and $F^z_{ij}(0) = 0$;
• for each continuous discount factor $\alpha > 0$, a real number $\rho^z_{ij}(\alpha)$, the expected discounted return earned during that transition.

The Laplace–Stieltjes transform $\tilde f^z_{ij}(s) = \int_0^\infty e^{-st}\,dF^z_{ij}(t)$ is the expected discount $\mathbb E[e^{-s\tau}]$ over one interval. The average one-step return is $\rho^z_i(\alpha) = \sum_j p^z_{ij}\rho^z_{ij}(\alpha)$, and for a vector of returns $v$ the test quantity is

$$\rho^z_i(\alpha) + \sum_j p^z_{ij}\,\tilde f^z_{ij}(\alpha)\,v_j .$$

A stationary policy is a map $d : S \to A$; a nonstationary policy is a sequence $\pi = (\pi_0, \pi_1, \dots)$ of such maps, $\pi_k$ being used at the $k$-th transition. The $n$-step return $V^\pi_i(n)$ of a policy, with boundary rewards $V_i(0,\alpha)$, is the test quantity of $\pi_0(i)$ applied to the $(n-1)$-step return of the shifted policy; the optimal $n$-step return $V_i(n,\alpha)$ of equation (6) replaces $\pi_0(i)$ by a maximum over $z$. The value-determination equations (15) of a stationary policy $d$ are $v_i = \rho^{d(i)}_i(\alpha) + \sum_j p^{d(i)}_{ij}\tilde f^{d(i)}_{ij}(\alpha) v_j$.

The algorithm of Fig. 1 alternates two steps: solve (15) for the current policy, then in every state pick an alternative maximizing the test quantity, keeping the old alternative if it still attains the maximum. It stops when two successive policies are identical.

Formalization targets

Goal (p. 947)

For every $\alpha > 0$: (15) has a unique solution for every stationary policy, and every run $(d_k, v_k)$ of Fig. 1 reaches $d_{K+1} = d_K$ with $K < Z^N$, where

$$\lim_{n\to\infty} V^{d_K}_i(n) = (v_K)_i,\qquad \lim_{n\to\infty} V^\pi_i(n) \le (v_K)_i \ \ \forall \pi,\qquad \lim_{n\to\infty} V_i(n,\alpha) = (v_K)_i ,$$

for every state $i$ and all boundary rewards, every limit existing. This is the paper's "the algorithm of Fig. 1 produces an optimal, stationary policy that is as good as any optimal, nonstationary policy".

Milestones

1. p. 945: $0 \le p^z_{ij}\tilde f^z_{ij}(s) < 1$ for $s > 0$.
2. Claim (a): (15) has exactly one solution for each stationary policy.
3. Eq. (15): the $n$-step return of a stationary policy converges to a solution of (15).
4. p. 946: $I - \tilde q(\alpha)$ is invertible and $([I-\tilde q(\alpha)]^{-1})_{ii} \ge 1$.
5. Claim (b): a change of policy raises the return of some state and lowers none.
6. Claim (c): a policy reproduced by the improvement step is optimal among stationary policies.
7. Claim (d): a run of Fig. 1 terminates within $Z^N$ cycles.
8. Eq. (14): $V_i(n,\alpha)$ converges, independently of the boundary rewards, to a solution of $v_i = \max_z\{\rho^z_i(\alpha) + \sum_j p^z_{ij}\tilde f^z_{ij}(\alpha) v_j\}$.
9. p. 946: some stationary policy's return dominates the limiting return of every nonstationary policy.

Significance

The result says that the infinite-step discounted Markov-renewal program is solved exactly, in finitely many cycles, by a finite-dimensional algorithm, and that the answer is a stationary policy. As the paper notes, this matters operationally because a nonstationary policy is hard to follow. The sojourn distributions enter only through the numbers $\tilde f^z_{ij}(\alpha)$, so the same algorithm serves any sojourn-time law. For fixed $\alpha$ the model is a discounted Markov decision process whose discount factor depends on the transition, which contains Howard's and Blackwell's constant-discount problem as the case of intervals of fixed length (p. 943).

The results are classical and proved in the literature. The paper itself refers the proofs to Howard and Blackwell. Machine-checked versions exist on this platform for finite stochastic shortest path and constant-discount problems (Bertsekas, Dynamic Programming and Optimal Control, Prop. 7.2.2 and 7.3.1, mission Dynamic Programming and Optimal Control VII). No formal treatment of Markov-renewal programs, of transition-dependent discounting, or of the retention rule of Fig. 1 is known to exist. The mission produces a verified policy-iteration theorem for semi-Markov decision processes, with an explicit termination bound and the comparison against nonstationary policies.

Difficulty

The discount over one transition, $\tilde f^z_{ij}(\alpha)$, varies with $i$, $j$ and $z$, so the problem is not a constant-$\gamma$ contraction of textbook form; the relevant bound is that every row of $\tilde q(\alpha)$ sums to less than one, which rests on $F^z_{ij}(0) = 0$. Entries in $[0, 1)$ alone, the paper's stated justification of Claim (a), do not make $I - \tilde q(\alpha)$ invertible: the $2 \times 2$ matrix with every entry $1/2$ has entries in $[0,1)$, yet $I$ minus it is singular.

Finite termination is not automatic either. If the improvement step may switch between tied maximizers, the iterates can cycle forever between two policies with equal returns; the retention rule of Fig. 1 excludes this, and Claim (b) must deliver a strict increase in some state, with no decrease anywhere, to rule out revisiting a policy. Comparing with nonstationary policies requires controlling returns of arbitrary policy sequences, whose limits must be shown to exist, not assumed.

Formalization scope

• States and alternatives are finite types; alternatives are nonempty. Every alternative is available in every state.
• $F^z_{ij}$ is a probability measure on $\mathbb R$ with no mass on $(-\infty, 0]$. The transform is integrated over $(0, \infty)$, which carries all the mass.
• The one-transition returns $\rho^z_{ij}(\alpha)$ are arbitrary real numbers, a generalization of the paper's Stieltjes integral (4), which is not formalized. The reward functions $R^z_{ij}(t\mid\tau)$ do not appear.
• Returns of policies are defined by the one-step recursion (the policy form of (6)); the Markov-renewal process is not built as a stochastic process.
• Policies are the paper's: deterministic and Markov, nonstationary ones indexed by the number of transitions made. Randomized and history-dependent policies are not in the comparison class.
• The following informal words are read as follows. "Solve the set of simultaneous equations": (15) has exactly one solution. "Strictly increases the expected return of at least one state": no state's return decreases and one strictly increases, under the hypothesis that the policy changed. "No other policy can lead to higher expected returns" in Claim (c): no stationary policy. "Terminates in a finite number of cycles": two successive policies coincide at some cycle $K < Z^N$. "If there is no improvement in the test quantity, retain the same alternative": the old alternative is kept whenever it attains the maximum. "Optimal" and "as good as any nonstationary policy": the limiting return of the returned policy dominates that of every policy from every state, for all boundary rewards. "$\lim_{n\to\infty} V_i(n,\alpha)$": the limit is proved to exist. "$\max_z$": a maximum over the finite nonempty set of alternatives.
• Eq. (14) is printed with $v_i(\alpha)$ inside the sum over $j$; the formalization uses $v_j(\alpha)$, as (6), (15) and Fig. 1 do.
• Every statement fixes one $\alpha > 0$. The undiscounted models (16)–(19), the finite-time and mixed-horizon models (9)–(13), and the infinite-time case of the stationarity result are out of scope.
• The return of a policy is never defined through a matrix inverse, whose Mathlib value for a singular matrix is $0$; (15) is a predicate, and the goal asserts unique solvability, so a vacuous reading through junk inverses or assumed limits is excluded.

Reusable infrastructure: bounds for substochastic matrices with row sums below one (invertibility, Neumann series, nonnegative inverse), convergence of iterated Bellman operators with transition-dependent discount, and the policy-iteration termination argument with a tie-breaking rule. Proofs of any milestone and alternative arguments are welcome.

Selected references

• W. S. Jewell, Markov-Renewal Programming. I: Formulation, Finite Return Models, Operations Research 11(6), 938–948, 1963. https://doi.org/10.1287/opre.11.6.938
• W. S. Jewell, Markov-Renewal Programming. II: Infinite Return Models, Example, Operations Research 11(6), 949–971, 1963. https://doi.org/10.1287/opre.11.6.949
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• D. Blackwell, Discrete Dynamic Programming, Annals of Mathematical Statistics 33(2), 719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• R. Pyke, Markov Renewal Processes: Definitions and Preliminary Properties, Annals of Mathematical Statistics 32(4), 1231–1242, 1961. https://doi.org/10.1214/aoms/1177704863
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Section 7.2–7.3.

Motivation

A coherent risk measure assigns to a future financial position the smallest amount of capital that makes it acceptable to a supervisor. Artzner, Delbaen, Eber and Heath characterised the one-period version: every coherent risk measure has the form $\pi(X)=\inf_{\mathbb Q\in\mathcal P}\mathbb E_{\mathbb Q}[X]$ for a set $\mathcal P$ of test probabilities (ADEH 1999). Regulators, insurers and banks, however, assess positions that evolve over several periods and whose risk is re-evaluated as information arrives. A multiperiod measurement should then be time consistent: the value assigned today should agree with the values the same method assigns tomorrow, so that it can be computed by backward induction, as in dynamic programming.

Artzner, Delbaen, Eber, Heath and Ku (Ann. Oper. Res. 2007) identify exactly which sets of test probabilities give time-consistent multiperiod risk-adjusted values. The condition, stability under pasting, also appears as "rectangularity" in the recursive multiple-priors model of decision theory (Epstein and Schneider 2003), and as m-stability in the theory of risk-neutral measures (Delbaen, The structure of m-stable sets, Séminaire de Probabilités XXXIX, 2006). Riedel treated dynamic coherent risk measures on finite state spaces (Riedel 2004); the continuous-time case is in Delbaen's m-stable paper and Cheridito, Delbaen and Kupper 2004.

Setting

Let $(\Omega,\mathcal F,\mathbb P_0)$ be a probability space with a filtration $(\mathcal F_n)_{n\ge0}$ and a horizon $N$. A value process is an adapted process $X=(X_n)_{0\le n\le N}$ with every $X_n$ essentially bounded; the class of value processes is $\mathcal G$. All stopping times take values in $\{0,\dots,N\}$, and $\mathcal F_\sigma$ is the σ-algebra of the stopping time $\sigma$.

A set $\mathcal P$ of test probabilities is a closed convex set of probabilities on $(\Omega,\mathcal F_N)$, each absolutely continuous with respect to $\mathbb P_0$. Its elements are identified with their densities $f=d\mathbb Q/d\mathbb P_0$, and "closed" refers to $L^1(\mathbb P_0)$. $\mathcal P^e$ denotes the elements equivalent to $\mathbb P_0$. Each $\mathbb Q\in\mathcal P$ has the density martingale $Z^{\mathbb Q}_n=\mathbb E_{\mathbb P_0}[d\mathbb Q/d\mathbb P_0\mid\mathcal F_n]$.

Pasting. For $\mathbb Q^0,\mathbb Q\in\mathcal P^e$ with density martingales $Z^0,Z$ and a stopping time $\tau$, the pasted martingale is $L_n=Z^0_n$ for $n\le\tau$ and $L_n=Z^0_\tau Z_n/Z_\tau$ for $n\ge\tau$: the pasted probability follows $\mathbb Q^0$ up to $\tau$ and $\mathbb Q$ afterwards. $\mathcal P$ is stable (Definition 3.1) if every such pasting is again in $\mathcal P$.

Two risk-adjusted values. For a value process $X$ and a stopping time $\sigma$,

$$\Psi_\sigma(X)=\operatorname*{ess.inf}\bigl\{\mathbb E_{\mathbb Q}[X_\tau\mid\mathcal F_\sigma]\ \bigm|\ \tau\ge\sigma\text{ a stopping time},\ \mathbb Q\in\mathcal P^e\bigr\},$$

the worst conditional expected value over all test probabilities and all later stopping times. The generalized Snell envelope is the backward recursion

$$\bar\Psi_N(X)=X_N,\qquad \bar\Psi_n(X)=X_n\wedge\operatorname*{ess.inf}_{\mathbb Q\in\mathcal P^e}\mathbb E_{\mathbb Q}\bigl[\bar\Psi_{n+1}(X)\mid\mathcal F_n\bigr].$$

For a stopping time $\tau$ let $X^{\tau-}_n=X_n$ for $n<\tau$ and $X_{\tau-1}$ for $n\ge\tau$, and ${}^\tau X_n=0$ for $n<\tau$ and $X_n-X_{\tau-1}$ for $n\ge\tau$.

Formalization targets

Goal: Theorem 4.2

Assume $\mathcal F_0$ is $\mathbb P_0$-trivial and $\mathcal P^e\neq\emptyset$. Then the following are equivalent:

1. $\mathcal P$ is stable.
2. For every $\mathbb Q\in\mathcal P$ and $X\in\mathcal G$, $\Psi(X)$ is a $\mathbb Q$-submartingale.
3. $\Psi(X)=\bar\Psi(X)$ for every $X\in\mathcal G$.
4. Bellman's principle holds: for every $X\in\mathcal G$ and all stopping times $\sigma\le\tau$,

$$\Psi_\sigma(X)=\Psi_\sigma\bigl(X^{\tau-}+\Psi_\tau({}^\tau X)\mathbf 1_{[\tau,N]}\bigr).$$

Milestones

In attack order, all stated for any set $\mathcal P$ with $\mathcal P^e\neq\emptyset$ unless stability is named:

• Theorem 4.1. $\bar\Psi(X)$ is the largest process in $\mathcal G$ that lies below $X$ and is a $\mathbb Q$-submartingale for every $\mathbb Q\in\mathcal P$.
• Step (1) of the proof of Theorem 4.2. $\Psi_n(X)\ge\bar\Psi_n(X)$.
• Theorem 4.2, first sentence. The family $(\Psi_\sigma(X))_\sigma$ is a process: $\Psi_\sigma(X)=\Psi_{\sigma(\omega)}(X)(\omega)$ a.s.
• Remark after Theorem 4.2. $\Psi_\tau(X)=\Psi_\tau({}^\tau X)+X_{\tau-1}$.
• Lemma 3.1 (stable $\mathcal P$). For $\tau\le\sigma\le\nu$, $\{(Z_\nu/Z_\sigma,Z_\sigma/Z_\tau)\mid Z\in\mathcal P^e\}=\{(Z'_\nu/Z'_\sigma,Z_\sigma/Z_\tau)\mid Z,Z'\in\mathcal P^e\}$.
• Lemma 4.1 (stable $\mathcal P$). The family defining $\Psi_\sigma(X)$ is closed under minima and maxima.
• Corollary of Lemma 4.1 (stable $\mathcal P$). $\mathbb E_\mu[\Psi_\sigma(X)]=\inf\{\mathbb E_\mu[\mathbb E_{\mathbb Q}[X_\tau\mid\mathcal F_\sigma]]\mid\mathbb Q\in\mathcal P^e,\ \tau\ge\sigma\}$ for every probability $\mu\ll\mathbb P_0$.

A supporting item states that the essential infimum defining $\Psi_\sigma(X)$ exists.

Significance

The result. Theorem 4.2 characterises the sets of test probabilities for which the natural worst-case risk-adjusted value is computable by dynamic programming. Stability is thereby the structural condition behind time-consistent coherent risk measurement, recursive multiple-priors utility and backward-induction pricing under ambiguity. Without it, the worst-case value computed today may disagree with the value obtained by first computing tomorrow's worst case and then today's. The equivalence with the submartingale property says that stability is also exactly what makes $\Psi(X)$ the largest submartingale minorant of Theorem 4.1. Theorem 4.3 and the recursivity results for final values in Section 5 are corollaries.

Formalizing it. The paper's proof is complete apart from Lemma 4.1 and its Corollary, whose proofs are left to the reader. No machine-checked version of this result, of the generalized Snell envelope or of essential infima of families of random variables is known to exist. A formal proof would provide a reusable development of discrete-time optimal stopping under a set of probabilities, the essential-infimum calculus of Neveu, and density-martingale pasting — infrastructure that many results on robust optimal stopping, dynamic risk measures and robust Markov decision processes need.

Difficulty

The direction from stability to Bellman's principle needs an essential infimum to be exchanged with a conditional expectation under another probability (step (3) of the proof). This is false for a general family: an essential infimum of conditional expectations is not the conditional expectation of an essential infimum. The exchange works only because stability makes the family closed under minima (Lemma 4.1), so that it is directed downward and its essential infimum is the limit of a decreasing sequence, and because Lemma 3.1 lets the test probabilities used before and after $\tau$ be chosen independently. The converse, from the submartingale property to stability, is not a computation: it uses the separation theorem in $L^1$ against a pasted density assumed outside $\mathcal P$, which is where convexity and $L^1$-closedness of $\mathcal P$ are used. Dropping either hypothesis breaks that direction.

Formalization scope

Lean represents $\mathcal P$ by its set of densities in $\mathbb P_0$: $\mathcal F_N$-measurable, a.s. nonnegative, integrable, of mass one, convex, sequentially closed in the $L^1(\mathbb P_0)$ seminorm and saturated under a.s. equality. Test probabilities are $\mathbb Q_f=f\cdot\mathbb P_0$, and $\mathbb E_{\mathbb Q}[\cdot\mid\mathcal F_\sigma]$ is Mathlib's conditional expectation under $\mathbb Q_f$. Time is $\mathbb N$, and every stopping time is bounded by $N$. A $\mathbb Q$-submartingale on $0,\dots,N$ is Mathlib's Submartingale of the process frozen after $N$. The essential infimum of a family is defined in the mission (Mathlib has only that of a single function); a supporting item shows that it exists, so its fallback value is never used. All identities between risk-adjusted values hold $\mathbb P_0$-almost surely.

Conventions made explicit:

• the goal assumes that $\mathcal F_0$ is $\mathbb P_0$-trivial, which the proof uses when it treats $\Psi_0(X)$ as a number (without it, stability is not implied by (2)–(3));
• $\mathcal P^e\neq\emptyset$ replaces the paper's convenience assumption $\mathbb P_0\in\mathcal P$;
• $X_{-1}=0$;
• the Corollary's printed essential infimum over $\mathbb Q$ alone is read over $\mathbb Q$ and $\tau\ge\sigma$, as its right-hand side and its use require.

Bellman's principle must be stated with $\Psi$ on both sides and for all stopping times $\sigma\le\tau$. Replacing $\Psi$ by $\bar\Psi$, or restricting to deterministic times, turns the goal into a property of the recursion and is not the theorem.

Needed infrastructure, reusable beyond this mission: existence and directedness of essential infima of families; conditional expectations under equivalent measures and the Bayes formula; optional sampling for bounded stopping times under each $\mathbb Q$; the $L^1$–$L^\infty$ separation theorem. Contributions of any of these, and proofs of the milestones in any order, are welcome.

Selected references

• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, H. Ku, Coherent multiperiod risk adjusted values and Bellman's principle, Annals of Operations Research 152 (2007) 5–22. https://doi.org/10.1007/s10479-006-0132-6
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9 (1999) 203–228. https://doi.org/10.1111/1467-9965.00068
• L. G. Epstein, M. Schneider, Recursive multiple-priors, Journal of Economic Theory 113 (2003) 1–31. https://doi.org/10.1016/S0022-0531(03)00097-8
• F. Riedel, Dynamic coherent risk measures, Stochastic Processes and their Applications 112 (2004) 185–200. https://doi.org/10.1016/j.spa.2004.03.004
• P. Cheridito, F. Delbaen, M. Kupper, Coherent and convex monetary risk measures for bounded càdlàg processes, Stochastic Processes and their Applications 112 (2004) 1–22. https://doi.org/10.1016/j.spa.2004.01.009
• F. Delbaen, The structure of m-stable sets and in particular of the set of risk neutral measures, Séminaire de Probabilités XXXIX, Lecture Notes in Mathematics 1874 (2006) 215–258. https://doi.org/10.1007/978-3-540-35513-7_17
• J. Neveu, Discrete-Parameter Martingales, North-Holland, 1975 (French original: Martingales à temps discret, Masson, 1972).
• Y. S. Chow, H. Robbins, D. Siegmund, Great Expectations: The Theory of Optimal Stopping, Houghton Mifflin, 1971; Dover reprint, 1991.

Motivation

Every proof of the index theorem in Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), uses the fact that a bandit not being processed is frozen. Chapter 6 drops that: Whittle's restless bandits evolve under the passive action too, by a different law, and $m$ of $n$ must be active at every time. The problem is PSPACE-hard in general, so Whittle proposed a heuristic built from a Lagrangian relaxation: replace the hard constraint by a subsidy $W$ paid whenever a bandit is passive, solve the resulting single-bandit average-reward problem, and read off, for each state, the least subsidy $W(x)$ at which the passive action becomes optimal. When the set of states where passivity is optimal grows monotonically with $W$, the bandit is indexable and $W(x)$ is its Whittle index; the Whittle index policy activates the $m$ bandits of largest index. It reduces to the Gittins index policy when the passive action freezes, it is asymptotically optimal as $n$ grows under a fluid-stability condition (Weber and Weiss), and it has become the standard heuristic for sensor management, opportunistic channel access, maintenance and queueing control. The price is that indexability must be established model by model. Section 6.5 shows how easy this is when the single-bandit problem is solved by a monotone policy, on two bi-directional models: the spinning plates asset, which improves under investment and deteriorates when neglected, and the vigour bandit of Whittle's Ehrenfest project, which tires when worked and recovers when rested.

Setting

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

The spinning plates asset lives on $\{1, \dots, k\}$: active moves $x \to x + 1$ at rate $\lambda(x)$, passive moves $x \to x - 1$ at rate $\mu(x)$, $\lambda(k) = \mu(1) = 0$, and $r(x)$ is earned under both actions, $r$ increasing. Uniformized so that rates are at most one, it is a discrete-time bandit whose kernels move with the rate's probability and otherwise stay. The monotone policy $(y)$ is passive exactly on $\{x \ge y\}$; under it the asset alternates between $y - 1$ and $y$, spending the fraction $\phi(y) = \lambda(y-1)/(\lambda(y-1) + \mu(y))$ of its time at $y$, so its average reward is $W\phi(y) + R(y)$ with $R(y) = r(y)\phi(y) + r(y-1)(1 - \phi(y))$, and $W^*(x) = (R(x+1) - R(x))/(\phi(x) - \phi(x+1))$. The vigour bandit is the mirror image: active moves down at rate $\nu(x)$ and earns $r(x)$, passive moves up at rate $\rho(x)$ and earns nothing, $\psi(y) = \nu(y)/(\nu(y) + \rho(y-1))$, and $W^{**}(x) = (r(x)(1 - \psi(x)) - r(x+1)(1 - \psi(x+1)))/(\psi(x+1) - \psi(x))$.

Formalization targets

Goal: Theorem 6.4

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

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

Milestones

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

Significance

Theorem 6.4 is the chapter's template for proving indexability: the single-bandit value $g(W)$ is the upper envelope of finitely many lines $W\phi(y) + R(y)$ whose slopes decrease in the threshold, so the optimal threshold moves monotonically with the subsidy and the hinge points of the envelope are the indices. The same argument gives Theorem 6.5, the admission-control indices of Section 6.7, and the marginal productivity indices of Niño-Mora; it is the reason Whittle indices are computable in closed form for bi-directional models. Its formalization establishes, on the platform, the first restless-bandit model with a proved index, and the general notions of passive set, indexability and Whittle index that every later restless-bandit statement will use.

None of this is machine-checked. The average-reward optimality notion is stated without the DP equation (6.6), through optimality from every initial state, which is what the equation's solution encodes on a finite state space and avoids the relative value function altogether.

Difficulty

The proof in the book is two paragraphs, but it stands on the reduction to monotone policies, which is only sketched: every deterministic stationary policy, from every initial state, drives the asset into an absorbing endpoint or a two-state cycle $\{z - 1, z\}$ whose average reward is that of the monotone policy $(z)$, so no policy beats the best monotone one and the passive set under an optimal-from-everywhere policy is exactly $\{x \ge x(W)\}$ for the smallest maximizing threshold. Formalizing this needs the average reward of a finite Markov chain as a limit determined by the stationary distribution of the recurrent class reached, for the two-point kernels of the model, and a case analysis of policies as $\{0,1\}$-strings. The envelope argument then needs that the smallest maximizer of $\max_y [W\phi(y) + R(y)]$ is nonincreasing in $W$ when $\phi$ is strictly decreasing, and that with $W^*$ strictly decreasing the maximizer is $\le x$ exactly when $W \ge W^*(x)$. Theorem 6.5 is the same with the roles of up and down exchanged. Nothing in Mathlib computes Cesàro limits of finite Markov chains.

Formalization scope

Restless bandits are the two-action DecisionProcesses of the superprocess module; average reward is a real limsup of Cesàro means of Bochner integrals over the chain law of the Bandit Algorithms model under the stationary kernel; the optimal average reward is a supremum over the finite type of deterministic stationary Markov policies and the finite state space, bounded by the reward bound. Both models are on Fin k with the book's states shifted down by one, kernels driftKernel p f that move to f x with probability p x, and the boundary conventions of $\phi$ and $\psi$ (the book's "convenient positive values") replaced by their values $1, 0$ and $0, 1$ at the two extreme thresholds; the model assumptions $\lambda(k) = \mu(1) = 0$, $\nu(1) = \rho(k) = 0$, rates in $[0, 1]$, and $r$ increasing and nonnegative are hypotheses. Theorem 6.5's "increasing" is read as strictly increasing, as in Theorem 6.4, since a nonstrict $\psi$ admits zero interior rates for which the monotone reduction fails. The milestone (6.9) requires $k \ge 1$ and positive interior rates, which Theorem 6.4's hypothesis (i) implies.

Trivializing readings are excluded: indexability is monotonicity of the passive set over all real subsidies, the passive set is defined through policies optimal from every initial state, and the index identity is for every state. Welcome contributions: the average reward of a two-state cycle, the reduction of an arbitrary $\{0,1\}$-policy to a monotone one, and the envelope lemma for lines with decreasing slopes.

Selected references

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