Dynamic Programming

Motivation

An inventory controller must decide how much to order while demand changes with an observed external condition. A single demand rate misses that dependence: the same inventory position can justify different orders when the condition changes. Song and Zipkin's 1993 study asks whether a simple policy remains optimal when the condition follows a continuous-time Markov chain and orders arrive after a random lead time. The answer for linear ordering costs is a world-dependent basestock policy: each world state has one target inventory position, and an order raises the current position to that target when it lies below it.

The policy claim concerns an infinite horizon. It is stronger than showing that a particular collection of target levels performs well or that such a policy minimizes a one-step cost. Theorem 2 of Song and Zipkin identifies the targets through a limiting value function and establishes optimality for the full discounted problem. This mission formalizes that theorem and the finite-stage results the authors use to state its limit precisely.

Setting

The world state $i$ belongs to a nonempty countable set $I$. The world evolves according to a conservative continuous-time Markov generator $Q=(q_{ij})$, with exit rate $q_i=-q_{ii}$. When the world is in state $i$, customers demand individual units at rate $\lambda_i\ge0$. The exit rates and demand rates are bounded above. Inventory is fully backlogged: a negative inventory level records unmet demand. The controller observes the world state and the inventory position $x\in\mathbb Z$, which includes outstanding orders, and chooses an order-up-to position $y\ge x$.

An order has actual unit cost $\bar c\ge0$ and may have fixed cost $\bar K\ge0$. This mission takes the linear-cost case, so the discounted fixed cost is $K=0$. The lead time $L$ is a finite nonnegative random time, independent of the world and demand process. Its Laplace transform discounts the ordering costs to $c=\bar c\,E[e^{-\alpha L}]$, where $\alpha>0$ is the discount rate. Holding one unit costs $h>0$ per unit time; backlogging one unit costs $p>0$.

Write $D_L^i$ for the number of demands during the lead time conditional on initial world state $i$. The cost rate of an inventory level $z$ is $\widehat C(z)=-pz$ for $z<0$ and $hz$ otherwise. The lead-time cost and myopic cost are

$$C(i,y)=E[e^{-\alpha L}\widehat C(y-D_L^i)],\qquad G^+(i,y)=(1-\gamma)cy+\beta C(i,y),$$

where $\mu>0$ is a uniformization rate at least $\sup_iq_i+\sup_i\lambda_i$, $\beta=(\mu+\alpha)^{-1}$, and $\gamma=\beta\mu$. The paper's Assumption 1, $\alpha\bar c<p$, applies to the later results. It ensures the myopic cost has finite nonnegative minimizers. The smallest such minimizer in world state $i$ is $y^+(i)$, and $y^+_{\min}=\min_i y^+(i)$.

With zero fixed cost and zero terminal cost, the $n$-stage transformed cost $W_n(i,x)$ minimizes the auxiliary cost $G_n(i,y)$ over $y\ge x$. Each $G_n$ combines the myopic cost with the expected discounted continuation after a demand, a world-state jump, or a self-loop. Let $W_\infty$ and $G_\infty$ denote their pointwise limits. A basestock policy $\pi(y)$ orders to $\max\{x,y(i)\}$ in state $(i,x)$; it never cancels an outstanding order.

Formalization targets

The main target is the finite, smallest global minimizer $y^*(i)$ of $G_\infty(i,\cdot)$ for each world state, with the inequalities of Theorem 2(c):

$$0\le y^+_{\min}\le y^*(i)\le y^*_\infty(i)\le y^+(i), \qquad G_\infty(i,y^*_\infty(i))=\min_{z\in\mathbb Z}G_\infty(i,z).$$

Here $y^*_\infty(i)$ is the limit of the smallest finite-stage minimizers $y^*_n(i)$. Theorem 2(e) then asserts that $\pi(y^*)$ has minimum infinite-horizon expected discounted cost from every state among all feasible policies. The milestone list states Lemmas 1, 2 and 4, Corollaries 1 and 2, all parts of Theorem 1 as identified by the paper's internal references, and the limit and optimality-equation clauses of Theorem 2. Together they fix the finite-stage and limiting objects used by the goal.

Significance

The theorem reduces a decision at every integer inventory position to one integer target for each observed world state. It gives an exact policy structure for a model with a changing demand rate and random lead time, rather than an approximation derived from a constant-demand model. The limiting inequalities also locate an optimal target relative to the myopic target and the finite-stage targets, giving a mathematically specified range for policy computation. These claims are the linear-cost part of Song and Zipkin's analysis; the paper proves the result but supplies no Lean proof.

Formalization will leave reusable definitions for countable-state uniformization with a demand counter, integer convexity of inventory cost functions, and discounted costs of history-dependent policies. The mission's theorem statements compile as open goals. The remaining work is to verify the analytic properties of the lead-time demand law, the finite-stage inequalities, convergence, and the infinite-horizon policy comparison. The fixed-order-cost and monotone-world-state results of the paper are separate missions.

Difficulty

The world can have countably many states, so a continuation value includes a series over possible world jumps. The stage cost grows with inventory position, so a bounded-cost finite-state dynamic-programming theorem does not directly cover the model. The minimization is over an unbounded set of integers, and the minimizers themselves change with the stage number. Convexity of a one-stage cost alone does not establish that the limiting policy beats policies that use the entire observation history. These are the specific gaps the paper's bound, ordered-difference, and limit results address.

Formalization scope

World states are a nonempty countable Lean type, inventory positions and order-up-to levels are integers, and costs are real until policy evaluation. The lead-time law is a probability measure on finite nonnegative real times, independent of world and demand. The demand-count law is defined by exact Poisson uniformization at rate $\mu$, with demand, world-jump, and self-loop branches. The infinite-horizon policy cost uses extended nonnegative reals and a supremum of finite-horizon costs, so it can express an infinite expected cost without a default real value. Policies may depend on all past observed states; the goal compares its basestock policy against every feasible deterministic policy in this class. Randomized policies are omitted because they cannot improve expected nonnegative costs on this countable state space.

Assumption 1 is attached only to the results that use it. The linear-cost recursion has $K=0$ and $W_0=0$. Integer convexity means nondecreasing forward differences. Smallest minimizers and the minimum across world states are asserted to exist; neither is encoded by an integer infimum that returns a default on an empty or unbounded set. The goal requires an actual optimal policy cost comparison from every state, so solving the limiting optimality equation only within basestock policies cannot close it. Contributions to the lead-time mixture, integer convexity, boundedness of the real series and infima, and unrestricted policy comparison all fit this scope.

Selected references

• Jing-Sheng Song and Paul Zipkin, Inventory Control in a Fluctuating Demand Environment, Operations Research 41(2):351–370, 1993. DOI 10.1287/opre.41.2.351.

Motivation

A Markov decision process is the standard model of sequential decision making under uncertainty: a controller observes the state of a finite system, chooses a decision, pays a cost, and the system moves to a random next state. In many applications (maintenance, inventory with unreliable records, robotics, medical treatment) the controller does not see the state itself, only partial information about it. This is the partially observed problem, and the usual way to solve it is to replace the state by the conditional distribution of the state given the observations (Åström 1965; Bertsekas). That reformulation has an infinite state space, and Smallwood and Sondik (1973) showed that the finite-horizon cost-to-go is nevertheless piecewise linear, but with a number of pieces that may grow exponentially with the horizon.

Papadimitriou and Tsitsiklis (Math. Oper. Res. 12(3), 1987) asked whether this blow-up is an artefact of the reformulation or intrinsic to the problem. Their Theorem 6 answers it: deciding whether a partially observed process can achieve a given expected cost is PSPACE-hard, already for stationary processes and horizons shorter than the number of states. This mission formalizes the reduction behind that theorem.

Setting

A partially observed stationary Markov decision process has a finite state set $S$, a partition $\Pi$ of $S$, and an initial state $s_0$. For a state $s$ write $z(s) \in \Pi$ for the set containing it. Each set $z$ carries a nonempty finite set $D_z$ of decisions; decision $i \in D_z$ costs $c(z, i)$ and moves a current state $s \in z$ to the next state $s'$ with probability $p(s, s', i)$. The controller sees only the sequence of sets visited, so a policy $\pi$ maps each observation sequence $z_0, \dots, z_t$ to a decision in $D_{z_t}$. For a horizon $T$, the expected cost of $\pi$ is

$$J_\pi(T) = \mathbb{E}_\pi\Bigl[\sum_{t=0}^{T} c\bigl(z(s_t), \pi(z(s_0), \dots, z(s_t))\bigr)\Bigr],$$

and the optimal cost is $\inf_\pi J_\pi(T)$.

A quantified Boolean formula is $Q_1 x_1 \cdots Q_n x_n\, F(x_1, \dots, x_n)$ with each $Q_j \in \{\exists, \forall\}$ and $F$ a conjunction of $m$ clauses $C_1, \dots, C_m$, each a set of literals $x_j$ or $\neg x_j$. It is true if there is a value of $x_1$ such that for all values of $x_2$, and so on, $F$ comes out true. Deciding truth (QSAT) is PSPACE-complete (Stockmeyer and Meyer 1973).

From a formula with $m \ge 1$ clauses the paper builds a process $M_\varphi$: an initial state, six states $A_{ij}, A'_{ij}, T_{ij}, T'_{ij}, F_{ij}, F'_{ij}$ per clause $i$ and variable $j$, end states $A_{i,n+1}, A'_{i,n+1}$, and one absorbing state, so $|S| = 6mn + 2m + 2$. The first transition chooses a clause uniformly; primed states record that the chosen clause is not yet satisfied; existential variables are set by decisions and universal ones by fair coins; the only nonzero cost, $1$, is paid at $A'_{i,n+1}$. The horizon is $T = 2n + 2$.

Formalization targets

Goal: the reduction is correct

For every formula $\varphi$ in the paper's QSAT class (an alternating prefix beginning with $\exists x_1$ and ending with $\forall x_n$, and three literals per clause), with $m \ge 1$ clauses and $T = 2n+2$,

$$T < |S|, \qquad \bigl(\exists \pi:\ J_\pi(T) = 0\bigr) \iff \varphi \text{ is true}, \qquad \inf_\pi J_\pi(T) \le 0 \iff \varphi \text{ is true}.$$

The goal states all three claims the paper makes: the horizon bound (p. 448), the existence of a zero-cost policy (p. 449), and the bound on the optimum (p. 448).

Milestones

1. The cost splits over the clause chosen at time 1: each clause is chosen with probability $1/m$, and a policy has zero expected cost iff it has zero cost for every choice of clause.
2. If a trajectory of positive probability ends in $A'_{i,n+1}$, the expected cost is at least $2^{-n}/m$.
3. A zero-cost policy makes the formula true.
4. A true formula yields a zero-cost policy.

Significance

Theorem 6 locates the partially observed finite-horizon problem in the complexity landscape: unless P = PSPACE there is no polynomial-time algorithm for it, even for stationary processes with short horizons. The paper's Corollary 1 strengthens this into evidence that no polynomial-size precomputed controller exists either. Together these results explain why exact algorithms for partially observed processes are exponential and motivated the later work on approximation and on restricted policy classes.

The formalization adds a machine-checked proof of the correctness of the reduction, the step on which the hardness claim rests, together with a reusable definition of a finite partially observed process with observation-history policies and of quantified Boolean formulas. The paper's argument is a short paragraph; a formal proof has to make precise how a policy that only sees observation sequences determines a strategy for the existential player. As far as we know, no machine-checked proof of this reduction exists.

Difficulty

The "if" direction is a direct translation of a winning strategy into a policy. The "only if" direction is where the work is. A zero-cost policy acts on observation sequences, and the paper argues that it never learns which clause was chosen. Under the paper's own partition this is not literally true: the sets $T_j$ and $T'_j$ differ, so the observations reveal whether the chosen clause was already satisfied. The existential strategy must therefore be extracted from the policy's behaviour on the observation histories in which the clause is still unsatisfied, and one must check that it is a single strategy, independent of the clause, that satisfies every clause against every choice of the universal variables. The bound of milestone 2 also requires tracking the probability of a single trajectory through the coin flips.

Formalization scope

The process is a Lean structure POMDP S Z with an observation map obs : S → Z encoding the partition, nonempty finite decision types D z, real costs c z i, and next-state laws given as Mathlib PMFs, so every transition row is a probability vector. A policy is a function List Z → (z : Z) → D z of the earlier observations and the current one. The expected cost is a finite sum over trajectories $x_0, \dots, x_T$ of their probability times $\sum_{t=0}^{T} c$, and the optimum is the infimum over all policies. Paper clause $C_i$ and variable $x_j$ are Lean indices $i - 1$ and $j - 1$.

Choices made explicit:

• Horizon. The paper prints $T = 2m + 2$ but says it is "just enough time for the process to reach one of $A_{i,n+1}$ or $A'_{i,n+1}$", which happens at time $2n+1$. With the printed value and $m < n$ the cost is never paid and every formula would map to a zero-cost process. We use $T = 2n+2$.
• The set $A_j$. The partition sentence puts all $A_{ij}$ and $A'_{ij}$ in one set $A_j$; the decision sentence mentions "the set $A'_j$". We follow the partition sentence.
• The new state reached from $A_{i,n+1}$ and $A'_{i,n+1}$ is unspecified; it gets its own set, one zero-cost decision and a self-loop.
• Formulas. The general QBF definition allows any quantifier prefix and clause width. Every theorem assumes IsPaperQSAT, which requires the paper's alternating prefix $\exists x_1 \forall x_2 \cdots \forall x_n$ with $n>0$ even and three literals per clause. Clauses are sets of literals; three witnesses allow repetitions. $m \ge 1$ is also a hypothesis.
• Decisions are nonempty; rows are probability vectors.

Policies see only observation sequences. A formalization in which the policy reads the state would make the "only if" direction false and the reduction meaningless; one in which it sees only the current observation would make the "if" direction false. Neither is admissible.

Not formalized: PSPACE-hardness itself (Mathlib has no PSPACE or polynomial-time reductions), the polynomial-time computability of the construction, the membership of the problem in PSPACE (sketched on p. 449), Corollary 1 (a $\Sigma_2^p$ collapse) and Corollary 2 (NP-completeness of the unobserved case, stated without proof).

The definitions of partially observed processes and quantified Boolean formulas are reusable. Contributions of lemmas on trajectory sums (marginalising later coordinates, the probability of a fixed prefix) are welcome; they also serve the other missions of this series.

Selected references

• C. H. Papadimitriou and J. N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 1987, 441–450. https://doi.org/10.1287/moor.12.3.441
• L. J. Stockmeyer and A. R. Meyer, Word problems requiring exponential time, Proc. 5th ACM STOC, 1973, 1–9. https://doi.org/10.1145/800125.804029
• R. D. Smallwood and E. J. Sondik, The optimal control of partially observable Markov processes over a finite horizon, Operations Research 21(5), 1973, 1071–1088. https://doi.org/10.1287/opre.21.5.1071
• K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10, 1965, 174–205. https://doi.org/10.1016/0022-247X(65)90154-X
• D. P. Bertsekas, Dynamic Programming: Deterministic and Stochastic Models, Prentice-Hall, 1987.

Motivation

Controlled Markov processes with the average cost criterion model systems that run indefinitely, such as queues, inventories, maintenance and communication networks, where only the long-run cost per unit time matters. The standard route to an optimal stationary policy goes through the average cost optimality equation (ACOE). The ACOE is usually obtained by the vanishing discount method: solve the discounted problem for each discount factor $\beta<1$ and let $\beta\to1$. The method works only when the differences of discounted values stay bounded as $\beta\to1$. Conditions that guarantee this are therefore central in the survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993), §5).

This mission formalizes one such condition, due to Ross: if the mean return time to a fixed state is bounded uniformly over all stationary policies and initial states, the differential discounted value functions are bounded uniformly in the discount factor and the state.

Timeline. Derman (Management Sci. 9 (1962); survey reference [38]) and Derman–Veinott (Ann. Math. Statist. 38 (1967); survey reference [43]) introduced recurrence conditions of this kind for countable-state processes. Ross (Ann. Math. Statist. 39 (1968), survey reference [147]; Introduction to Stochastic Dynamic Programming, 1983, survey reference [150]) showed, for bounded costs, that under a Derman–Veinott type recurrence condition $h_\beta$ is bounded uniformly in $\beta$, and obtained a bounded solution of the ACOE by letting $\beta\uparrow1$ (survey, pp. 291 and 301). Later work replaced the condition with weaker ones (survey Assumptions 5.1–5.3) and with Sennott's conditions (survey Theorem 5.9).

Setting

The state space is $S=\{0,1,2,\dots\}$. In each state $i$, an action $a$ is chosen from a nonempty compact set $U(i)$ of a metric space $A$. The one-stage cost $c(i,a)$ is nonnegative and the next state is drawn from the transition law $P(\cdot\mid i,a)$. For fixed $i,j$, the maps $a\mapsto c(i,a)$ and $a\mapsto P(j\mid i,a)$ are continuous on $U(i)$. A policy $\pi\in\Pi$ chooses the action at time $t$ at random, given the whole history, and must choose from $U(X_t)$. A stationary deterministic policy $f\in\Pi_{SD}$ is a map $f:S\to A$ with $f(i)\in U(i)$. $P^\pi_i$ and $E^\pi_i$ denote the law and the expectation of the controlled process $(X_t,A_t)$ started at $i$.

For a discount factor $\beta\in(0,1)$, the discounted cost and the optimal discounted cost are

$$J_\beta(i,\pi)=E^\pi_i\Big[\sum_{t=0}^\infty\beta^t c(X_t,A_t)\Big],\qquad J^*_\beta(i)=\inf_{\pi\in\Pi}J_\beta(i,\pi).$$

A policy $f\in\Pi_{SD}$ is $\beta$-discount optimal if $J_\beta(i,f)=J^*_\beta(i)$ for all $i$. The differential discounted value function is

$$h_\beta(i)=J^*_\beta(i)-J^*_\beta(0),$$

measured relative to the fixed state $0$. The return time to $0$ is

$$\tau=\min\{t\ge1:\ X_t=0\},$$

with $\tau=\infty$ if the process never returns. Throughout, as in §5.1 of the survey, the cost is bounded: $c(i,a)\le M$ on admissible pairs.

Formalization targets

Goal: Theorem 5.3

If there is a constant $K>0$ with

$$E^f_i[\tau]<K\qquad\text{for all } f\in\Pi_{SD},\ i\in S, \tag{5.7}$$

then there is a constant $B$ such that

$$|h_\beta(i)|\le B\qquad\text{for all }\beta\in(0,1),\ i\in S.$$

This is the theorem as printed: it asserts only uniform boundedness and fixes no constant.

Milestones

1. Theorem 2.1 (iii): for every $\beta\in(0,1)$, a $\beta$-discount optimal $f_\beta\in\Pi_{SD}$ exists.
2. (5.8): for such an $f_\beta$, $J^*_\beta(i)\le M\,E^{f_\beta}_i[\tau]+J^*_\beta(0)\,E^{f_\beta}_i[\beta^\tau]$.
3. (5.9): $J^*_\beta(i)-\beta J^*_\beta(0)\le MK$.
4. Jensen step: $J^*_\beta(i)\ge J^*_\beta(0)\,E^{f_\beta}_i[\beta^\tau]\ge J^*_\beta(0)\,\beta^K$.
5. (5.10): $J^*_\beta(0)-J^*_\beta(i)\le(1-\beta^K)J^*_\beta(0)\le(1-\beta^K)\frac{M}{1-\beta}\le MK$.
6. Explicit bound: $|h_\beta(i)|\le MK$. This is stronger than the goal and is the constant the survey's argument yields.

Significance

The result. Theorem 5.3 verifies the hypothesis of the vanishing discount theorem (Theorem 5.2 of the survey) from a condition on the uncontrolled dynamics of stationary policies. Theorem 5.2 then gives a bounded solution $(\rho,h)$ of the ACOE, an average optimal stationary policy, and the limit $\lim_{\beta\to1}(1-\beta)J^*_\beta(i)=\rho$. Mean return times can often be estimated directly, for instance through Foster–Lyapunov drift arguments on queues, which makes (5.7) checkable in applications. The explicit bound $MK$ also controls the span of the relative value function.

Formalizing it. The result is proved in the literature; to our knowledge it has not been machine-checked. A formal proof needs discounted dynamic programming on a countable state space with compact action sets, the existence of optimal stationary policies (Theorem 2.1 (iii), which the survey cites without proof), and the strong Markov property of the controlled chain at a return time. All of these are reusable well beyond this mission.

Difficulty

The estimates (5.9) and (5.10) are elementary once (5.8) and the existence of $f_\beta$ are available. The weight lies elsewhere.

• Optimal stationary policies. The infimum defining $J^*_\beta$ ranges over all history-dependent randomized policies. Bringing it down to a single stationary deterministic policy requires the discounted optimality equation, a measurable selection of minimizers on compact action sets, and a verification argument against arbitrary policies.
• Restarting at $\tau$. (5.8) splits the discounted cost at the random time $\tau$. The tail must be identified with $\beta^\tau$ times the discounted cost from state $0$. This is the strong Markov property for the process built by the Ionescu-Tulcea theorem, applied at a stopping time that may be infinite.

Formalization scope

• The state space is ℕ; the action space is a metric space with its Borel $\sigma$-algebra. The model CMP carries compact nonempty $U(i)$, a nonnegative measurable cost, and continuity of $c(i,\cdot)$ and $P(j\mid i,\cdot)$ on $U(i)$, the standing assumptions of §5.
• Policies are history-dependent, randomized and admissible. The path measure is Mathlib's Kernel.trajMeasure. $J^*_\beta$ is an infimum over all such policies, not over Markov or stationary policies only.
• Costs are lower Lebesgue integrals in $[0,\infty]$. $h_\beta$ is the difference of the real parts of $J^*_\beta(i)$ and $J^*_\beta(0)$. This is exact here because bounded cost gives $J^*_\beta\le M/(1-\beta)<\infty$.
• Explicit choices:
  • The bounded-cost hypothesis $c\le M$ on admissible pairs is a binder of every §5.1 statement. It is the section's standing assumption, and without it the theorem is false.
  • $\tau$ counts from $t\ge1$ and takes values in $\mathbb N\cup\{\infty\}$, so (5.7) applies from $i=0$ and forces $\tau<\infty$ almost surely; $\beta^\tau=0$ on $\{\tau=\infty\}$.
  • The typo $\beta^n$ in (5.8) is read as $\beta^t$.
  • $K\ge1$ in (5.10) is not assumed; it follows from (5.7).
• Theorem 2.1 is stated in the survey for Borel models under Assumptions 2.1–2.3. Here it is posed in the countable model, where those assumptions follow from the §5 continuity and compactness assumptions.
• The goal's bound $B$ is quantified before $\beta$ and $i$. A per-$\beta$ or per-state bound would be trivial, since every $h_\beta(i)$ is a finite number.
• Welcome contributions include discounted dynamic programming on countable state spaces, the strong Markov property for trajMeasure, and return-time estimates.

Selected references

• 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) (1993) 282–344. https://doi.org/10.1137/0331018
• C. Derman, On sequential decisions and Markov chains, Management Sci. 9 (1962) 16–24. https://doi.org/10.1287/mnsc.9.1.16
• C. Derman, A. F. Veinott Jr., A solution to a countable system of equations arising in Markovian decision processes, Ann. Math. Statist. 38 (1967) 582–584 (cited as [43] in the survey, https://doi.org/10.1137/0331018).
• S. M. Ross, Non-discounted denumerable Markovian decision models, Ann. Math. Statist. 39 (1968) 412–423 (cited as [147] in the survey, https://doi.org/10.1137/0331018).
• S. M. Ross, Introduction to Stochastic Dynamic Programming, Academic Press, 1983 (cited as [150] in the survey, https://doi.org/10.1137/0331018).

Why average cost is a control problem

A controller acting over an indefinite horizon must decide whether a lower cost today is worth a higher cost later. Average cost measures the expected expenditure per stage as the horizon grows. It is appropriate when operation has no natural terminal date, but its limiting definition makes it difficult to compute an optimal policy directly. Discounted cost assigns less weight to distant stages and has a more direct optimality equation. Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus survey these criteria for controlled Markov processes and state a condition under which solving one discounted problem yields a solution to an average-cost problem (Arapostathis et al., 1993, §5.1).

The condition is a common lower bound on the one-step probability of moving to a distinguished state. Ross's reduction, reported as Theorem 5.6 of the survey, uses that bound to define a new transition law and a specific discount factor. The survey's theorem states the reduction informally; its proof specifies the transformed law, the optimality equation and the resulting average-cost policy. Those claims are the targets of this mission (Arapostathis et al., 1993, pp. 303–304).

Controlled process and criteria

The state space is $S=\{0,1,2,\ldots\}$. In state $i$, the controller may choose an action $a$ from a nonempty compact set $U(i)$ in a metric action space. Choosing $a$ incurs the one-stage cost $c(i,a)\ge0$ and moves the state to $j$ with probability $P(j\mid i,a)$. The cost is measurable, and for each fixed $i,j$ its value and $P(j\mid i,a)$ vary continuously with $a$ on $U(i)$. Section 5 imposes these state and continuity conventions; §5.1 additionally assumes the costs are bounded (Arapostathis et al., 1993, pp. 284–288, 299, 301).

An admissible policy $\pi$ chooses a probability law for the next action from the entire observed history, and assigns probability one to admissible actions. A stationary deterministic policy is a map $f$ with $f(i)\in U(i)$; it always takes action $f(i)$ in state $i$. These are distinct classes. Let $J_N(i,\pi)$ be expected cost over the first $N$ stages from $i$, and let $J_\beta(i,\pi)$ be expected cost when stage $t$ is weighted by $\beta^t$, where $0<\beta<1$. The average-cost criterion is $J(i,\pi)=\limsup_{N\to\infty}J_N(i,\pi)/N$. The optimal values $J^*(i)$ and $J_\beta^*(i)$ are infima over all admissible policies, including randomized and history-dependent ones (Arapostathis et al., 1993, pp. 285–287).

The average cost optimality equation, or ACOE, asks for a scalar $\rho$ and a real function $h$ such that, for each state $i$,

$$\rho+h(i)=\min_{a\in U(i)}\left\{c(i,a)+\sum_{j\in S}P(j\mid i,a)h(j)\right\}.$$

The minimum is attained. The survey's verification theorem identifies $\rho$ with the optimal average cost when the terminal contribution of $h(X_t)$ vanishes after division by $t$ (Arapostathis et al., 1993, p. 299, (5.1), Theorem 5.1).

Formalization targets

The reduction

Assume that $P(0\mid i,a)\ge\alpha$ on every admissible state-action pair for a single constant $0<\alpha<1$. The transformed process $\widetilde M$ has the same admissible actions and costs and has transition probabilities

$$\widetilde P(j\mid i,a)=\frac{P(j\mid i,a)-\alpha\mathbf1_{\{j=0\}}}{1-\alpha}.$$

Write $\widetilde J^*_{1-\alpha}$ for its discounted value at discount factor $1-\alpha$. The goal states that this value is finite, a stationary deterministic discounted-optimal policy exists, and every such policy is average-cost optimal for the original process. It also identifies a constant optimal average cost for every initial state:

$$J^*(i)=\alpha\widetilde J^*_{1-\alpha}(0),\qquad i\in S.$$

The goal does not assume the average optimality that it asserts. It requires the transformed law to satisfy the displayed formula at every admissible state-action pair (Arapostathis et al., 1993, Theorem 5.6 and proof, pp. 303–304).

Supporting targets

The milestones establish that the transformed law gives a controlled Markov process, that the discounted problem has an optimal stationary deterministic policy, and that the transformed discounted value satisfies the original ACOE with $\rho=\alpha\widetilde J^*_{1-\alpha}(0)$. The final milestone is the ACOE verification theorem needed to identify the average cost. The source gives the first two discounted claims through Theorem 2.1 and writes out the transformed equation in the proof of Theorem 5.6 (Arapostathis et al., 1993, pp. 289, 299, 304).

What the result supplies

The theorem replaces an average-cost optimization problem by one discounted problem with a prescribed discount factor and transition law. It yields a stationary deterministic policy that is optimal even when compared with every history-dependent randomized policy, and it shows that the optimal average cost is independent of the initial state. Without the common return probability, neither this particular law nor this fixed discount factor follows from the survey's argument (Arapostathis et al., 1993, Theorem 5.6).

The survey reports this as a known result of Ross rather than an open conjecture. The formalization work is to give the path measures, value functions, transformed process and verification result machine-checkable meanings. The Lean declarations here are open theorem statements awaiting proofs; compiling a statement with sorry does not establish the mathematical theorem. The policy and cost definitions can also support the other countable-state missions drawn from §5.

Difficulty

The transformed probabilities have to form a measurable stochastic kernel, preserve the action continuity assumptions and yield a controlled process with the original feasible actions and costs. The discounted value must be finite and uniformly bounded before its real form can enter the ACOE. A simple comparison of numerical optimal values is insufficient: a policy chosen in the transformed model must be shown optimal for the original model against the full policy class. The verification theorem also requires control of the terminal expectation of $h(X_t)$ for arbitrary admissible policies, rather than only the stationary policies named in its printed condition (Arapostathis et al., 1993, pp. 299–300, 304).

Formalization scope

Lean uses $\mathbb N$ for the countable state space and Mathlib probability kernels for the transition and randomized decision rules. Strategic path measures are constructed from those kernels. Nonnegative expected costs and their infima live in $[0,\infty]$, so an unbounded integral cannot silently become a finite real value. The transformed discounted value is converted to a real only in conclusions that also assert its finiteness. The ACOE uses real sums with explicit summability and an attained minimum. The model requires a Borel metric action space, nonempty compact action sets, measurable costs, and coordinatewise action continuity of the transition probabilities.

The source's §5.1 bounded-cost assumption is explicit in the goal and its discounted milestones. The displayed transformation needs $\alpha<1$; the paper's theorem sentence gives only $\alpha>0$, so the case $\alpha=1$ is excluded from this version. The paper prints (5.2) for stationary deterministic policies, but the proof uses it for all admissible policies to compare with $J^*$; the verification milestone takes the stronger, proof-supported hypothesis. Expectations in that condition are explicitly integrable. The converse part of Theorem 5.1 is not used and is outside this mission.

The transformed process is represented by another CMP constrained to have exactly the source's action sets, admissible costs and transition formula. A milestone poses its existence. This representation keeps the definition layer free of an unproved stochastic-kernel construction. The discount-optimal policy conclusion ranges over every stationary deterministic policy attaining the transformed discounted value, while the values themselves take infima over all admissible policies. Definitions of admissible path laws and the verification theorem are reusable contributions; proofs of the transformed kernel, stationary discounted existence and ACOE identity are welcome.

Selected references

• A. Arapostathis, V. S. Borkar, E. Fernández-Gaucherand, M. K. Ghosh and S. I. Marcus, Discrete-time controlled Markov processes with average cost criterion: a survey, SIAM Journal on Control and Optimization 31(2), 282–344, 1993. DOI: 10.1137/0331018.

Motivation

Distribution systems often move stock in two stages. A depot orders from an outside supplier and ships to a retail outlet, where customer demand arrives and unmet demand is backordered. Stock held anywhere costs money, a shortage at the outlet costs more, and each order carries a fixed charge. The basic question is what ordering and shipping rule minimizes total cost.

Clark and Scarf (Management Science 6, 1960) showed that over a finite planning horizon this two-echelon problem decomposes. The outlet solves its own single-location problem, and the depot solves a second single-location problem in which the outlet's shortfall is charged through an induced penalty cost. Federgruen and Zipkin (Operations Research 32(4), 1984) carried the decomposition to the infinite horizon. In the infinite-horizon problems the induced penalty becomes stationary and explicit, which makes the system computable with single-location tools. This mission covers the discounted-cost half of that paper (§§1–2).

Timeline:

• 1960: Clark and Scarf, finite-horizon decomposition, with a nonstationary penalty $\hat P_n$ built from the outlet's optimal cost functions.
• 1963: Iglehart (Management Science 9) proved, for the single-location discounted problem, that the finite-horizon value functions converge uniformly and that an $(s,S)$ policy is optimal.
• 1984: Federgruen and Zipkin combine the two results and prove that a stationary policy built from the decomposition is optimal for the infinite-horizon discounted and average-cost problems.

Setting

Time is discrete. The cost data are a fixed order cost $K$, an order cost rate $c^d$, a shipment cost rate $c^r$, a holding cost rate $h^d$ on all system stock, an extra holding cost rate $h^r$ at the outlet, and a backorder penalty rate $p^r$; all are positive. The discount factor $\alpha$ satisfies $0 \le \alpha < 1$, shipments take $l$ periods and orders take $L$ periods. One-period demands are independent copies of a nonnegative continuous random variable $u$ with mean $\mu < \infty$, and $u^{(i)}$ denotes the sum of $i$ copies.

The state is $(\hat y, v^d, x^r)$:

• $\hat y = (y^1, \dots, y^L)$ lists the outstanding orders, $y^i$ placed $i$ periods ago;
• $v^d$ is the depot's echelon inventory (its own stock plus $x^r$);
• $x^r$ is the outlet's stock plus shipments in transit.

An action is an order $y \ge 0$ and a shipment $z \ge 0$ with $x^r + z \le v^d + y^L$. With demand $u$, the next state is $((y, y^1, \dots, y^{L-1}), v^d + y^L - u, x^r + z - u)$. The one-period cost is

$$c^d(y) + h^d(v^d + y^L) + c^r z + R(x^r + z),$$

where $c^d(y) = K + c^d y$ for $y > 0$, $c^d(0) = 0$, and

$$R(x) = \alpha^l\{-h^d(x - l\mu) + p^r E[u^{(l+1)} - x]^+ + (h^d + h^r)E[x - u^{(l+1)}]^+\}.$$

$B^\alpha(s \mid \pi)$ is the expected total discounted cost of a policy $\pi$ from state $s$.

The critical number $x^{r*}$ minimizes $(1-\alpha)c^r x + R(x)$. The stationary induced penalty is $P(x) = 0$ for $x \ge x^{r*}$ and $P(x) = (1-\alpha)c^r(x - x^{r*}) + R(x) - R(x^{r*})$ otherwise. The depot problem $IH^d_\alpha$ has state $(\hat y, v^d)$, action $y \ge 0$ and one-period cost $c^d(y) + h^d(v^d + y^L) + P(v^d + y^L)$. The policy $\pi_\alpha^*$ orders by an optimal stationary policy $\sigma^d$ of $IH^d_\alpha$ and ships $z = \max\{0, \min\{x^{r*}, v^d + y^L\} - x^r\}$: up to the critical number when the depot has the stock, otherwise as much as it has.

Formalization targets

Goal: Theorem 1 (p. 827)

Assume $\alpha^l p^r \ge (1-\alpha^l)h^d$. For every state with $\hat y \ge 0$ and $x^r \le v^d$, and every admissible policy $\pi$,

$$B^\alpha(\hat y, v^d, x^r \mid \pi_\alpha^*) \le B^\alpha(\hat y, v^d, x^r \mid \pi).$$

The goal leaves the form of $\sigma^d$ open: any optimal stationary depot policy will do, and no $(s,S)$ structure is assumed.

Milestones

The milestones follow the paper's own route. Write $\hat g_n$, $g_n^r$, $\hat g_n^d$, $g_n^d$ for the $n$-period optimal costs of the system, of the outlet, of the depot with penalties $\hat P_n$, and of the depot with penalty $P$.

• Eq. (4): $\hat g_n = \hat g_n^d + g_n^r$.
• Property (e): $g_n^r \to g^r = B^{r\alpha}$.
• §2 claim (Iglehart): $g_n^r \to g^r$ uniformly on $(-\infty, x^{r*}]$.
• Lemma 1: $\hat P_n \to P$ uniformly on $\mathbb R$.
• Lemma 2: $\hat g_n^d - g_n^d \to 0$ uniformly.
• Lemma 3: $\hat g_n \to g^d + g^r$.
• Lemma 4: $g$ satisfies the optimality equation (8), and $\pi_\alpha^*$ attains it.

Significance

The theorem shows that, under discounting, the infinite-horizon two-echelon problem is solved by two single-location problems, with a penalty $P$ that is written in terms of $R$ alone. Computing $P$ does not require the outlet's optimal cost functions. The rest of the paper relies on this: its computational sections evaluate $P$ in closed form for normal demand, and they treat several outlets by relaxation. A machine-checked version also gives an infinite-horizon decomposition theorem against which future multi-echelon formalizations can be checked.

The result was proved in 1984 and is not open. It has not been formalized. The paper's proof is short only because it cites Iglehart's convergence results and Propositions 9.12 and 9.16 of Bertsekas and Shreve (1978) for its last step, so a formal proof must also supply these.

Difficulty

The obvious argument passes to the limit in the finite-horizon decomposition (4). That fails as stated, because the depot program (3) has nonstationary penalties $\hat P_n$, built from the outlet's optimal costs $g_{n-1}^r$, and its value functions are not those of any stationary problem. The comparison of $\hat P_n$ with $P$ needs uniform control over the whole real line. The first few $\hat P_n - P$ are in fact unbounded, since $g_0^r = 0$ has the wrong slope. The uniform control therefore holds only for large $n$, and the error has to be propagated through the depot recursion.

The second obstacle is that the one-period costs are unbounded in both directions: $h^d v$ is negative for negative $v$. Contraction arguments for bounded costs therefore do not apply. Lower boundedness on the feasible set needs the cost relation $\alpha^l p^r \ge (1-\alpha^l)h^d$, and passing from the optimality equation to optimality of a policy needs the theory of models with costs bounded below.

Formalization scope

Everything lives in the namespace FZEchelon.Discounted.

• Model. The data form a structure Model. The pipeline $\hat y$ is a vector indexed by $\{0, \dots, L-1\}$, whose index $k$ is the paper's $y^{k+1}$. For $L = 0$ the current order arrives at once.
• Policies and cost. Time runs forward with weight $\alpha^k$; the paper counts periods remaining. Policies are measurable, non-anticipative, deterministic and history dependent, and they must be feasible along every demand path. $B^\alpha$ is an extended real: the expectation of the positive part of the discounted cost sum minus that of the negative part, under the product law of the demands.
• Finite-horizon programs. These are real infima over the feasible actions.
• Hypotheses. Statements quantify over the physical states $\hat y \ge 0$, $x^r \le v^d$. The standing assumptions of §1 are bundled in StandingAssumptions: positive costs, $0 \le \alpha \le 1$, demand nonnegative, atomless and of finite mean. The §2 statements add $\alpha < 1$ and the cost relation, which the paper names in the proof of Theorem 1. The critical numbers $x^{r*}$ and $x_n^{r*}$ enter as minimizers. The depot policy $\sigma^d$ enters as a measurable, nonnegative stationary policy that is optimal for $IH_\alpha^d$; that is the paper's definition of $\pi_\alpha^*$, and its existence is Iglehart's.
• Ruled out. Comparing $\pi_\alpha^*$ only against stationary policies, or reading $B^\alpha$ as a bare series or a truncated sum, would trivialize or change the theorem. The comparison class is all admissible history-dependent policies.
• Corrections. Where the paper says "bounded" for every $n$ (§2 claim, Lemmas 1 and 2), the statements claim boundedness only where it holds: $n \ge 1$, $n \ge 2$, and eventually, respectively. The moderation notes give the counterexample at $n = 1$. Lemma 2 also carries the standing assumption of p. 821 that never ordering is not optimal. The statement is false without it.
• Infrastructure. A complete development needs the convexity theory of the single-location newsvendor function $R$, value iteration for discounted models with costs bounded below, and the Markov property for the product measure on demand sequences. The control-system file is reusable for other inventory and queueing missions. Formalizations of Iglehart's theorem and of Bertsekas–Shreve Propositions 9.12 and 9.16 are welcome.

Selected references

• A. Federgruen, P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
• A. J. Clark, H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/soc.html

Motivation

Many supply chains move stock through a central warehouse to the retail locations that face customer demand. Deciding how much the warehouse should order from outside, and how much it should ship to each retailer and when, is a stochastic dynamic program whose state contains every stock level and every outstanding order. Exact solution is out of reach except for the smallest systems, so structural results that reduce such a problem to single-location problems matter in practice.

Timeline.

• Clark and Scarf (Management Science 1960) showed that the finite-horizon, discounted problem of a serial system decomposes: an optimal policy is obtained by solving the most downstream location alone, charging its shortfalls to the upstream location through an induced penalty cost, and then solving the upstream location as a single-location problem with that penalty.
• Iglehart (Management Science 1963, and a 1963 chapter in Multistage Inventory Models and Techniques) established the infinite-horizon theory of the single-location problem with a fixed order cost: optimality of stationary $(s,S)$ policies under discounted and average costs, and the convergence of value iteration.
• Federgruen and Zipkin (Operations Research 1984) carried the decomposition to the infinite horizon for a depot and one retail outlet, under discounted costs (Theorem 1) and under the average-cost criterion (Theorem 2). This mission is about the average-cost case, §3 of that paper.

Setting

Time is divided into periods. A depot orders from an outside supplier with lead time $L \ge 0$ and supplies a retail outlet with shipment lead time $l \ge 0$. The demand $u$ in each period is a nonnegative random variable with law $\nu$ and finite mean $\mu$; demands in different periods are independent and identically distributed. Unmet demand at the outlet is backordered.

The state is $(\tilde y, v^d, x^r)$:

• $\tilde y = (y^1,\dots,y^L)$ lists the orders placed $1,\dots,L$ periods ago;
• $v^d$ is the depot's echelon inventory, its own stock plus the outlet's inventory position;
• $x^r$ is the outlet's inventory position, its stock plus shipments in transit.

In each period the decision is an order $y \ge 0$ and a shipment $z \ge 0$ with $x^r + z \le v^d + y^L$, where $y^L$ is the order arriving now. The state then moves to $((y, y^1,\dots,y^{L-1}),\, v^d + y^L - u,\, x^r + z - u)$.

Costs are a fixed order cost $K$, proportional order and shipment rates $c^d$ and $c^r$, a holding rate $h^d$ on system inventory, an extra holding rate $h^r$ at the outlet and a backorder penalty rate $p^r$. After the paper's accounting transformation, the one-period cost is

$$c^d(y) + D(v^d + y^L) + c^r z + R(x^r + z),$$

with $c^d(y) = K + c^d y$ for $y > 0$ and $c^d(0) = 0$, $D(v) = h^d v$, and, at $\alpha = 1$,

$$R(x) = -h^d(x - l\mu) + p^r E[u^{(l+1)} - x]^+ + (h^d + h^r) E[x - u^{(l+1)}]^+ ,$$

where $u^{(l+1)}$ is the demand over $l + 1$ periods. The critical number $x^{r*}$ is a minimizer of $R$. The stationary induced penalty is $P(x) = R(x) - R(x^{r*})$ for $x < x^{r*}$ and $0$ otherwise.

For a policy $\pi$ and initial state $s$, $B_n(s \mid \pi)$ is the expected cost of the first $n$ periods and $B(s \mid \pi) = \limsup_n B_n(s \mid \pi)/n$ is the average cost. Problem IH asks for a policy minimizing $B(s\mid\cdot)$ from every state. The depot problem IH$^d$ has states $(\tilde y, v^d)$, orders $y \ge 0$ and one-period cost $c^d(y) + D(v^d + y^L) + P(v^d + y^L)$. Its minimal average cost is $a^d$. The outlet problem has states $x^r$, shipments $z \ge 0$ and one-period cost $c^r z + R(x^r + z)$. The policy $\pi^*$ orders by an optimal stationary policy of IH$^d$ and ships $z = \max(0, \min(x^{r*}, v^d + y^L) - x^r)$: up to the critical number if the depot has the stock, otherwise as much as it has.

Formalization targets

Goal: Theorem 2 (p. 828)

With $\alpha = 1$ and $c^d = c^r = 0$, the policy $\pi^*$ is measurable and feasible from every physical state, and for every such state $s$ and every measurable feasible policy $\pi$,

$$B(s \mid \pi^*) \le B(s \mid \pi).$$

Milestones

• Property (f) (p. 824): $g^r_n(x)/n \to B^r(x) = c^r\mu + R(x^{r*})$ for the outlet program $g^r_n$.
• Eq. (4) (p. 823), for $0 \le \alpha \le 1$: $\hat g_n(\tilde y, v^d, x^r) = \hat g^d_n(\tilde y, v^d) + g^r_n(x^r)$.
• §3 claims (p. 828): with $c^r = 0$, $x^{r*}$ is the critical number of every period, $g^r_n(x) = nR(x^{r*})$ for $x \le x^{r*}$, $\hat P_n = P$, $\hat g^d_n = g^d_n$ and $\hat g_n = g_n$.
• §3 display (p. 828): $\hat g_n(\tilde y, v^d, x^r)/n \to a = a^d + R(x^{r*})$.
• Lemma 5 (p. 828): $B(s \mid \pi^*) = a$.
• Proof of Theorem 2 (p. 828): $\hat g_n(s) \le B_n(s \mid \pi)$ for every measurable feasible $\pi$.

Significance

The result. Theorem 2 reduces an average-cost problem with a multidimensional state to two problems with smaller states: a single-location $(s,S)$-type problem for the depot with a known convex penalty $P$, and a myopic critical-number rule for the outlet. The optimal system cost is the sum $a^d + a^r$ of their optimal costs. The paper uses this to compute optimal policies with standard single-location software, and its §5 builds heuristics for several outlets on the same decomposition.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of it has been machine-checked. A formal proof has to make precise what the paper leaves to "standard arguments":

• the class of measurable history-dependent policies;
• the expected costs of policies with unbounded one-period costs;
• the passage from history-dependent to Markov policies;
• the transient of $\pi^*$ when the outlet starts above its critical number.

Difficulty

The obvious argument would identify the average-cost optimal value through an average-cost optimality equation on the full state space and verify that $\pi^*$ attains it. No such equation is available here. The state space is unbounded, the one-period costs are unbounded both above and below in the state, and the depot's fixed cost makes its value functions $K$-convex rather than convex.

The paper's route avoids that equation but needs three separate facts:

• value iteration for the whole system, divided by $n$, converges to $a^d + a^r$, which rests on Iglehart's convergence for the depot and on the stationarity of the penalties when $c^r = 0$;
• the finite-horizon value bounds the cost of every history-dependent policy, not only of Markov ones;
• $\pi^*$ achieves $a$ from every state, including states with $x^r > x^{r*}$, where it does not ship at all until demand has brought the outlet below its critical number.

Formalization scope

• Representation. A state is a triple in $(\mathrm{Fin}\,L \to \mathbb R) \times \mathbb R \times \mathbb R$. For $L = 0$ the order placed now arrives at once. Time runs forward in Lean; the paper numbers periods backward. Finite-horizon value functions keep the paper's index $n$ (periods remaining). Each "min" of programs (1), (2), (3), (5) is a real infimum over the constraint set.
• Policies and costs. Policies are deterministic, history-dependent and measurable, and they must be feasible along every demand realization. $B_n$ is an extended real (expected positive part minus expected negative part of each period's cost). $B$ is a $\limsup$ in the extended reals, and the optimal average costs are infima in the extended reals.
• Standing assumptions (p. 821):
  • $K, h^d, h^r, p^r > 0$;
  • demands i.i.d., nonnegative, without atoms ("for convenience we shall assume $u$ is continuous") and with finite mean.
• Added hypotheses.
  • States are restricted to the physical ones, $\tilde y \ge 0$ and $x^r \le v^d$.
  • $c^d = c^r = 0$. The paper reduces to this case "without loss of generality", on the grounds that average proportional costs equal $c^d\mu$ and $c^r\mu$ "under all interesting policies" (p. 827). That class is never specified, and the proofs are written for $c^d = c^r = 0$. The general-cost version is the paper's informal reduction and is not part of the goal.
  • Eq. (4) is stated for $0 \le \alpha \le 1$ with $K, h^d, h^r, p^r > 0$ and $c^d, c^r \ge 0$ (so that it covers §3's case $c^d = c^r = 0$), and with the relation $\alpha^l p^r \ge (1 - \alpha^l)h^d$, which the paper names on p. 827; it holds automatically at $\alpha = 1$.
• Ruling out trivial readings.
  • $\pi^*$ is built from a depot rule $\sigma^d$ assumed optimal for IH$^d$ from every depot state. Its existence is Iglehart's theorem, cited and not formalized; no $(s,S)$ form is required.
  • The goal quantifies over all measurable feasible policies, and $\pi^*$'s own feasibility is a conclusion, so a vacuous policy class cannot satisfy it.
  • A sorry-free check in the workspace exhibits an instance (exponential demand) meeting every standing hypothesis other than the optimality of $\sigma^d$, including the existence of $x^{r*}$.
• Reusable infrastructure. The definitions of history-dependent policies and of extended-real expected and average costs for controlled processes driven by i.i.d. real noise are generic, and could be reused for other inventory and queueing models. Contributions are welcome on any milestone, and especially on a formal version of the Markov reduction (Dynkin–Yushkevich III.1) for this setting and on Iglehart's convergence of $g^d_n/n$.

Selected references

• A. Federgruen and P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
• A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2):259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259
• D. L. Iglehart, Dynamic Programming and Stationary Analyses of Inventory Problems, Chapter 1 in H. Scarf, D. Gilford and M. Shelly (eds.), Multistage Inventory Models and Techniques, Stanford University Press, 1963.
• E. B. Dynkin and A. A. Yushkevich, Controlled Markov Processes, Springer, 1979.
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.

Motivation

A controlled Markov process run under the long-run average cost criterion asks for a policy minimizing the asymptotic cost per stage. When every stationary policy induces a single recurrent class, the optimal average cost is a constant and is characterized by one equation, the average cost optimality equation (ACOE). In general it is not: under some policies the state process splits into several ergodic classes, different classes have different optimal costs, and the optimal average cost is a function $\rho(x)$ of the initial state. This is the multichain case.

For finite models, Howard ([Dynamic Programming and Markov Processes, 1960, pp. 61–62]) introduced a pair of coupled equations for this situation: one for the gain function $\rho$ alone, and one, the ACOE, for $\rho$ together with a relative value function $h$. Denardo and Fox (1968) developed the approach for finite multichain Markov renewal programs. For general Borel models, Yushkevich (1973) and Dynkin and Yushkevich (1979) introduced canonical triplets: a gain $\rho$, a terminal cost $h$ and a policy $\pi^*$ such that $\pi^*$ is optimal for every finite horizon $N$ with terminal cost $h$, and the optimal $N$-stage cost is exactly $h + N\rho$. The survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993), §6.1) states the link between the two notions as Theorem 6.2 and proves it on p. 317.

Setting

A controlled Markov process is a five-tuple $(\mathbf S, \mathbf A, U, P, c)$:

1. $\mathbf S$, the state space, and $\mathbf A$, the action space, are Borel spaces;
2. $U(x) \subseteq \mathbf A$ is the nonempty compact set of admissible actions at $x$, and $\mathbf K = \{(x,a) : a \in U(x)\}$ is measurable;
3. $P(dy \mid x, a)$ is a transition kernel on $\mathbf S$ given $\mathbf K$;
4. $c : \mathbf K \to \mathbb R$ is a measurable one-stage cost with $c \ge 0$ (the paper's standing Assumption 2.1).

A history is $h_t = (x_0, a_0, \dots, x_{t-1}, a_{t-1}, x_t)$. An admissible policy $\pi = (\pi_t)$ is a sequence of stochastic kernels $\pi_t(\cdot \mid h_t)$ on $\mathbf A$ with $\pi_t(U(x_t) \mid h_t) = 1$; the class of all of them is $\Pi$. A stationary deterministic policy $f \in \Pi_{SD}$ is a measurable map $f : \mathbf S \to \mathbf A$ with $f(x) \in U(x)$. An initial state $x$ and a policy $\pi$ determine a probability measure $\mathcal P^\pi_x$ on trajectories, with expectation $E^\pi_x$. For a terminal cost $h$ and $N \in \mathbb N_0$,

$$J_N(x, \pi, h) = E^\pi_x\Big[\sum_{t=0}^{N-1} c(X_t, A_t) + h(X_N)\Big], \qquad J^*_N(x, h) = \inf_{\pi \in \Pi} J_N(x, \pi, h).$$

$\mathcal M_b(\mathbf S)$ denotes the bounded measurable real functions on $\mathbf S$. For $R, H \in \mathcal M_b(\mathbf S)$ and $\pi^* \in \Pi$, the triplet $(R, H, \pi^*)$ is canonical if

$$J_N(x, \pi^*, H) = J^*_N(x, H) = H(x) + N R(x) \qquad \forall N \in \mathbb N_0,\ x \in \mathbf S. \tag{6.4}$$

Formalization targets

Goal: Theorem 6.2

Let $\pi^* \in \Pi_{SD}$, $\rho, h \in \mathcal M_b(\mathbf S)$, and $c$ bounded on $\mathbf K$. Then $(\rho, h, \pi^*)$ is a canonical triplet if and only if, for all $x \in \mathbf S$,

$$\rho(x) = \inf_{a \in U(x)} \Big\{ \int_{\mathbf S} \rho(y) P(dy \mid x, a) \Big\}, \tag{6.6}$$ $$\rho(x) + h(x) = \inf_{a \in U(x)} \Big\{ c(x,a) + \int_{\mathbf S} h(y) P(dy \mid x, a) \Big\}, \tag{6.7}$$

and $\pi^*(x)$ attains the infimum in both (6.6) and (6.7).

Milestones (the steps of the proof on p. 317)

1. One-step decomposition (last line of (6.8)): for $f \in \Pi_{SD}$, $J_{N+1}(x, f, h) = c(x, f(x)) + \int J_N(y, f, h) P(dy \mid x, f(x))$.
2. Dynamic programming step (second line of (6.8)): if $J^*_N(\cdot, h)$ is bounded and measurable, then $J_{N+1}(x, \pi, h) \ge T(J^*_N)(x)$ for every admissible $\pi$, where $T(v)(x) = \inf_{a \in U(x)}\{c(x,a) + \int v\, dP(\cdot \mid x, a)\}$ is the map (2.5).
3. Sufficiency, lower bound: under (6.6)–(6.7) and $J^*_N = h + N\rho$, $J^*_{N+1} \ge h + (N+1)\rho$.
4. Sufficiency, upper bound: under (6.6)–(6.7) and $J_N(\cdot, \pi^*, h) = h + N\rho$, $J_{N+1}(\cdot, \pi^*, h) = h + (N+1)\rho \ge J^*_{N+1}$.

Significance

The result. Theorem 6.2 turns a statement about every finite horizon and every history-dependent randomized policy into two pointwise equations in $(\rho, h)$ and a pointwise selection condition on $\pi^*$. A canonical policy is $N$-stage optimal for every $N$ with terminal cost $h$; dividing (6.4) by $N$ shows that its average cost is $\rho$. In the paper this is the entry point of Theorem 6.3, which shows that a canonical policy is strong average optimal and that $\rho$ is the optimal average cost, without any recurrence assumption. Equation (6.6) is the condition that makes $\rho$ behave as a constant in the optimization; when $\rho$ is constant it holds trivially, and Theorem 6.2 specializes to the bounded ACOE with a minimizing selector.

Formalizing it. The theorem is proved in the paper (and earlier by Yushkevich). This mission formalizes that proof on a general Borel model with history-dependent randomized policies and path measures built by the Ionescu-Tulcea theorem. Prove2Me has no formalization of the multichain coupled equations or of canonical triplets beyond finite models. The finite-horizon dynamic programming inequality of milestone 2, for policies that may use the whole history, is reusable in any finite-horizon or average-cost development on Borel spaces.

Difficulty

The algebra in the proof takes a few lines. The work is in two probabilistic facts that the paper uses without comment.

The first is the Markov decomposition of the $(N+1)$-stage cost: conditioning on the first state–action pair turns the remaining $N$ stages into an $N$-stage problem started from the next state. For a stationary policy the continuation is the same policy. For a history-dependent policy, the continuation is a policy that depends measurably on $(x_0, a_0)$. Expressing this on the Ionescu-Tulcea measure is where the effort goes.

The second is the identity $J^*_{N+1} = T(J^*_N)$. On a Borel model, $J^*_N$ need not be measurable and the infimum need not be attained by a measurable selector. That is why the paper usually works with semicontinuous models (p. 288). Theorem 6.2 avoids the issue: only the inequality $J^*_{N+1} \ge T(J^*_N)$ is needed, under the measurability that $J^*_N = h + N\rho$ supplies, and the reverse direction is supplied by the given $\pi^*$. A first attempt that proves the full identity $J^*_{N+1} = T(J^*_N)$ for general Borel models runs into measurable selection problems that the theorem never needs.

Formalization scope

• Model. BorelCMP S A has standard Borel S and Borel A, compact nonempty U x with measurable graph, a measurable cost c : S × A → ℝ with c ≥ 0 on K, and a Markov kernel P. c and P are total on S × A; only values on K enter. No continuity of c or P is assumed: Theorem 6.2 does not use Assumptions 2.2, 2.3 or 6.1.
• Policies. Policy M is the paper's $\Pi$: history-dependent, randomized, with admissibility $\pi_t(U(x_t)^c \mid h_t) = 0$. StationaryPolicy M is $\Pi_{SD}$ (measurable $f$ with $f(x) \in U(x)$). The infimum $J^*_N$ ranges over all of Policy M. Restricting it to stationary policies would make sufficiency trivial and necessity false, and is not what the paper states.
• Costs. $J_N(x, \pi, h)$ is a Bochner integral against the path measure. Every statement assumes $c$ bounded on $\mathbf K$ and $h$ bounded measurable, so the integral is a genuine expectation. $J^*_N$ is a real infimum, which is the true infimum because the family is bounded below by $-\sup|h|$ and nonempty whenever a stationary policy is given.
• Coupled equations. (6.6) and (6.7) with "$\pi^*(x)$ attains the infimum" are encoded in attained form: equality at $a = \pi^*(x)$ and the inequality for every $a \in U(x)$. This is equivalent to the printed condition and never forms a real infimum.
• The gain is a function. $\rho$ is a function of the state, not a constant. Specializing to a constant $\rho$ (the unichain case) would trivialize (6.6) and is not the theorem.
• Explicit choices. The paper's induction from $N-1$ to $N$ is stated from $N$ to $N+1$, so that no natural-number subtraction appears. Milestone 2 takes the measurability and boundedness of $J^*_N(\cdot, h)$ as a hypothesis, and takes any pointwise lower bound $w$ of $T(J^*_N)$ in place of the infimum. In the second display of the sufficiency part, the paper prints $J^*_{N-1}(y, \pi^*, h)$; the quantity meant is $J_{N-1}(y, \pi^*, h)$, which milestone 4 uses.
• Infrastructure. A complete development needs the Markov property of Kernel.trajMeasure at the first step, the shifted (continuation) policy and its measurability in the first state–action pair, and bounded-convergence bookkeeping for the Bochner integrals. These are reusable for every finite-horizon statement on this model. Proofs of the milestones are welcome independently. So are alternative proofs of the goal that bypass milestone 2 and argue directly with the canonical policy.

Selected references

• 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) (1993), 282–344, §6.1, Theorem 6.2. https://doi.org/10.1137/0331018
• A. A. Yushkevich, On a class of strategies in general Markov decision models, Theory Probab. Appl. 18 (1973), 777–779.
• E. B. Dynkin, A. A. Yushkevich, Controlled Markov Processes, Springer-Verlag, New York, 1979.
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, Cambridge, MA, 1960, pp. 61–62.
• E. V. Denardo, B. L. Fox, Multichain Markov renewal programs, SIAM J. Appl. Math. 16 (1968), 468–487.