Dynamic Programming

Motivation

Many sequential decision problems accumulate costs that are never recovered: inventory holding and shortage costs, waiting times, the expected number of steps until a target is reached. Written as rewards, these are non-positive rewards summed over an infinite horizon without discounting. Ralph Strauch's paper Negative Dynamic Programming (Ann. Math. Statist. 37 (1966), doi:10.1214/aoms/1177699369) is the foundational treatment of this negative case on general Borel state and action spaces. It complements Blackwell's treatment of the discounted case (Blackwell 1965) and of the positive bounded case (Blackwell 1964, mimeographed), and it sets out which conclusions of the discounted theory survive when rewards are non-positive and undiscounted.

A central question in that theory is how simple an optimal policy can be taken to be. A policy may in principle randomize and consult the entire past history. Strauch showed that in the negative case, whenever an optimal policy exists, an optimal stationary one exists, using one measurable decision rule at every stage. This mission formalizes that result together with the reduction from general policies to semi-Markov ones on which its proof rests.

Timeline. Blackwell (1965) proved that in the discounted case a stationary optimal policy exists whenever an optimal policy does, and gave an example showing that Markov policies need not suffice on Borel spaces. Strauch (1966) proved the corresponding statement for the negative case and proved that semi-Markov policies, which remember the initial state as well as the current one, are enough.

Setting

A negative dynamic programming problem consists of non-empty Borel sets $S$ (states) and $A$ (actions), a law of motion $q(\cdot\mid s,a)$, which is a probability kernel from $S\times A$ to $S$, and a Borel return function $r(s,a,t)$ with

$$r\le 0,\qquad r>-\infty,\qquad \int r(s,a,t)\,dq(t\mid s,a)>-\infty\ \ \text{for all }(s,a).$$

There is no discounting. A policy $\pi=(\pi_1,\pi_2,\dots)$ chooses the action $a_n$ at stage $n$ from a probability kernel $\pi_n(\cdot\mid h_n)$, where $h_n=(s_1,a_1,\dots,a_{n-1},s_n)$ is the history. A policy is Markov if $a_n=f_n(s_n)$ for Borel maps $f_n:S\to A$, semi-Markov if $a_n=g_n(s_1,s_n)$ for Borel $g_n$, and stationary, written $f^{(\infty)}$, if $a_n=f(s_n)$ for one Borel rule $f$. Random Markov and random semi-Markov policies draw $a_n$ from kernels in $s_n$, respectively $(s_1,s_n)$.

The expected total return from the initial state $s$ is

$$I(\pi)(s)=\sum_{n=1}^{\infty}\mathbb E^{\pi}_{s}\,r(s_n,a_n,s_{n+1})\in[-\infty,0],$$

the optimal return is $v^*(s)=\sup_\pi I(\pi)(s)$ over all policies, and $\pi^*$ is optimal if $I(\pi^*)(s)\ge v^*(s)$ for every $s$. For a Borel rule $f$, the operator $T$ acts on non-positive Borel functions $u$ by

$$Tu(s)=\int r(s,f(s),t)+u(t)\,dq(t\mid s,f(s)).$$

The namespace is NegativeDP.Stationary. The objects above are Problem, Plan, I, In, vstar, IsOptimal and T.

Formalization targets

Goal: Theorem 8.3 (negative case), p. 886

$$\big(\exists\,\pi^*\ \ I(\pi^*)\ge v^*\big)\ \Longrightarrow\ \exists\,f\ \text{Borel},\ \ I(f^{(\infty)})\ge v^* .$$

Milestones

1. Lemma 2.1: for a kernel $q(\cdot\mid x)$ and a Borel $u\le 0$ on $X\times Y$ there is a Borel $f$ with $u(x,f(x))\ge\int u(x,y)\,dq(y\mid x)$.
2. Lemma 3.1 (N): $I_n(\pi)\downarrow I(\pi)$.
3. Lemma 4.1 (a), (b): policies built from the conditional laws of $a_n$ given $(s_1,s_n)$, respectively given $s_n$ under an initial law $p$, reproduce the laws of $(s_1,s_n,a_n,s_{n+1})$, respectively the $p$-averaged laws of $(s_n,a_n,s_{n+1})$.
4. Theorem 4.1: for every policy $\pi$ and initial law $p$ there are a random semi-Markov $\pi^*$ and a random Markov $\pi^{**}$ with $I(\pi)=I(\pi^*)$ and $pI(\pi)=pI(\pi^{**})$ for every return function.
5. Theorem 4.2 (N): if $I(\pi^n\sigma)\ge I(\sigma)$ for all large $n$, then $I(\pi)\ge I(\sigma)$.
6. Theorem 4.3 (N): a semi-Markov $\tau$ with $I(\tau)\ge I(\pi)$ and a Markov $\sigma$ with $pI(\sigma)\ge pI(\pi)$.
7. Theorem 5.1 (N), parts (a)–(g): the properties of $T$, including $TI(\pi)=I(f,\pi)$, $TI(f^{(\infty)})=I(f^{(\infty)})=\lim_n T^n0$ and $I_n(\pi,v)=T_1\cdots T_nv$ for Markov $\pi$.

Significance

Theorem 8.3 reduces a search over all randomized, history-dependent policies to a search over single measurable decision rules, whenever an optimal policy exists at all. It underlies policy iteration and the stationary-policy conclusions of the later negative-programming literature, and it shows that the negative case behaves like the discounted case on this point. In the positive case only a weaker statement holds. The reduction of §4 (Theorems 4.1–4.3) is reused throughout the paper: Theorem 8.1 on $(p,\varepsilon)$-optimal Markov policies starts from Theorem 4.3, and the value-iteration results of §9 use Lemma 3.1 and Theorem 5.1.

All results in this mission are proved in the paper. None of them has a machine-checked proof that we know of. The closest formal result is part 2 of Bertsekas's Proposition 7, formalized in an abstract monotone-mapping model (MonotoneDP.Increase.prop7_optimal_stationary_criterion). There, policies are sequences of selectors, so it contains neither the measure-theoretic reduction from randomized history-dependent policies nor Borel state spaces. The formal work here is to build the law of the controlled process on Borel spaces, carry out the conditional-distribution argument of Theorem 4.1, and combine it with the operator calculus of §5.

Difficulty

The obvious argument starts from an optimal $\pi^*$, takes its first decision rule $f$, and shows that $f^{(\infty)}$ is optimal. That fails for a general $\pi^*$, because its first action may be randomized and its later actions may depend on the entire history. One first needs Theorem 4.3, which says a non-random semi-Markov policy is at least as good. That theorem needs two things. One is Theorem 4.1, which replaces a history-dependent policy by one built from conditional distributions of actions, and this requires disintegration of measures on Borel spaces. The other is the measurable selection of Lemma 2.1, which the paper takes from Theorem 2 of Blackwell and Ryll-Nardzewski 1963, applied stage by stage, with Theorem 4.2 to pass to the limit. On Borel spaces Markov policies are not enough (Blackwell's example, Example 4.1 of the paper), so the semi-Markov step cannot be skipped. Returns can equal $-\infty$, and every limit exchange has to respect that.

Formalization scope

Borel sets are non-empty standard Borel types and Baire functions are measurable functions. The return $r$ is real-valued, non-positive and integrable under $q(\cdot\mid s,a)$ for every $(s,a)$. Returns live in the extended reals. $I(\pi)$, $I_n(\pi,v)$, $T$ and all integrals of non-positive functions are computed as minus lower Lebesgue integrals of the corresponding losses in $[0,\infty]$, so a return of $-\infty$ is never collapsed to $0$. $I(\pi)$ is the sum of stage expectations, which equals the paper's expectation of the total return by monotone convergence. $v^*$ is the supremum over every randomized history-dependent plan. Restricting it to Markov or stationary policies would make the goal weaker, and that encoding is ruled out. Only the negative case ($r\le 0$, $\beta=1$) is formalized. Results the paper labels "D, P, N" or "D, N" appear here in their N form.

Explicit choices:

• Lean numbers decisions from $0$. Hist S A n is the paper's $H_{n+1}$ and the plan's kernel κ n is $\pi_{n+1}$.
• The objects $\pi^*$ and $\pi^{**}$ of Lemma 4.1 are defined in the paper's proof as conditional distributions. Here their defining property is a hypothesis: for every initial state, or after averaging over $p$, the joint law of $(s_n,a_n)$ is the law of $s_n$ followed by the kernel.
• In Theorem 4.1, "for any return function $r$" is a quantifier over every negative problem with the same law of motion, placed after the choice of $\pi^*$ and $\pi^{**}$.
• In Theorem 5.1 (b), $u+c$ is required to lie in $M(S)$. In (d), the increasing part holds only on $\{\sup_jTu_j>-\infty\}$.
• In Theorem 5.1 (f), $T$ is applied to $I(\pi)$ for a general plan with no measurability hypothesis. The lower integral is defined for every function.

Infrastructure needed: the law of the controlled process (built here by iterated kernel composition, as in the published DiscountedDP.Stationary model), disintegration of kernels on standard Borel spaces, a measurable selection theorem of Blackwell–Ryll-Nardzewski type, and monotone convergence for lower integrals. The disintegration and selection results are reusable well beyond this paper. Contributions to Theorems 4.1 and 4.3 are especially welcome, since missions II–IV of this series build on them.

Selected references

• R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4) (1966) 871–890. https://doi.org/10.1214/aoms/1177699369
• D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36(1) (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
• D. Blackwell and C. Ryll-Nardzewski, Non-existence of everywhere proper conditional distributions, Ann. Math. Statist. 34(1) (1963) 223–225. https://doi.org/10.1214/aoms/1177704259

Motivation

Q-learning is the basic model-free algorithm of reinforcement learning: an agent that does not know the transition probabilities or the reward structure of a controlled Markov process learns the optimal action values from experience alone, by a one-line update applied after every observed transition. It was introduced in C. J. C. H. Watkins' 1989 thesis, and the convergence theorem posed here is the one proved in C. J. C. H. Watkins and P. Dayan, Technical Note: Q-Learning, Machine Learning 8 (1992), 279–292 (doi:10.1023/A:1022676722315). Every later analysis of tabular temporal-difference control, and much of deep reinforcement learning's vocabulary, starts from this algorithm.

Timeline.

• 1989: Watkins' thesis introduces Q-learning and sketches a convergence argument.
• 1992: Watkins and Dayan publish the proof via the action-replay process, for bounded rewards, discount $0<\gamma<1$ and learning rates satisfying condition (3) at every state–action pair.
• 1994: Jaakkola, Jordan and Singh (Neural Computation 6) and Tsitsiklis (Machine Learning 16) give proofs through stochastic approximation for asynchronous iterations, with predictable random choices of state, action and step.
• Later work (Szepesvári 1997; Even-Dar and Mansour 2003) quantifies the convergence rate.

Setting

A finite controlled Markov process has a finite state set $X$, a finite nonempty action set $\mathfrak A$ (the same in every state), mean rewards $\mathcal R_x(a)$ and transition probabilities $P_{xy}[a]$. Rewards received $s$ steps later are discounted by $\gamma^s$ with $0<\gamma<1$. The optimal action-value function $Q^*$ is the unique solution of the Bellman optimality equation

$$Q^*(x,a)=\mathcal R_x(a)+\gamma\sum_y P_{xy}[a]\max_b Q^*(y,b).$$

In the $n$-th episode the agent observes a state $x_n$, performs an action $a_n$, observes the next state $y_n$ and a reward $r_n$ of mean $\mathcal R_{x_n}(a_n)$, and updates its table with a learning rate $\alpha_n$:

$$Q_n(x,a)=\begin{cases}(1-\alpha_n)Q_{n-1}(x,a)+\alpha_n\bigl[r_n+\gamma\max_b Q_{n-1}(y_n,b)\bigr]&(x,a)=(x_n,a_n),\\ Q_{n-1}(x,a)&\text{otherwise,}\end{cases}$$

from given initial values $Q_0$. Episodes need not form a single trajectory. Writing $n^i(x,a)$ for the episode of the $i$-th visit to $(x,a)$, the learning-rate condition is

$$\sum_{i=1}^\infty\alpha_{n^i(x,a)}=\infty,\qquad\sum_{i=1}^\infty\bigl[\alpha_{n^i(x,a)}\bigr]^2<\infty\qquad\forall x,a.\tag{3}$$

The proof uses the action-replay process (ARP): from the recorded episodes one builds a finite-horizon process with states $\langle x,n\rangle$ (a real state and a level $n$), in which taking $a$ at $\langle x,n\rangle$ replays a randomly chosen earlier episode that tried $a$ in $x$, emitting its reward and dropping to the level below that episode. Its expected one-step reward is $\mathcal R^{(n)}_x(a)$ and its aggregated transition probabilities are $P^{(n)}_{xy}[a]$.

Formalization targets

Goal: the Theorem (p. 282)

Given bounded rewards $|r_n|\le\mathcal R$, learning rates $0\le\alpha_n<1$ and (3),

$$Q_n(x,a)\to Q^*(x,a)\quad\text{as }n\to\infty,\ \forall x,a,\ \text{with probability }1.$$

Milestones (the paper's appendix, in attack order)

• Lemma A (p. 288): $Q_n(x,a)=Q^*_{\mathrm{ARP}}(\langle x,n\rangle,a)$ for all $a,x$ and $n\ge0$.
• Lemma B.1 (p. 289): the values of $s$ actions with and without a continuation policy differ by at most $\gamma^s\mathcal R/(1-\gamma)$.
• Lemma B.2 (p. 289): started high enough, the ARP strays below any level $l$ within $s$ actions with arbitrarily small probability.
• The stochastic-convergence theorem quoted in the proof of B.3 (p. 290): $X_{n+1}=X_n+\beta_n(\xi_n-X_n)$ with $\sum\beta_n=\infty$, $\sum\beta_n^2<\infty$ and bounded $\xi_n$ of mean $\Xi$ converges to $\Xi$ almost surely.
• Lemma B.3 (p. 290): almost surely $P^{(n)}_{xy}[a]\to P_{xy}[a]$ and $\mathcal R^{(n)}_x(a)\to\mathcal R_x(a)$.
• Lemma B.4 (p. 291): rewards within $\eta$ and transition rows within $\eta/\mathcal R$ give values of $s$ actions within $\eta s(s+1)/2$.

A further item states that the optimality equation has exactly one solution for $0\le\gamma<1$.

Significance

The result. The theorem is the first guarantee that an agent can find optimal behaviour in an unknown finite Markov decision process from samples, with a per-step cost independent of the model. It is the template for convergence results on SARSA, TD($\lambda$), double Q-learning and asynchronous value iteration, and it is the reference point against which finite-sample rates and function-approximation counterexamples are measured.

Formalizing it. The theorem has been proved since 1992–1994; this mission asks for a machine-checked proof. Two parts are reusable beyond Q-learning: the almost-sure convergence of scalar stochastic averaging with adapted steps (a Robbins–Siegmund type statement), and the perturbation bounds for finite-horizon values of Markov chains (B.1, B.4). The paper's own assembly in §3.2 bounds the error for each fixed action sequence and then passes to optimal behaviour; that passage is not justified on the page, so a complete development may route the final step differently. The milestones are the paper's lemmas as stated, with the corrections listed below.

Difficulty

The update touches one table entry at a time, at random times chosen by the agent, and its target $r_n+\gamma\max_b Q_{n-1}(y_n,b)$ depends on the current estimates, so the iteration is neither a plain average nor a contraction applied synchronously. Treating each entry as a separate Robbins–Monro average fails because the targets move with the other entries. The paper's device is to recognize $Q_n$ as exact optimal values of the ARP (Lemma A), which turns the analysis into showing that the ARP, viewed from a high level, behaves like the real process for many steps; the probabilistic content is then concentrated in Lemma B.3, and the deterministic content in B.1, B.2 and B.4.

Formalization scope

Everything lives in the namespace QLearning.Convergence, with one definitions module QLearning.Convergence.Setting. Conventions:

• $X$ and $\mathfrak A$ are Fintypes with decidable equality, $\mathfrak A$ is nonempty, and $\max_b$ is Finset.sup'. The process is a structure with R x a $=\mathcal R_x(a)$ and P x a y $=P_{xy}[a]$, rows nonnegative and summing to $1$.
• $Q^*$ enters the goal through the predicate IsOptimalQ M γ Q (the optimality equation), which has exactly one solution (separate item); it is not defined by a limit or a choice.
• Lean index $n$ is the paper's episode $n\ge1$; index $0$ of the episode data is unused and qIter … 0 $=Q_0$.
• Condition (3) is written over episodes: the learning rate charged to $(x,a)$ at episode $n$ is $\alpha_n$ if $(x_n,a_n)=(x,a)$ and $0$ otherwise; its partial sums tend to $+\infty$ and its squares are summable. This equals (3) and forces infinitely many visits.
• Probability model (pinned). The paper describes it in words only. On a filtered probability space, $x_n,a_n,\alpha_n$ are $\mathcal F_{n-1}$-measurable, $y_n,r_n$ are $\mathcal F_n$-measurable, $\Pr[y_n=y\mid\mathcal F_{n-1}]=P_{x_ny}[a_n]$, $\mathbb E[r_n\mid\mathcal F_{n-1}]=\mathcal R_{x_n}(a_n)$, $|r_n|\le\mathcal R$, $0\le\alpha_n<1$, and (3) holds almost surely. Fixed episode schedules with independent outcomes are a special case.
• The ARP deck at level $n$ includes card $n$ (as in the card game and Lemma A's proof); $P^{(n)}$ keeps the printed range of levels $1,\dots,n-1$; ARP optimality is over deterministic Markov policies of the ARP. Finite action sequences are lists of actions with $0$ terminal reward.
• Corrections disclosed in the items. B.1 is stated with $\le$ (the page's strict inequalities fail for a constant reward). B.4 assumes closeness of transition rows in $\ell^1$ and $s\ge1$: with the page's entrywise closeness the printed constant is false once $|X|\ge4$. The stochastic-convergence theorem is read with conditional mean $\Xi$ and adapted steps.

Trivializing formalizations are ruled out: the optimality predicate is satisfiable, conditional expectations are taken only of bounded measurable variables, the goal is the almost-sure statement under the probability model above rather than a pathwise or fixed-schedule one, and the ARP's optimal value is a supremum over policies, not the Q-learning recursion.

The development needs finite Markov chain values and contraction arguments (available in Mathlib in pieces), conditional expectations and almost-sure convergence for adapted sequences (Mathlib's martingale library), and the ARP construction above. Proofs of any milestone, alternative routes to the goal, and reusable lemmas on stochastic averaging are welcome. §4's extensions (absorbing undiscounted processes, multiple updates per episode) and equation (4) are not posed.

Selected references

• C. J. C. H. Watkins and P. Dayan, Technical Note: Q-Learning, Machine Learning 8 (1992), 279–292. https://doi.org/10.1023/A:1022676722315
• C. J. C. H. Watkins, Learning from Delayed Rewards, PhD thesis, University of Cambridge, 1989.
• T. Jaakkola, M. I. Jordan and S. P. Singh, On the Convergence of Stochastic Iterative Dynamic Programming Algorithms, Neural Computation 6 (1994), 1185–1201. https://doi.org/10.1162/neco.1994.6.6.1185
• J. N. Tsitsiklis, Asynchronous Stochastic Approximation and Q-Learning, Machine Learning 16 (1994), 185–202. https://doi.org/10.1007/BF00993306
• H. J. Kushner and D. S. Clark, Stochastic Approximation Methods for Constrained and Unconstrained Systems, Springer, 1978. https://doi.org/10.1007/978-1-4684-9352-8

Motivation

A firm that holds a single stock of a product often serves customers of different priority: military and civilian requisitions, contract and spot customers, emergency and routine orders for spare parts. When stock runs short, it must decide not only how much demand to satisfy but whose. Satisfying a low-priority order now may leave the firm unable to serve a high-priority order that arrives later in the same replenishment cycle. Inventory rationing asks for the optimal rule.

Veinott (Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13 (1965)) studied a model with $n$ demand classes, but fixed in advance the rule that a lower class is served only when every higher class has been served in full, and gave conditions on the costs under which that rule is optimal. Topkis (Management Science 15 (1968), 160–176) dropped the fixed rule and characterized the optimal rationing policy within a replenishment period. Theorem 1 of that paper is the target of this mission. It extends the author's earlier two-class analysis; the two-class case was later partly rediscovered by Evans and by Kaplan. Critical-level rationing policies of this kind are a standard object in the later literature on multi-class inventory systems.

Setting

A period between two replenishments is divided into $k$ intervals, indexed backwards: interval $t$ has $t-1$ intervals after it, so the period starts in interval $k$ and ends in interval $1$. Demand comes in classes $1,\dots,n$, with class $n$ the most important. At the start of interval $t$ the firm holds stock $z\ge0$ and faces the outstanding demand vector $B=(B^1,\dots,B^n)\ge0$: the backlog $b$ carried in plus the new demand $d_t$, whose law $\mu_t$ on $[0,\infty)^n$ has finite means. Demands of different intervals are independent.

The firm chooses the vector $u$ of demand left unsatisfied, with $0\le u\le B$, so that $w=z-\mathbf 1\cdot(B-u)\ge0$ units remain in stock, where $\mathbf 1\cdot y=\sum_j y^j$. It pays the penalty $p_t\cdot u$ and the holding cost $h_t(w)$. A fraction $a_t\ge0$ of the unsatisfied demand is carried into the next interval: $b_{t-1}=a_tu$, with $a_t=1$ meaning complete backlogging and $a_t=0$ lost sales. At the end of interval $1$ the salvage cost $v_1(z)+v_2(z-\mathbf 1\cdot b)$ is charged. The standing assumptions are:

• (A) $h_t$ is convex and continuous on $[0,\infty)$;
• (B) $v_1$ is convex and continuous on $[0,\infty)$, $v_2$ is convex and continuous on $\mathbb R$, and $D^+v_2$ is bounded below, where $D^+$ is the right derivative;
• (C) $0\le p_t^1\le\cdots\le p_t^n$.

The minimal expected cost $f_t$ of the last $t$ intervals and its expectation $g_t$ satisfy

$$f_t(z,B)=\inf_{\substack{0\le u\le B\\ w=z-\mathbf 1\cdot(B-u)\ge0}}\big[p_t\cdot u+h_t(w)+g_{t-1}(w,a_tu)\big],\qquad g_t(z,b)=\mathbb E\,f_t(z,b+d_t),$$

with $g_0(z,b)=v_1(z)+v_2(z-\mathbf 1\cdot b)$.

For a class $j$, with $\delta_j$ its unit vector, the critical rationing level $\bar z_t^j\in[0,+\infty]$ is $+\infty$ if $\varphi_t^j(w)=p_t^jw+h_t(w)+g_{t-1}(w,a_tw\delta_j)$ is strictly decreasing on $[0,\infty)$, and is the smallest minimizer of $\varphi_t^j$ on $[0,\infty)$ otherwise. With $B^{(j)}=\sum_{i\ge j}B^i$, the rationing level policy leaves unsatisfied

$$u^j=\big(B^{(j)}-z+\bar z_t^j\big)^+\wedge B^j .$$

In words: going down from class $n$, it serves as much of each class as it can without letting the stock fall below that class's critical level.

Formalization targets

Goal: Theorem 1

Suppose $a_i\in\{0,1\}$ for every $i\le t$. Then

1. the rationing level policy attains $f_t(z,B)$ for every $z\ge0$, $B\ge0$;
2. the critical levels are ordered as

$$\bar z_t^1\ge\bar z_t^2\ge\cdots\ge\bar z_t^n;$$

3. for $\varepsilon>0$, the differences $f_t(z,B)-f_t(z+\varepsilon,B+\varepsilon\delta_j)$ and $g_t(z,b)-g_t(z+\varepsilon,b+\varepsilon\delta_j)$ do not depend on $B^1,\dots,B^j$ and $b^1,\dots,b^j$.

Milestones

In attack order:

1. Lemma 1: the infimum of a convex function over one block of variables is convex.
2. Lemma 2: $g_t$ and $f_t$ are convex and continuous on the orthant, and the infimum in (1) is a minimum.
3. The critical levels exist, so they are well defined.
4. Lemma 3: moving $\varepsilon$ of demand from class $i$ to a less important class $j<i$ does not raise $f_t$ or $g_t$.
5. (6): $f_t(z,B)=\min_wf_t(w;z,B)$, where $f_t(w;z,B)$ is the cost of issuing exactly $z-w$ units.
6. Lemma 4: for each $w$, serving the classes in order of importance is optimal.
7. Corollary 1: some optimal $u$ never serves a class before every more important class has been served in full.

A companion item states the paper's remark that with a linear ordering cost $c(y)=c\cdot y$ the optimal order is $y(z)=(y(0)-z)^+$.

Significance

Theorem 1 reduces the $n$-dimensional rationing decision in each interval to $n$ numbers, which are computed from one-dimensional convex minimizations. Under complete or no backlogging this is the structural result that the rest of the paper builds on: the monotonicity of the levels in time (Theorem 2), the reduction of the backlog case to a single-interval problem (Theorem 3), and the multi-period ordering policy (Theorem 4). The hypothesis on $a_i$ is sharp in the sense the paper shows: for $a_2\in(0,1)$ an example on pp. 165–166 has no optimal policy of this form.

The theorem is proved in the paper, but no part of it is machine-checked. A formal development would contribute a reusable treatment of finite-horizon dynamic programs whose value function is defined by an infimum and an expectation over an orthant, with convexity and continuity propagated through the recursion. It would also contribute the comparative statics of critical-level policies.

Difficulty

The obvious argument proves optimality of the rationing level policy by induction from convexity alone. That is not enough. Convexity gives a one-dimensional problem in $w$ (by (6) and Lemma 4). But identifying its minimizer with the class-wise critical levels requires the marginal value of class-$j$ demand to be independent of the demand of the less important classes, which is part (c). Part (c) is false when $0<a_t<1$, so the induction must carry (a), (b) and (c) together and use $a_t\in\{0,1\}$ at every step. A second difficulty is analytic: $f_t$ is an infimum and $g_t$ an expectation, and before any structural argument starts the value functions must be shown to be finite, attained, continuous and integrable on the closed orthant (Lemma 2).

Formalization scope

• Representation. Classes are Fin n; the paper's class $j$ is index $j-1$, so class $n$ is the largest index and (b) is Antitone. Intervals are natural numbers counted backwards, as in the paper. Vectors are Fin n → ℝ with the pointwise order.
• Value functions. $f_t$ is defined by the recursion (1) itself, with a real infimum (sInf), and $g_t$ by a Bochner integral against $\mu_t$. Every statement about $f_t$, $g_t$ is restricted to $z\ge0$ and $B\ge0$ (or $b\ge0$). Lemma 2's attainment and integrability conjuncts are what identify these values with the paper's.
• Critical levels. The levels live in WithTop ℝ, with $\top=+\infty$. They are specified by the predicate IsCriticalLevel: strictly decreasing for $+\infty$, smallest minimizer otherwise. They are never computed by a real sInf, which would give the junk value $0$ when no minimizer exists.
• Standing assumptions. (A)–(C) are imposed for $1\le t\le k$. (B)'s limit condition is read as "$D^+v_2$ is bounded below". $D^+$ is an extended-real right Dini derivative. Assumption (D) on the ordering cost is not used.
• Added hypothesis. Lemma 1 adds the hypothesis that the function is bounded below on every fibre, because a real infimum cannot be $-\infty$.
• Not stated. The paper's remark that Assumption (D) ensures an optimal order $y(z)$ exists for a general continuous $c$ is not formalized. With $n=k=1$, $h_1(w)=w^2$, $c(w)=w-w^2$, $p_1=1$, $v_1=v_2=0$ and demand $1$ with certainty, (D) holds but $c(y)+g_1(y,0)=1-y$ for $y\ge1$, so no minimizer exists.
• Ruled out. Theorem 1 is not proved by assuming Lemma 2, the shape of the optimal vector, or the paper's derivative formulas (8)–(9). Those appear only as milestones or not at all. Part (a) asserts optimality over all feasible $u$, not among rationing level policies.
• Contributions welcome. Proofs of the milestones, general lemmas on convexity of partial infima and on continuity of parametric minima over polytopes, and integrability of functions of linear growth against laws with finite means.

Selected references

• D. M. Topkis, Optimal ordering and rationing policies in a nonstationary dynamic inventory model with n demand classes, Management Science 15(3) (1968), 160–176. https://doi.org/10.1287/mnsc.15.3.160
• A. F. Veinott, Jr., Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13(5) (1965), 761–778. https://doi.org/10.1287/opre.13.5.761
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (convexity of partial minima, Theorem 5.7). https://doi.org/10.1515/9781400873173

Motivation

A Markov decision process with the average cost criterion asks for a policy that minimizes the long-run expected cost per unit time. The criterion is the natural one for inventory, queueing and maintenance systems that run indefinitely without a meaningful discount rate, and it is the standard benchmark in the theory of controlled Markov chains (Arapostathis et al. 1993, Hernández-Lerma and Lasserre 1996). Unlike the discounted criterion, it has no contraction to work with, and an average-optimal policy may fail to exist.

The classical route to average optimality is the vanishing discount approach: solve the $\beta$-discounted problem, which is well behaved, and let $\beta \uparrow 1$. Schäl's paper gives conditions on a model with a general (Borel) state space under which this limit produces an average-optimal stationary policy.

Timeline. Taylor (1965) and Ross (1968) used the vanishing discount approach with equicontinuity via Arzelà–Ascoli. Sennott (1989) proved, for countable state spaces, that pointwise bounded relative discounted values yield an average cost optimality inequality and an average-optimal stationary policy. Schäl (1993, this mission) extended this to standard Borel state spaces under two alternative compactness–continuity conditions, (W) and (S). Later work, e.g. Feinberg, Kasyanov and Zadoianchuk (2012) and Feinberg and Liang (2022), weakened the compactness assumptions and studied when the inequality becomes an equation.

Setting

The model $(S, A, A(\cdot), q, c)$ consists of standard Borel spaces $S$ (states) and $A$ (actions); nonempty action sets $A(x) \subseteq A$ whose graph $\{(x, a) : a \in A(x)\}$ is measurable; a transition law $q(\cdot \mid x, a)$; and a measurable one-step cost $c(x, a) \in [0, \infty]$. A policy $\delta \in \Delta$ chooses, at each stage $n$, a randomized action that may depend on the whole history and lies in $A(x_n)$ with probability one. A stationary policy $f \in \mathbb F$ is a measurable $f : S \to A$ with $f(x) \in A(x)$.

For a policy $\delta$ and initial state $x$, $J^n(\delta, x)$ is the expected total cost of the first $n$ stages, and

$$\Phi(\delta, x) = \limsup_{n\to\infty} \tfrac1n J^n(\delta, x), \qquad g = \inf_{x \in S}\inf_{\delta \in \Delta} \Phi(\delta, x).$$

A policy is average optimal if $\Phi(\delta, x) = g$ for every $x$. The General Assumption is $g < \infty$.

For $0 < \beta < 1$, $J_\beta(\delta, x)$ is the expected total $\beta$-discounted cost, $v_\beta(x) = \inf_\delta J_\beta(\delta, x)$, $m_\beta = \inf_x v_\beta(x)$, and $w_\beta = v_\beta - m_\beta \ge 0$ is the relative discounted value function. The quantities $\bar g$ and $\underline g$ are the upper and lower limits of $(1-\beta)m_\beta$ as $\beta \uparrow 1$. Condition (B) requires $\sup_{\beta < 1} w_\beta(x) < \infty$ for each $x$.

Condition (W): $S$ is locally compact with countable base, the $A(x)$ are compact and $x \mapsto A(x)$ is upper semicontinuous, $q$ is weakly continuous on the graph of $A$, and $c$ is lower semicontinuous there. Condition (S): the $A(x)$ are compact, and for each fixed $x$, $a \mapsto q(\cdot \mid x, a)$ is setwise continuous and $a \mapsto c(x, a)$ is lower semicontinuous on $A(x)$.

Formalization targets

Goal: Theorem 3.8

Under the General Assumption, (B), and (W) or (S):

$$\exists f_1 \in \mathbb F:\ \Phi(f_1, x) = g \ \ \forall x \in S, \qquad g = \lim_{\beta\to1}(1-\beta)m_\beta = \lim_{\beta \to 1}(1-\beta)v_\beta(x)\ \ \forall x.$$

Moreover, for every sequence $\beta(k) \uparrow 1$ and every choice of $\beta(k)$-discount-optimal stationary policies $f_{\beta(k)}$, some average-optimal $f_1$ is a limit of them: under (W), $f_1(x) = \lim_m f_{\beta_m}(x_m)$ with $\beta_m$ from $\{\beta(k)\}$, $\beta_m \to 1$ and $x_m \to x$; under (S), $f_1(x) = \lim_m f_{\beta_m}(x)$.

Milestones

1. Lemma 1.2: $\limsup_{\beta\to1}(1-\beta)J_\beta(\delta, x) \le \Phi(\delta, x)$, and $\underline g \le \bar g \le g$.
2. Proposition 1.3: a finite measurable $\underline w \ge 0$ and $f_1 \in \mathbb F$ with $\underline w(x) + \underline g \ge c(x, f_1(x)) + \int \underline w\, dq(x, f_1(x))$ give $\Phi(f_1, \cdot) = g = \underline g = \bar g$.
3. Proposition 2.1 and (2.2): existence of discount-optimal stationary policies, the discounted optimality equation and its relative form.
4. Lemma 2.3: Fatou's lemma for setwise and for weakly converging measures.
5. (3.2), Lemmas 3.3, 3.4: the lower limit $\underline w(x) = \liminf_{k\to\infty, y\to x} w_{\beta(k)}(y)$ is attained along measurable sequences.
6. Proposition 3.5 and its (S) version (3.7): $\underline w$ and some $f_1$ satisfy the optimality inequality with $\underline g$.

Significance

The theorem gives existence of an average-optimal stationary policy on a general state space from checkable model conditions plus pointwise bounds on relative values, without assuming a solution of the average cost optimality equation. It also identifies the optimal average cost as the Abelian limit of discounted values, and says how to compute an optimal policy: as a limit of discount-optimal ones. §4 of the paper verifies (B) through entrance-time bounds and applies the theorem to Assaf's invariant problem and to a finite-capacity inventory model.

The result is a published theorem; none of it is machine-checked. Formalizing it requires the measure-theoretic layer of Borel dynamic programming (canonical path measures of history-dependent policies, discounted optimality equations, measurable selection of minimizers and of accumulation points) and Fatou lemmas for varying measures. These components are reusable for any Borel-space MDP. Related platform work: the Feinberg–Liang average-cost optimality equation under an additional equicontinuity assumption is posed separately (FeinbergLiang.ACOE.acoe_of_assumptionEC); it is a different theorem.

Difficulty

The naive argument takes a pointwise limit of $w_{\beta}$ as $\beta \to 1$ in the relative optimality equation (2.2). Under (B) the family $\{w_\beta(x)\}$ is only bounded pointwise, so no subsequence need converge, and even a pointwise lower limit loses the continuity needed to pass $\int w_\beta\, dq(x, f_\beta(x))$ to the limit when $q$ is only weakly continuous. The generalized lower limit $\underline w(x) = \liminf_{k, y\to x} w(k, y)$ repairs this, but then the limit has to be realized along measurably chosen states and indices, and the limiting actions must be selected measurably as accumulation points. The second obstacle is that only an inequality survives, with the constant $\underline g$; turning it into average optimality needs the Tauberian comparison of Lemma 1.2.

Formalization scope

The model reuses the published FeinbergLiang.ACOE.MDP (history-dependent randomized policies, the Ionescu-Tulcea path measure, $J^n$, $J_\beta$, $\Phi$) with its constant lower = 0, and a local definition file adds action sets, admissibility, $g$, $v_\beta$, $m_\beta$, $\bar g$, $\underline g$, $w_\beta$, $\underline w$ and Conditions (W), (S), (B). Committed conventions:

• All costs and values lie in $[0, \infty]$; $(1-\beta)$ is a nonnegative extended real, and $\beta \to 1$ means $\beta \uparrow 1$.
• Every infimum defining $g$ and $v_\beta$ runs over admissible policies only (actions in $A(x)$ almost surely); $q$ and $c$ are defined on $S \times A$, but only their values on the graph of $A$ enter.
• $w_\beta$ is a truncated difference, which equals $v_\beta - m_\beta$ because the General Assumption gives $m_\beta < \infty$. The General Assumption is an explicit hypothesis of every statement that involves $g$, $\underline g$, $\bar g$, $m_\beta$ or $w_\beta$.
• Upper semicontinuity of $A(\cdot)$ is Berge's. Condition (W)(0) is part of CondW: the topology on $S$ generates its σ-algebra and is locally compact, second countable and Hausdorff, hence metrizable; the metric $\rho$ of §3 is a metric-space instance. Under (S) no topology on $S$ is used, and the lower limit is $\liminf_k w_{\beta(k)}(x)$ (the discrete metric).
• (W)(1) prints "$A(x) \in \mathcal C(x)$", read as $\mathcal C(A)$. (3.2) prints $\inf_{k\ge n}\underline w_k(k, x)$, which is false in general; the subscript-$n$ version used in the proof of Lemma 3.4 is stated. "$\{\beta_m\} \subset \{\beta(k)\}$, $\beta_m \to 1$" is encoded as $\beta_m = \beta(k_m)$ with $k_m \to \infty$.
• Theorem 3.8's "$\{\beta(k)\}$ can be any sequence" is a universal quantifier over sequences and over choices of discount-optimal policies.

A formalization that assumes an average cost optimality inequality or equation, or that assumes the existence of the limit $\lim(1-\beta)m_\beta$, proves Proposition 1.3 rather than the goal; the goal derives the inequality from (W) or (S), (B) and the General Assumption alone. Contributions to the shared infrastructure (Markov property of the canonical process, measurable selection theorems such as Brown–Purves, Fatou lemmas for varying measures) are welcome as separate theorems. §4 of the paper (entrance-time bounds for (B)) is outside this mission.

Selected references

• M. Schäl, Average Optimality in Dynamic Programming with General State Space, Mathematics of Operations Research 18(1), 163–172, 1993. https://doi.org/10.1287/moor.18.1.163
• M. Schäl, Conditions for optimality in dynamic programming and for the limit of n-stage optimal policies to be optimal, Z. Wahrscheinlichkeitstheorie verw. Gebiete 32, 179–196, 1975. https://doi.org/10.1007/BF00532612
• 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
• R. F. Serfozo, Convergence of Lebesgue integrals with varying measures, Sankhyā Ser. A 44, 380–402, 1982.
• 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
• E. A. Feinberg, P. O. Kasyanov, N. V. Zadoianchuk, Average cost Markov decision processes with weakly continuous transition probabilities, Mathematics of Operations Research 37(4), 591–607, 2012. https://doi.org/10.1287/moor.1120.0555

Motivation

A controller observes a finite system period after period, chooses an action in each state, earns an income and moves the system at random. When future income is not discounted, the natural criterion is the average return per unit time (the gain), but many policies share the maximal gain while differing in their transient income. Blackwell (1962) showed that the policies that are optimal as the discount factor tends to one, the 1-optimal policies, are exactly the stationary policies that first maximize the gain and then, among those, the bias. He gave no finite procedure for the second maximization. Veinott (1966) supplied one: an extension of Howard's policy improvement method in which a second improvement test, on the bias, is run after the gain test is exhausted, with a third vector $z(f)$ guaranteeing termination. The method and its sensitivity hierarchy became the starting point of the $n$-discount optimality theory developed by Veinott (1969) and treated in Puterman's Markov Decision Processes (1994), Chapter 10.

Timeline:

• 1960: Howard, Dynamic Programming and Markov Processes: policy improvement for the discounted and the average-return problems.
• 1962: Blackwell, Discrete Dynamic Programming: existence of stationary policies optimal for all discount factors near one; the expansion $V_\beta(f^\infty)=x(f)/(1-\beta)+y(f)+o(1)$; nearly optimal (1-optimal) policies characterized by lexicographic maximization of $(x,y)$.
• 1966: Veinott, this paper: the extended policy improvement method that finds a 1-optimal stationary policy in finitely many steps (Theorem 6), and a finite-horizon characterization of the same policies (Theorem 7).
• 1969: Veinott, Discount optimality and sensitive optimality: the full hierarchy of $n$-discount optimal policies and the corresponding nested improvement method.

Setting

There are finitely many states $s$ and a finite set of actions. Choosing action $a$ in state $s$ earns the income $i(s,a)$ and moves the system to state $s'$ with probability $q(s'\mid s,a)$. A decision rule $f\in F$ picks an action $f(s)$ in each state; $r(f)$ is the vector with entries $i(s,f(s))$ and $Q(f)$ the stochastic matrix with entries $q(s'\mid s,f(s))$. A policy is a sequence $(f_1,f_2,\dots)$ of decision rules, $f^\infty=(f,f,\dots)$ is a stationary policy, and for $0\le\beta<1$

$$V_\beta(\pi)=\sum_{n=0}^\infty \beta^n Q(f_1)\cdots Q(f_n)\,r(f_{n+1})$$

is the vector of expected discounted returns. For vectors, $u\ge v$ is coordinatewise and $u>v$ means $u\ge v$ and $u\ne v$.

Let $Q^*(f)$ be the Cesàro limit of the powers of $Q(f)$. The gain $x(f)$ and the bias $y(f)$ are the unique solutions of

$$[I-Q(f)]x=0,\quad Q^*(f)x=Q^*(f)r(f);\qquad [I-Q(f)]y=r(f)-x(f),\quad Q^*(f)y=0,$$

and $z(f)$ is the unique solution of $[I-Q(f)]z=-y(f)$, $Q^*(f)z=0$. Write $F'$ for the decision rules of maximal gain and $F''\subset F'$ for those of maximal bias within $F'$.

The two improvement sets compare $f$ with a decision rule $g$ through the state-by-state tests

$$\text{(i) } [Q(g)x(f)]_s\ge[x(f)]_s,\qquad \text{(ii) } [r(g)+Q(g)y(f)]_s\ge[x(f)+y(f)]_s .$$

$G(f)$ consists of the $g$ for which (i) holds everywhere, (ii) holds wherever (i) is an equality, some inequality is strict, and $g(s)=f(s)$ wherever both are equalities. $E(f)$ consists of the $g$ for which (i) and (ii) are equalities at every state. For $g\in E(f)$,

$$\text{(iii) } [-y(f)+Q(g)z(f)]_s\ge[z(f)]_s,$$

and $H(f)$ consists of the $g\in E(f)$ for which (iii) holds everywhere, strictly somewhere, with $g(s)=f(s)$ wherever it is an equality.

Formalization targets

Goal: Theorem 6 (p. 1290)

For every $f\in F$:

1. $G(f)=\varnothing\ \Rightarrow\ f\in F'$;
2. $G(f)\cup H(f)=\varnothing\ \Rightarrow\ f\in F''$;
3. $g\in G(f)\ \Rightarrow\ x(g)>x(f)$, or $x(g)=x(f)$ and $y(g)>y(f)$;
4. $g\in H(f)\ \Rightarrow\ x(g)=x(f)$, and $y(g)>y(f)$, or $y(g)=y(f)$ and $z(g)>z(f)$.

Part 2 is the stopping certificate and parts 3 and 4 are the progress guarantee; together they say that the extended method raises $(x,y,z)$ lexicographically and stops at a decision rule in $F''$.

Milestones

• Theorem 3 (Blackwell): $V_\beta(f^\infty)=x(f)/(1-\beta)+y(f)+\epsilon(\beta,f)$ with $\epsilon(\beta,f)\to0$ as $\beta\to1^-$, and the unique-solution characterizations of $x(f)$, $y(f)$ (already posed on the platform, referenced).
• Lemma 1 (Blackwell): $g\in E(f)\Rightarrow x(g)=x(f)$, and $y(g)=y(f)$ if moreover $Q^*(g)Q^*(f)=Q^*(g)$ (referenced).
• Theorem 1: for fixed $0\le\beta<1$, exactly one of "$f^\infty$ has no one-step improvement and is $\beta$-optimal" and "some $g$ gives $V_\beta(g,f^\infty)>V_\beta(f^\infty)$ and $V_\beta(g^\infty)>V_\beta(f^\infty)$".
• Theorem 4: $F''$ is the nonempty set of $f$ with $f^\infty$ 1-optimal.
• Theorem 5 and Corollary 1: $G(f)=\varnothing\Rightarrow f\in F'$; $g\in G(f)\Rightarrow V_\beta(g^\infty)>V_\beta(f^\infty)$ for $\beta$ near one, hence the lexicographic increase of $(x,y)$.
• Lemma 4: for $g\in E(f)$, $y(g)=y(f)+w(g)$, where $w(g)$ is the unique solution of $[I-Q(g)]w=0$, $Q^*(g)w=Q^*(g)(-y(f))$.
• (12): $z(f)$ is the unique solution of its system.
• Lemma 5: $G(f)=\varnothing$ and $y(f)\ge y(g)$ for all $g\in E(f)$ imply $f\in F''$.
• Two steps of the proof of Theorem 6: $H(f)=\varnothing\Rightarrow y(g)\le y(f)$ on $E(f)$; and $g\in H(f)\Rightarrow w(g)>w(f)=0$, or $w(g)=w(f)=0$ and $z(g)>z(f)$.

Significance

Theorem 6 turns Blackwell's existence result into an algorithm. Blackwell's characterization requires maximizing the bias over $F'$, a set with no explicit description; Lemma 5 shows that maximizing over the explicitly available set $E(f)$ suffices, and Lemma 4 shows that this maximization has the same form as the original gain maximization, so the familiar policy improvement machinery applies a second time. The same mechanism, iterated, gives the $n$-discount optimal policies of the later sensitivity theory and the lexicographic policy improvement algorithms in standard texts.

The results are proved in the paper (with a correction to the proof of Lemma 5 credited to Bruce Miller). They are not formalized in any proof assistant known to the mission. A complete development yields machine-checked policy improvement for average and bias optimality on top of the published Blackwell model, including the convergence-free closed forms of gain, bias and $z$ and the facts about the limit matrix $Q^*$ and the deviation matrix they rest on.

Difficulty

Parts 1 and 3 are Blackwell's policy improvement for the gain, transported to Veinott's set $G(f)$. The new content is in parts 2 and 4, and in both the obvious argument fails at the same place: the bias of $g\in E(f)$ cannot be compared with the bias of $f$ by a state-by-state test in the original problem, because $E(f)$ is a product of action sets $E(s,f)$ different from the original ones, and Blackwell's comparison works only after a reduction to a problem in which the reward is $-y(f)$ and the role of the gain is played by $w(g)$. A second difficulty is Lemma 5: $E(f)$ may be a proper subset of $F'$ (Example 3 of the paper), so maximizing the bias over $E(f)$ does not obviously maximize it over $F'$. The certificate does not follow from the gain and bias tests at $f$ alone, and the paper's original proof of it contained an error (corrected, as the paper records, by Bruce Miller).

Formalization scope

Everything is built on the published Blackwell definitions (BlackwellDiscreteDP.NearOne.Model, LimitMatrix, GainBias): one finite action type available in every state (Veinott's $A_s$ are all equal to it), decision rules St → Act, policies indexed from $0$ (π 0 is $f_1$), real vectors St → ℝ with the pointwise order, and VecGt for the paper's $>$ (not coordinatewise strict). $Q^*(f)$ is the published Cesàro limit $\lim (N+1)^{-1}\sum_{i=0}^N Q(f)^i$, the same limit as Veinott's $N^{-1}\sum_{i=0}^{N-1}$. The gain and bias are the published closed forms $x(f)=Q^*(f)r(f)$ and $y(f)=H(f)r(f)$ with the deviation matrix $H(f)$; the new vectors are closed forms too: $w(g)=Q^*(g)(-y(f))$ and $z(f)=H(f)(-y(f))$, and their characterizations by (10) and (12) are milestones. 1-optimality is the published IsNearlyOptimal, which compares against every policy. Veinott's set $H(f)$ is HSet, to keep it apart from the deviation matrix Hf.

$G(f)$ and $H(f)$ are defined literally from the paper's inequalities, including the clauses "at least one strict" and "$g(s)=f(s)$ where the tests are equalities". Dropping either clause makes parts 3 and 4 false (a $g$ that only reshuffles ties would count as an improvement); replacing $F''$ or $G(f)$ by a set defined through the conclusion of the theorem would make the goal trivial. Neither is acceptable.

The reduction "replace $A_s$ by $E(s,f)$ and $r(g)$ by $-y(f)$" is not instantiated, since the published model has a single action set; its two uses in the proof of Theorem 6 are milestones stated in the original model. A development of the general model with state-dependent action sets, and of the limit-matrix identities $Q^*Q=QQ^*=Q^*Q^*=Q^*$, $(I-Q)H=I-Q^*$, $Q^*H=0$, would be reusable well beyond this mission. Proofs of any milestone are welcome, as is a proof of the published Theorem 3 and Lemma 1, on which most of the mission rests.

Selected references

• D. Blackwell, Discrete Dynamic Programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• A. F. Veinott, Jr., On Finding Optimal Policies in Discrete Dynamic Programming with No Discounting, Ann. Math. Statist. 37(5):1284–1294, 1966. https://doi.org/10.1214/aoms/1177699272
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• A. F. Veinott, Jr., Discount Optimality and Sensitive Optimality, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887