Markov Chain

Motivation

A convention is a pattern of behaviour that is customary because everyone expects everyone else to follow it: driving on the right, or which party yields at a narrow bridge. Peyton Young's The Evolution of Conventions (Econometrica 61 (1993) 57–84) asks how such a pattern can emerge from decentralized play. The players have limited memory and limited information, and nobody coordinates them. The paper's model, adaptive play, is now a standard dynamic of learning in games. It is the starting point of the stochastic-stability theory of equilibrium selection (Foster and Young 1990; Kandori, Mailath and Rob 1993), which builds on the perturbation theory of Freidlin and Wentzell (1984).

This mission covers the first half of the paper: §3 (the model) and §4 (convergence when the players make no mistakes). Before mistakes can be added and stochastically stable conventions selected, the unperturbed process must be shown to settle at all. Theorem 1 gives the condition under which it does.

Setting

Let $\Gamma$ be a game with finitely many players $i$, a finite nonempty strategy set $S_i$ for each player, and payoffs $u_i(s)$ for strategy tuples $s \in \prod_j S_j$. Write $(x, s_{-i})$ for $s$ with player $i$'s strategy replaced by $x$.

• A play is a strategy tuple. Fix a memory $m$ and a sample size $k$ with $1 \le k \le m$. The state $h \in H = (\prod_j S_j)^m$ is the sequence of the last $m$ plays, oldest first.
• A successor of $h$ is obtained by deleting the oldest play and appending a new one.
• A sample is a set of $k$ positions of $h$. Player $i$'s best reply to a sample $K$ maximizes the total payoff $\sum_{t \in K} u_i(x, (h_t)_{-i})$ against the sampled plays.
• A best-reply distribution gives, for each $i$ and $h$, a probability distribution $p_i(\cdot \mid h)$ on $S_i$ that is positive exactly on the strategies that are best replies to some sample of size $k$. The sampling law itself is arbitrary.
• Adaptive play $P^0$ is the Markov chain on $H$ that moves from $h$ to the successor with new play $s$ with probability $\prod_i p_i(s_i \mid h)$.
• A strict Nash equilibrium is a tuple $s$ from which every unilateral deviation is strictly worse. A convention is a state $(s, s, \dots, s)$ with $s$ a strict Nash equilibrium.
• The best-reply graph has an edge $s \to (x, s_{-i})$ whenever $x \ne s_i$ is a best reply of $i$ to $s_{-i}$. $\Gamma$ is weakly acyclic if from every $s$ a directed path leads to a sink. $L(s)$ is the length of a shortest such path from $s$ to a strict Nash equilibrium, and $L_\Gamma = \max_s L(s)$.

Formalization targets

Goal: Theorem 1 (p. 64)

If $\Gamma$ is weakly acyclic and $k \le m/(L_\Gamma + 2)$, then for every best-reply distribution and every initial state $h$,

$$\lim_{t\to\infty} \sum_{h' \text{ a convention}} \big((P^0)^t\big)_{hh'} = 1 .$$

Milestones

1. Absorbing states (§4, p. 62): $P^0_{hh} = 1$ if and only if $h$ is a convention.
2. Sinks (§4, p. 64): the sinks of the best-reply graph are exactly the strict Nash equilibria. Hence weak acyclicity means that one-player-at-a-time best replies can reach a strict equilibrium from every tuple.
3. A run of best replies (proof of Theorem 1, p. 64): if $m \ge 2k-1$, then with positive probability $k$ consecutive identical best replies to the last $k$ plays are appended.
4. Uniform bound (proof of Theorem 1, p. 65): there is $q > 0$ such that from every state a convention is reached within $M = kL_\Gamma + m$ periods with probability at least $q$.
5. Geometric tail (proof of Theorem 1, p. 64): such a uniform bound makes the probability of no convention after $rM$ periods at most $(1-q)^r$.
6. Example 2 (pp. 65–66, off the goal's path): in a Battle-of-the-Sexes game with complete sampling $k = m$, a perfectly miscoordinated history stays miscoordinated forever.

Significance

Theorem 1 identifies a class of games, the weakly acyclic ones, in which boundedly rational players who best-reply to small random samples of the past almost surely lock in to a strict pure equilibrium. The paper's examples of weakly acyclic games (p. 63) are pure coordination games and games with common interests in which no two strategy tuples are payoff equivalent. Absorption is in behaviour, not just in empirical frequencies. Example 2 shows that this fails for fictitious-play-like complete sampling, so the sampling ratio $k/m$ is a real ingredient. The absorbing states identified in the first milestone are the states among which the stochastic-stability analysis of the paper's later sections selects.

The result is proved in the paper. To the best of our knowledge no machine-checked version exists. The mission asks for a formal proof of Theorem 1 and its milestones for an arbitrary best-reply distribution. That generality is the paper's own: non-uniform sampling is explicitly allowed. A formal proof also pins down the memory bookkeeping in the paper's proof (look-backs of $2k-1$, $3k-1$ and $kr + 2k - 1$ periods), which the text checks only in words.

Difficulty

Adaptive play is a finite Markov chain. The obvious route through the generic theory of absorbing chains requires showing that a convention is reachable from every state, and that is where the argument becomes delicate. A best-reply path in the game cannot be followed directly: each player only sees a random sample, and the players who are not moving must keep playing their old strategies. The proof gets around this by having the non-moving players keep sampling older parts of the history, so those parts must still be in memory. This is what forces the bound $k \le m/(L_\Gamma+2)$. A uniform, state-independent constant is then needed to turn reachability into almost-sure convergence.

Formalization scope

Players form a finite type ι, strategies a family of finite nonempty types S i, and payoffs u : ι → (∀ i, S i) → ℝ. A state is Fin m → ∀ i, S i with position 0 the oldest play. A best-reply distribution is any p : ∀ i, H → S i → ℝ with the stated support. All statements quantify over every such p. Adaptive play is a Matrix H H ℝ, and "converges almost surely to a convention" is stated through matrix powers. That is equivalent to almost-sure absorption because conventions are absorbing. The condition $k \le m/(L_\Gamma+2)$ is $k(L_\Gamma+2) \le m$ in ℕ. $L(s)$ is an sInf on ℕ that is never empty under weak acyclicity.

The display (1) on p. 62 reads "the right-most element of $h$". The formalization uses the right-most element of the successor $h'$, the only reading under which the rule is meaningful.

The goal cannot be satisfied trivially. The sampling law is not fixed, the conclusion is a limit equal to $1$ from every initial state (not "with positive probability" or "along some path"), and the hypotheses are jointly satisfiable, for example by a $2\times2$ coordination game with uniform sampling. A best reply to a sample uses the joint empirical distribution of the sampled plays, not independent marginals.

A complete development needs elementary Markov-chain facts about matrix powers and absorbing sets, plus combinatorics of shifted histories. These parts are reusable for any finite-memory learning dynamic. Proofs of individual milestones are welcome independently.

Related platform work: stochastic fictitious play in potential games (StochFictPlay.*, Hofbauer–Sandholm 2002) and calibrated learning to correlated equilibrium (CalibratedCE.*, Foster–Vohra 1997) formalize other learning dynamics. The perturbed process and the selection of risk-dominant conventions are the subject of the sibling missions The Evolution of Conventions II and III.

Selected references

• H. P. Young, The Evolution of Conventions, Econometrica 61(1), 1993, 57–84. https://doi.org/10.2307/2951778
• D. Foster and H. P. Young, Stochastic Evolutionary Game Dynamics, Theoretical Population Biology 38, 1990, 219–232. https://doi.org/10.1016/0040-5809(90)90011-J
• M. Kandori, G. J. Mailath and R. Rob, Learning, Mutation, and Long Run Equilibria in Games, Econometrica 61(1), 1993, 29–56. https://doi.org/10.2307/2951777
• M. I. Freidlin and A. D. Wentzell, Random Perturbations of Dynamical Systems, Springer, 1984. https://doi.org/10.1007/978-1-4684-0176-9
• J. C. Harsanyi and R. Selten, A General Theory of Equilibrium Selection in Games, MIT Press, 1988.
• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70(6), 2002, 2265–2294. https://doi.org/10.1111/1468-0262.00376
• D. P. Foster and R. V. Vohra, Calibrated Learning and Correlated Equilibrium, Games and Economic Behavior 21, 1997, 40–55. https://doi.org/10.1006/game.1997.0595

Motivation

Many models in economics, biology and computer science are finite Markov chains that have several absorbing states or recurrent classes, so their long-run behaviour depends on where they start. Adding a small amount of noise (mistakes, mutations, experimentation) makes the chain irreducible, and the noisy chain then has a unique stationary distribution. As the noise vanishes, that distribution concentrates on some of the original recurrent classes. The stochastically stable states are the ones that keep positive weight in the limit; they are the states the system spends nearly all its time in when the noise is small but nonzero.

H. Peyton Young's The Evolution of Conventions (Econometrica, 1993) proved a general finite-state characterization of these states, which he used to select among the equilibria of coordination games under adaptive play. The characterization rests on the theory of small random perturbations of Freidlin and Wentzell (1984), developed for diffusions, and on a combinatorial lemma of theirs expressing stationary distributions through spanning trees. Kandori, Mailath and Rob (1993) characterized the limit distribution by spanning trees on the whole state space for their model of learning with mutations; Young's Lemma 1 generalizes their Theorem 1 (p. 78), and his Lemma 2 reduces the computation to the much smaller graph of recurrent classes. Foster and Young (1990) introduced stochastic stability for evolutionary dynamics, and the equilibria it selects in $2\times 2$ games coincide with the risk-dominant equilibria of Harsanyi and Selten (1988).

Setting

Let $X$ be a finite set and $P^0$ the transition matrix of a Markov chain on $X$. A state $y$ is reachable from $x$ if $(P^0)^n_{xy} > 0$ for some $n \ge 0$; $x$ is recurrent if every state reachable from $x$ can reach $x$ back; the recurrent communication classes $X_1, \dots, X_J$ are the communication classes of recurrent states.

A family $(P^\varepsilon)_{\varepsilon \in (0,a]}$ of Markov chains on $X$ is a regular perturbation of $P^0$ if for all $x, y$:

• (6) $P^\varepsilon$ is aperiodic and irreducible for every $\varepsilon \in (0,a]$;
• (7) $P^\varepsilon_{xy} \to P^0_{xy}$ as $\varepsilon \to 0$;
• (8) if $P^\varepsilon_{xy} > 0$ for some $\varepsilon$, there is $r \ge 0$ with $0 < \lim_{\varepsilon \to 0} \varepsilon^{-r} P^\varepsilon_{xy} < \infty$.

The exponent $r = r(x,y)$ is the resistance of the transition $x \to y$. The graph $G$ has vertex set $X$ and an edge $(x,y)$ when $P^\varepsilon_{xy} > 0$ for all small $\varepsilon$, weighted by $r(x,y)$.

For $z \in X$, a $z$-tree is a spanning tree of edges of $G$ in which every $x \ne z$ has a unique directed path to $z$. The potential of $z$ is

$$\gamma(z) = \min_{T \in \mathcal T_z} \sum_{(x,y) \in T} r(x,y). \tag{9}$$

For classes $i \ne j$, $r_{ij}$ is the least resistance of a path in $G$ from $X_i$ to $X_j$. On the complete directed graph $\mathcal G$ with vertices $1, \dots, J$ and edge weights $r_{ij}$, the stochastic potential $\gamma_j$ of $X_j$ is the least total weight of a $j$-tree in $\mathcal G$.

Formalization targets

Goal: Theorem 4 (p. 78)

If $\mu^\varepsilon$ is the stationary distribution of $P^\varepsilon$ for $\varepsilon \in (0,a]$, then $\mu^\varepsilon \to \mu^0$ as $\varepsilon \to 0$, where $\mu^0$ is a stationary distribution of $P^0$, and

$$\mu^0_x > 0 \iff x \in X_j \text{ for some } j \text{ with } \gamma_j = \min_i \gamma_i .$$

Milestones, in the order of the paper's proof

1. Resistance (p. 77). The exponent in (8) is unique; a transition positive for some $\varepsilon$ is an edge of $G$; and the edges of zero resistance are exactly the transitions with $P^0_{xy} > 0$.
2. Markov chain tree formula (p. 79). For an aperiodic irreducible chain $P'$, $\mu'_z = p'_z / \sum_x p'_x$ with $p'_z = \sum_{T \in \mathcal T_z} \prod_{(x,y)\in T} P'_{xy}$ is the unique stationary distribution.
3. Lemma 1 (p. 78). $\mu^\varepsilon \to \mu^0$, $\mu^0$ is stationary for $P^0$, and $\mu^0_x > 0$ iff $\gamma(x) \le \gamma(y)$ for all $y$.
4. (p. 80) A stationary distribution of a finite chain vanishes on non-recurrent states.
5. (p. 80) All states of a recurrent class of $P^0$ have the same potential.
6. Lemma 2 (p. 80). $\gamma(x) = \gamma_j$ for every $x \in X_j$.

Significance

Theorem 4 turns a limit of stationary distributions into a finite optimization: compute least-resistance paths between the recurrent classes, then a minimum-weight arborescence on the reduced graph. The answer depends only on the orders of magnitude of the perturbations, not on their exact values, which is what makes the result usable when the noise model is known only qualitatively. It underlies the equilibrium-selection results of the same paper (risk dominance in $2\times 2$ coordination games, Theorem 3) and much of the later stochastic evolutionary game theory literature.

The result is proved in the paper, with the tree formula imported from Freidlin and Wentzell. As far as is known, none of it is formalized: Mathlib has irreducible and primitive nonnegative matrices but neither the Markov chain tree formula, aperiodicity, recurrent classes of a finite chain, nor minimum arborescences. A complete development would produce these as reusable components.

Difficulty

The first idea is to take the limit in $\mu^\varepsilon P^\varepsilon = \mu^\varepsilon$: compactness and (7) give that every limit point of $\mu^\varepsilon$ is stationary for $P^0$, but $P^0$ has many stationary distributions, so this neither proves convergence nor identifies the support. Both come from the tree formula, which makes $\mu^\varepsilon_z$ a ratio of sums of products whose orders of magnitude are read off from the resistances; the absence of cancellation (all terms are nonnegative) is essential. The second difficulty is Lemma 2: an optimal $x$-tree on the whole state space must be transformed, by the paper's tree surgery on junctions (pp. 80–83), into something comparable with a $j$-tree on the class graph without increasing its resistance. The easy inequality $\gamma(x_j) \le \gamma_j$ glues optimal paths and zero-resistance trees together; the reverse inequality is where the work lies.

Formalization scope

States form a Fintype X with decidable equality; chains are real matrices Matrix X X ℝ, row stochasticity is Matrix.rowStochastic, irreducibility is Mathlib's Matrix.IsIrreducible, and aperiodicity (every state has period 1) is defined in the mission. The family $P^\varepsilon$ is a function ℝ → Matrix X X ℝ constrained only on $(0, a]$; all limits are one-sided ($\varepsilon \to 0^+$), $\varepsilon^{-r}$ is the real power, and "$0 < \lim < \infty$" is a real limit $c > 0$. Distributions are row vectors and stationarity is $\mu A = \mu$. Trees are parent maps with edges pointing toward the root. Potentials, class resistances and stochastic potentials are infima in EReal, where an empty infimum is $+\infty$; under the hypotheses all of them are finite.

The goal quantifies over every regular perturbation, not a parametric family such as $(1-\varepsilon)P^0 + \varepsilon Q$, and over every family of stationary distributions of the $P^\varepsilon$ (unique by (6)). The recurrent classes are computed from $P^0$, not supplied as data, and $\gamma_j$ is computed on the class graph with weights $r_{ij}$; defining $\gamma_j$ as $\gamma(x)$ for some $x \in X_j$ would make Lemma 2 definitional and is ruled out.

Contributions welcome: the Markov chain tree formula and the uniqueness of stationary distributions for irreducible finite chains (both reusable well beyond this mission), recurrence and the support of stationary distributions, and the arborescence surgery of Lemma 2.

Selected references

• H. P. Young, The Evolution of Conventions, Econometrica 61(1), 1993, 57–84. https://doi.org/10.2307/2951778
• M. I. Freidlin and A. D. Wentzell, Random Perturbations of Dynamical Systems, Springer, 1984 (Ch. 6, Lemma 3.1). https://doi.org/10.1007/978-1-4684-0176-9
• M. Kandori, G. J. Mailath and R. Rob, Learning, Mutation, and Long Run Equilibria in Games, Econometrica 61(1), 1993, 29–56. https://doi.org/10.2307/2951777
• D. P. Foster and H. P. Young, Stochastic Evolutionary Game Dynamics, Theoretical Population Biology 38, 1990, 219–232. https://doi.org/10.1016/0040-5809(90)90011-J
• J. C. Harsanyi and R. Selten, A General Theory of Equilibrium Selection in Games, MIT Press, 1988. https://mitpress.mit.edu/9780262582384/
• Related missions on learning dynamics: StochFictPlay.* (Hofbauer and Sandholm 2002, stochastic fictitious play) and CalibratedCE.* (calibrated learning and correlated equilibrium).

Motivation

A finite dynamic program with total reward is the basic model of sequential decision making without discounting: a system moves among finitely many states, a decision maker picks an action in each state, collects a reward, and the system moves on or stops. The quantity of interest is the expected total reward of a policy, summed over the whole (possibly infinite) horizon, and the question is whether a simple policy — one that uses the same decision rule at every step — is as good as any other.

For discounted or strictly substochastic models the answer has long been known. Shapley (1953) showed by successive approximations that, when every transition matrix has row sums strictly below one, some stationary policy maximizes the total reward among stationary policies; Howard (1960) gave the policy-improvement method for finding one; Blackwell (1962) showed that the maximum over all policies is attained among stationary ones. All of these rest on a contraction hypothesis $\|P(f)\|<1$.

Veinott's 1969 paper (DOI 10.1214/aoms/1177697379), best known for its sensitive discount optimality criteria, opens in §2 by proving these classical results under the much weaker hypothesis that each stationary policy is transient, and without requiring the transition weights to be substochastic at all. Partial results in this direction were due to Eaton and Zadeh, Derman, and Denardo. The total-reward model without a contraction assumption covers stopping problems, shortest-path type problems and models in which "transition weights" are not probabilities (growth factors, populations), which is why the generalized model is of independent interest.

Setting

There are $S\ge 1$ states $1,\dots,S$. In state $s$ a finite nonempty set $A_s$ of actions is available; taking action $a$ earns the real reward $r(s,a)$ and assigns the transition weight $p(t\mid s,a)\ge 0$ to each state $t$. No bound on $\sum_t p(t\mid s,a)$ is assumed. The set of decision rules is $F=\times_{s=1}^S A_s$; for $f\in F$, $r(f)$ is the vector $(r(s,f(s)))_s$ and $P(f)$ the matrix $(p(t\mid s,f(s)))_{s,t}$.

A policy is a sequence $\pi=(f_1,f_2,\dots)$ of decision rules. The policy $f^\infty=(f,f,\dots)$ is stationary; $(g,\pi)=(g,f_1,f_2,\dots)$ uses $g$ first and then follows $\pi$; ${}^N\pi$ repeats the first $N$ rules of $\pi$ forever and is called periodic. Let $P^0(\pi)=I$ and $P^N(\pi)=P(f_1)\cdots P(f_N)$. The policy $\pi$ is transient if $\sum_{N\ge0}P^N(\pi)$ converges, and then its vector of total returns is

$$V(\pi)=\sum_{N=0}^\infty P^N(\pi)\,r(f_{N+1}).$$

The one-step comparison $v(g,\pi^*)=V(g,\pi^*)-V(\pi^*)$ measures the gain from deviating to $g$ for one step. Vectors are compared coordinatewise, and $x>y$ means $x\ge y$, $x\ne y$. For a matrix $B$, $\|B\|=\max_i\sum_j|b_{ij}|$ and $|\sigma(B)|$ is its spectral radius. Finally $V^*=\max_f V(f^\infty)$ and $\Re V=\max_g[r(g)+P(g)V]$, both coordinatewise.

Formalization targets

Goal: Corollary 6

If every stationary policy is transient, there is $f\in F$ with

$$V(\pi)\le V(f^\infty)\qquad\text{for every policy }\pi.$$

The hypothesis concerns only the finitely many stationary policies; the conclusion compares against every policy, stationary or not.

Milestones

1. Lemma 1. For transient $\pi=(g_i)$ and $\pi^*$: $V(\pi)-V(\pi^*)=\sum_N P^N(\pi)\,v(g_{N+1},\pi^*)$, and $V(g^\infty)-V(\pi^*)=[I-P(g)]^{-1}v(g,\pi^*)$.
2. Lemma 2. If every stationary policy is transient and $f\in F$: either $v(g,f^\infty)>0$ for some $g$, and then $V(g^\infty)>V(f^\infty)$, or $v(g,f^\infty)\le0$ for all $g$, which holds iff $f^\infty$ is best among stationary policies.
3. Corollary 1. If every stationary policy is transient, some stationary policy maximizes $V$ over the stationary policies.
4. Corollary 2. Under the same hypothesis, $V^*$ is the unique fixed point of $\Re$.
5. Lemma 3 (Hoffman). For every $\varepsilon>0$ and every program there is a positively similar program with $\max_g\|\tilde P(g)\|<\max_g|\sigma(P(g))|+\varepsilon$.
6. Corollary 4, read with "every" and with "some": stationary, periodic and arbitrary policies are transient together, and this is equivalent to $\|P^N(\pi)\|<1$ for some $N\ge1$; with $\|P(g)\|\le1$ also to $\|P^S(\pi)\|<1$.
7. Theorem 1. If every stationary policy is transient and $\pi^*$ is any policy: $v(g,\pi^*)>0$ implies $V(g^\infty)>V(\pi^*)$, and $v(\cdot,\pi^*)\le0$ iff $V(\pi)\le V(\pi^*)$ for all $\pi$.

Significance

Corollary 6 is the existence half of the theory of total-reward Markov decision processes: it says that the search for an optimal policy can be restricted to the finite set of stationary policies, and, together with Corollary 2 and Theorem 1, that such a policy is characterized by the optimality equation $\Re V=V$ and by the absence of one-step improvements. Corollary 4, which the paper's introduction singles out as the section's main new result, shows that transience of the finitely many stationary policies already forces transience of every policy, uniformly; this is what makes $V(\pi)$ well defined for all policies. Hoffman's Lemma 3 converts transience into a contraction in a rescaled norm, the device behind geometric convergence of value iteration (Corollary 3 of the paper).

On the formal side, Mathlib has matrices, summability and spectral radii but no total-reward decision model. These results are proved in the 1969 paper and are standard in the textbook literature on Markov decision processes; none of them has a machine-checked proof that we know of. Related platform items concern other models: the stochastic shortest path results of Bertsekas and Tsitsiklis (a cost model with a termination state, stochastic rows and an infinite-cost assumption on improper policies) and Blackwell's discounted model; neither covers nonnegative, non-substochastic weights.

Difficulty

Without a contraction, the standard argument — $\Re$ is a contraction, so it has a unique fixed point attained by a stationary policy — has nothing to start from: $\|P(g)\|$ may exceed one for every $g$, and the transition weights need not be probabilities, so no probabilistic coupling or stopping-time argument applies directly. Transience of each stationary policy is a statement about finitely many matrix powers $P(g)^N$, whereas the goal concerns infinite products of different matrices $P(f_1)P(f_2)\cdots$, whose behaviour is not controlled by the spectral radii of the factors in general. Passing from the stationary policies to all policies is the step where the obvious argument fails.

Formalization scope

The Lean development fixes these conventions.

• States are a nonempty finite type St; actions are a family of nonempty finite types A : St → Type, so $F$ is the dependent function type (s : St) → A s, not a common action set.
• A program is a structure Program St A with real rewards and nonnegative weights; no row-sum bound is part of the structure. Only 5° of Corollary 4 assumes $\|P(g)\|\le1$.
• Policies are deterministic Markov sequences ℕ → F, indexed from $0$: π 0 is $f_1$. "All policies" means all such sequences.
• Transience is Summable of $N\mapsto P^N(\pi)$ in the entrywise topology. $V$ is a tsum; it is the genuine series exactly for transient policies.
• $>$ on vectors is written out as $\ge$ and $\ne$; $\|\cdot\|$ is the maximum absolute row sum, defined explicitly; $|\sigma(\cdot)|$ is Mathlib's spectralRadius ℂ of the complexified matrix, valued in $[0,\infty]$.
• $V^*$ and $\Re$ are coordinatewise Finset.sup' over the finite set $F$.

A trivializing formalization is ruled out: the goal and Theorem 1 do not assume the competing policies transient (that would hide Corollary 4 inside the hypothesis), and since a non-summable tsum is $0$, no statement compares $V$ of a policy whose transience is not either assumed or implied by the hypotheses. The hypothesis "every stationary policy is transient" is satisfiable (for instance when all weights are zero) and is not implied by any row-sum bound.

A complete development needs Neumann series for nonnegative matrices, the Perron–Frobenius-type fact that a nonnegative matrix with spectral radius below one has a nonnegative $(I-B)^{-1}=\sum B^N$, and finite-dimensional spectral theory relating $|\sigma(B)|<1$ to $B^N\to0$. These are reusable well beyond this mission; contributions of such lemmas, and of proofs of the milestones in any order, are welcome.

Selected references

• A. F. Veinott, Jr., Discrete dynamic programming with sensitive discount optimality criteria, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
• D. Blackwell, Discrete dynamic programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• L. S. Shapley, Stochastic games, Proc. Nat. Acad. Sci. 39(10):1095–1100, 1953. https://doi.org/10.1073/pnas.39.10.1095
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• E. V. Denardo, Contraction mappings in the theory underlying dynamic programming, SIAM Review 9(2):165–177, 1967. https://doi.org/10.1137/1009030
• C. Derman, On sequential decisions and Markov chains, Management Sci. 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16

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

Demand for many products does not arrive at a constant rate. It moves with an underlying environment: the economy, the season, a product's life-cycle stage, the state of a customer's own operations. Song and Zipkin (Oper. Res. 41(2):351–370, 1993) modelled this environment as a continuous-time Markov chain, the world, whose current state sets the Poisson demand rate, and showed that a basestock policy whose level depends on the current world state is optimal under linear order costs. Missions I and II of this series formalize those optimality results.

A practitioner who uses such a policy wants to know how the levels depend on the world. If a higher world state means more demand now and more demand later, a higher level should be kept. That is what intuition says, but the optimal level depends on the whole future of the world chain, not only on the current demand rate. §4 of the paper answers it for a world with an arbitrary partial order, which covers several independent demand drivers at once.

Setting

The world $A$ is a continuous-time Markov chain on a countable set $\mathbf I$ with generator $Q = (q_{ij})$, $q_i = -q_{ii}$, and bounded rates $q^* = \sup_i q_i$, $\lambda^* = \sup_i \lambda_i$. While $A = i$, unit demands arrive at rate $\lambda_i$, all demand is backlogged, and orders arrive after a random lead time $L$ that is independent of the world and the demand. Costs are discounted at rate $\alpha > 0$. With the unit order cost $\bar c$, holding rate $h$ and penalty rate $p$, set $c = \bar c\,E[e^{-\alpha L}]$ and

$$\hat C(x) = \max\{-px,\ hx\}, \qquad C(i,y) = E\big[e^{-\alpha L}\hat C(y - D^i_L)\big],$$

where $D^i_L$ is the demand during a lead time when the world starts in $i$. Uniformizing at a rate $\mu \ge q^* + \lambda^*$ with $\beta = 1/(\mu+\alpha)$ and $\gamma = \beta\mu$, the myopic cost is $G^+(i,y) = (1-\gamma)cy + \beta C(i,y)$. The linear-cost model ($K = 0$) is solved by value iteration from $W_0 \equiv 0$:

$$G_n(i,y) = G^+(i,y) + \beta\lambda_i c + \beta\Big\{\lambda_i W_{n-1}(i,y-1) + \sum_{j\ne i} q_{ij}W_{n-1}(j,y) + (\mu-\lambda_i-q_i)W_{n-1}(i,y)\Big\},$$

$W_n(i,x) = \min_{y\ge x} G_n(i,y)$, with limits $G_\infty$ and $W_\infty$. The myopic level $y^+(i)$, the finite-horizon levels $y^*_n(i)$ and the optimal level $y^*(i)$ are the smallest minimizers of $G^+(i,\cdot)$, $G_n(i,\cdot)$ and $G_\infty(i,\cdot)$, and $y^*_\infty(i) = \lim_n y^*_n(i)$. Throughout, $\alpha\bar c < p$ (Assumption 1).

The world states carry a partial order $\preceq$. The chain is stochastically partial-monotone (display (14)) if for every $i \preceq j$ there is a probability space carrying copies of $A$ started at $i$ and at $j$ whose paths satisfy $A(t) \preceq A'(t)$ for all $t \ge 0$ almost surely. Condition 1 requires this together with $\lambda_i$ nondecreasing in $i$.

Formalization targets

Goal: Theorem 8

Under Condition 1, the three families of levels exist and are nondecreasing along $\preceq$:

$$i \preceq j \ \Longrightarrow\ y^+(i) \le y^+(j),\qquad y^*(i) \le y^*(j),\qquad y^*_\infty(i) \le y^*_\infty(j).$$

Milestones

• Lemma 8, with its fixed-lead-time form from the proof: $D(l)$ given $A(0)=i$ is stochastically smaller than given $A(0)=j$ for each $l \ge 0$, and $D^i_L \le_{st} D^j_L$.
• Lemma 9: $\Delta C(i,y) \ge \Delta C(j,y)$ for $i \preceq j$.
• Theorem 7: for all $n \ge 1$ and fixed $x$, $\Delta W_{n-1}(i,x)$ and $\Delta G_n(i,x)$ are nonincreasing in $i$, and $y^*_n(i)$ is nondecreasing in $i$.
• Theorem 9 (companion): if $q_{ij} \ne 0$ only for $j \succeq i$, then $y^*(i) = y^+(i)$, so the myopic policy is optimal.
• Theorem 10 (companion): with a fixed order cost $K > 0$, the bounds $S^+(i)$, $r^+(i)$, $r^-(i)$, $r^{--}(i)$ on the optimal $(r,S)$ parameters are nondecreasing in $i$.

Significance

Theorem 8 turns an optimal policy into a structured one. A world-dependent basestock policy has one level per world state; monotonicity says the levels follow the order of the states, which reduces search, makes the levels interpretable, and gives sanity checks for computed solutions. Theorem 9 identifies when nothing beyond the one-step cost needs to be computed at all. Theorem 10 is the paper's substitute for an open question: the authors could not show that the optimal $(r,S)$ parameters are monotone, and instead bound them between monotone functions.

All of these results are proved in the paper. None of them has been machine-checked. The formalization requires a value-iteration argument for a model with unbounded one-period costs, a coupling argument for Markov-modulated Poisson demand, and the passage to the limit in the levels. These are the ingredients of most monotone-policy results in inventory theory with Markov-modulated demand.

Difficulty

The obvious argument fails at the generator. For a single scalar world, stochastic monotonicity is equivalent to the expectation inequality (15) for nondecreasing functions, and the inductive step of Theorem 7 only needs that. For a partial order, the expectation inequality is strictly weaker than the coupling (14) (Massey 1987). The induction must also handle the cross term $\sum_j q_{ij}\Delta W_{n-1}(j,x)$, which requires an embedded discrete-time chain whose one-step kernel preserves the order. The paper's Lemma 7 asserts that the embedded chain $P = I + Q/\nu$ is monotone for every $\nu \ge q^*$. As printed, this is false at $\nu = q^*$: for two states with $q_{01} = q_{10} = 1$, $P$ swaps the states. A complete proof cannot rely on that lemma as printed.

A second difficulty is that the one-period cost is unbounded. The classical theorems that ordered differences survive value iteration (Denardo, Lovejoy) assume bounded costs, so the induction has to be carried out by hand, and the limits $G_\infty$, $y^*_\infty$ must be justified by Lemma 4's uniform bounds.

Formalization scope

The Lean development lives in the namespace SongZipkinFluct.Monotone. World states form a countable nonempty type with a PartialOrder instance; no linear order is assumed. Inventory positions are integers. The demand-count law $f_i(d\mid l)$ and the world transition function $P(t)$ are defined by uniformization at the model's rate $\mu$, the paper's own device. The lead-time law is a probability measure on $[0,\infty)$, and $C(i,y)$ is the series $\sum_d g_i(d\mid\alpha)\hat C(y-d)$ of display (16). $W_n$ uses an infimum over integers $y \ge x$, and $W_\infty$, $G_\infty$ are suprema over $n$, which equal the limits because the sequences are nondecreasing and bounded. Monotonicity in $i$ is Monotone/Antitone with respect to $\preceq$. Smallest minimizers, maxima and minima are IsLeast/IsGreatest characterizations, never sInf on $\mathbb Z$.

Condition 1(a) is encoded as the coupling (14) itself, with one probability space per pair $i \preceq j$ and copies identified by their finite-dimensional distributions. Replacing it by the expectation inequality (15), or the partial order by a total order, would change the theorem and is ruled out. Every goal statement asserts the existence of the levels it constrains before constraining them, so no conclusion holds vacuously. The standing hypotheses together with Condition 1 are satisfiable: a one-state instance is checked in Lean.

Lemma 7 is not included because it is false as printed. A guarded version (for instance with $\nu \ge 2q^*$) would be a welcome contribution. Reusable parts include the uniformized Markov-modulated Poisson process, the coupling definition of stochastic monotonicity for a countable partially ordered state space, and the usual stochastic order on $\mathbb N$. Proofs of Lemma 9 and Theorem 7 that avoid Lemma 7 are particularly welcome.

Selected references

• J.-S. Song and P. Zipkin, Inventory Control in a Fluctuating Demand Environment, Operations Research 41(2):351–370, 1993. https://doi.org/10.1287/opre.41.2.351
• W. A. Massey, Stochastic orderings for Markov processes on partially ordered spaces, Mathematics of Operations Research 12(2):350–367, 1987. https://doi.org/10.1287/moor.12.2.350
• J. Keilson and A. Kester, Monotone matrices and monotone Markov processes, Stochastic Processes and their Applications 5(3):231–241, 1977. https://doi.org/10.1016/0304-4149(77)90033-3
• A. F. Veinott Jr., Optimal policy for a multi-product, dynamic, nonstationary inventory problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
• W. S. Lovejoy, Ordered solutions for dynamic programs, Mathematics of Operations Research 12(2):269–276, 1987. https://doi.org/10.1287/moor.12.2.269

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 partially observed Markov decision process (POMDP) models a controller that cannot see the state of the system it controls. It sees only noisy observations, and so it acts on a belief: a probability vector over the hidden states. Machine maintenance, medical screening, quality control and search problems all have this form. The dynamic program of a POMDP lives on the simplex of beliefs, a continuum, so computing exact optimal policies is expensive even when the state, action and observation sets are small. Structural results reduce that cost. A value function that is monotone in the belief, or a policy known to dominate a cheap reference policy, shrinks the space a computation must search. Such results also explain the model: they say when one belief is "better" than another.

W. S. Lovejoy, Some Monotonicity Results for Partially Observed Markov Decision Processes (Operations Research 35(5):736–743, 1987), provides such results by ordering beliefs with the monotone likelihood ratio (MLR) order instead of first-order stochastic dominance.

Timeline. Smallwood and Sondik (1973) set out the finite POMDP and its piecewise-linear value functions. White (1979, 1980) obtained monotone policies and values for machine replacement, for single-stage problems, and for the completely observed and completely unobserved extremes, all under first-order stochastic dominance. Albright (1979) treated the two-state case, where the usual orders coincide. Whitt (1979, 1982) developed the likelihood-ratio orders and showed that they are preserved by Bayesian updating. Lovejoy (1987) combined these into general monotonicity results for finite POMDPs, and the MLR order has since become the standard tool for structural results in POMDPs.

Setting

Let $S=\{1,\dots,n\}$ (states) and $O=\{1,\dots,m\}$ (observations) carry their natural orders, and let $A$ be a finite, completely ordered action set. For a finite chain $X$, $\Pi(X)$ is the set of probability vectors on $X$. For $\pi,\pi'\in\Pi(X)$, $\pi\ge_s\pi'$ (first-order stochastic dominance) means $\sum_{i\ge q}\pi_i\ge\sum_{i\ge q}\pi'_i$ for every $q$. $\pi\ge_r\pi'$ (MLR order) means $\pi_i\pi'_{i'}\ge\pi_{i'}\pi'_i$ whenever $i\ge i'$. For matrices $f,g$ on $X\times Y$, $f\ge_{tp}g$ means $f(x\vee x',y\vee y')\,g(x\wedge x',y\wedge y')\ge f(x,y)\,g(x',y')$ for all pairs, and $f$ is TP₂ if $f\ge_{tp}f$.

In each period the decision maker in state $s_t=i$ chooses $a\in A$ and receives the reward $g(i,a)$. The state moves to $j$ with probability $p^a_{ij}$ (matrix $P^a$), and an observation $k$ arrives with probability $r^a_{jk}$ (matrix $R^a$, with row $r^a(j)\in\Pi(O)$), generated by the new state $j$ and the action $a$. The paper assumes $r^a_{jk}>0$ throughout. The discount factor is $\beta\ge 0$. From a belief $\pi$, the observation $k$ has probability $\sigma(k;\pi,a)=\sum_{i,j}\pi_i p^a_{ij}r^a_{jk}$, and the posterior is the Bayes update $T_j(\pi,a,k)=\sum_i\pi_ip^a_{ij}r^a_{jk}/\sigma(k;\pi,a)$. With

$$h(\pi,a,V)=\sum_{i}\pi_i g(i,a)+\beta\sum_{k}\sigma(k;\pi,a)\,V(T(\pi,a,k)),$$

a finite horizon $N$ with salvage value $g_s$ gives the optimal values $V^*_{N+1}(\pi)=\sum_i\pi_ig_s(i)$ and $V^*_t(\pi)=\max_a h(\pi,a,V^*_{t+1})$. For $N=\infty$ and $0<\beta<1$, $V^*$ is the bounded solution of $V^*(\pi)=\max_a h(\pi,a,V^*)$. The myopic actions are $\alpha(\pi)=\operatorname{argmax}_a\sum_i\pi_ig(i,a)$.

Formalization targets

Goal: Proposition 2 (myopic lower bound)

Under (a) $g_s$ nondecreasing, (b) $g(\cdot,a)$ nondecreasing, (c) $P^a\ge_{tp}P^{a'}$ for $a\ge a'$, (d) $r^a(j)\ge_r r^a(j')$ for $j\ge j'$, (e) $r^a(j)\ge_s r^{a'}(j)$ for $a\ge a'$, and (f) $r^a_{jk}r^{a'}_{j'k}\ge r^{a'}_{jk}r^a_{j'k}$ for $a\ge a'$, $j\ge j'$: for every $t\le N$ (finite horizon), or for the infinite horizon with $0<\beta<1$, and every $\pi\in\Pi(S)$,

$$\forall\,\delta^*(\pi)\ \exists\,\alpha(\pi)\le\delta^*(\pi),\qquad \forall\,\alpha(\pi)\ \exists\,\delta^*(\pi)\ge\alpha(\pi),$$

where $\delta^*(\pi)$ ranges over the maximizers of $a\mapsto h(\pi,a,V^*_{t+1})$ (resp. $h(\pi,a,V^*)$).

Milestone: Proposition 1 (MLR-monotone values)

Under (a)–(d) with every $P^a$ TP₂: $\pi\ge_r\pi'$ in $\Pi(S)$ implies $V^*_t(\pi)\ge V^*_t(\pi')$ for $t=1,\dots,N+1$, and, without (a), $V^*(\pi)\ge V^*(\pi')$ for $N=\infty$.

Supporting milestones

The ordering facts behind both propositions: MLR implies stochastic dominance (§1), Lemma 1.1 (characterization of $\ge_s$), Lemma 1.3 (TP₂ prediction preserves $\ge_r$), Lemma 1.2 (the Bayes update is MLR-monotone in the observation, the prior and the action), the stochastic monotonicity of $\sigma$ in the belief (proof of Proposition 1) and in the action (Lemma 2.3), the comparison of $h$-increments with myopic increments (proof of Proposition 2), and Lemma 2.2 (dominated increments order maximizer sets).

Significance

The result. Proposition 2 makes the myopic policy, which solves a one-stage problem, a lower bound on an optimal policy for every belief and every period. In a search over policies, actions below $\alpha(\pi)$ can be discarded. When $g$ also has isotone differences, $\alpha$ is nondecreasing, and the optimal policy is bounded below by a monotone function that is easy to compute. Proposition 1 gives MLR-monotone value functions, the input to many later structural results for POMDPs. Lemma 1.2 records the fact behind it: Bayesian updating respects the MLR order, while first-order stochastic dominance does not survive conditioning.

Formalizing it. These results are proved on paper. This mission produces machine-checked proofs, together with a reusable finite-POMDP layer (belief update, observation probabilities, Bellman operator, finite- and infinite-horizon values) and a library of the stochastic orders on finite chains. One statement in the paper is wrong: the printed "only if" direction of Lemma 1.2(1) is false. The mission states only the direction that is true and used.

Difficulty

The obvious induction on $t$ for Proposition 1 needs $k\mapsto V(T(\pi,a,k))$ to be nondecreasing and $\sigma(\pi,a)$ to increase with $\pi$. Both need a belief order that conditioning preserves. Under first-order stochastic dominance the posterior is not monotone in the prior, and the paper's counterexample (p. 740) shows that the induction then fails. The MLR order repairs this, but proving that the prediction step preserves it (Lemma 1.3) requires a total-positivity composition argument (Karlin–Rinott, Theorem 2.4) on product lattices. For Proposition 2 the difficulty is to compare continuation values across actions: the observation distribution and the posterior both change with the action, and two separate orderings (Lemma 2.3 and Lemma 1.2(3)) must be combined before the maximizer comparison applies. The infinite-horizon parts additionally need the Bellman fixed point characterized well enough to pass monotonicity to the limit.

Formalization scope

Everything is finite, so all probabilities and expectations are finite sums and no measure theory is involved. States, observations and actions are finite nonempty types with a LinearOrder (any finite chain is isomorphic to $\{1,\dots,n\}$). $\Pi(X)$ is Mathlib's stdSimplex ℝ X. The orders $\ge_s,\ge_r,\ge_{tp}$ are plain relations (StochGE, MLRGE, TPGE) with the larger argument first, and every statement assumes simplex membership explicitly. The standing assumptions (stochastic rows of $P^a$ and $R^a$, $r^a_{jk}>0$, $\beta\ge0$) are fields of the structure POMDP. $V^*_t$ is computed by recursion (3) counted in steps to go, Vstar gs N t = valueToGo gs (N+1-t). The infinite-horizon $V^*$ is any function bounded on $\Pi(S)$ that solves the Bellman equation there. For $0<\beta<1$ such a function exists and is unique on $\Pi(S)$, by contraction. The equivalence between recursion (3) and the optimum over history-dependent strategies is cited by the paper from the literature and is not part of this mission. Maximizer sets (argmaxSet) carry the "for all $\delta^*$ / there exists $\alpha$" quantifiers. Both halves of each part of Proposition 2 are $\forall\exists$ statements.

The goal is not to be read with $V^*_{t+1}$ or $V^*$ replaced by an arbitrary, or an arbitrary nondecreasing, value function. That reading would reduce Proposition 2 to Lemma 2.2 plus a hypothesis. The goal quantifies only over the value functions of recursion (3) and over bounded Bellman solutions.

A complete development needs finite total-positivity composition (Mathlib's four functions theorem is the natural starting point), Abel summation for Lemma 1.1, and a contraction argument for the infinite horizon. The order library and the finite POMDP layer are reusable beyond this paper. Proofs of any milestone are welcome, as are alternative arguments for Lemma 1.3.

Selected references

• W. S. Lovejoy, Some Monotonicity Results for Partially Observed Markov Decision Processes, Operations Research 35(5):736–743, 1987. https://doi.org/10.1287/opre.35.5.736
• R. D. Smallwood and E. J. Sondik, The Optimal Control of Partially Observable Markov Processes over a Finite Horizon, Operations Research 21(5):1071–1088, 1973. https://doi.org/10.1287/opre.21.5.1071
• W. Whitt, A Note on the Influence of the Sample on the Posterior Distribution, Journal of the American Statistical Association 74:424–426, 1979.
• W. Whitt, Multivariate Monotone Likelihood Ratio and Uniform Conditional Stochastic Order, Journal of Applied Probability 19:695–701, 1982.
• S. Karlin and Y. Rinott, Classes of Orderings of Measures and Related Correlation Inequalities. I. Multivariate Totally Positive Distributions, Journal of Multivariate Analysis 10(4):467–498, 1980. https://doi.org/10.1016/0047-259X(80)90065-2
• C. White, Optimal Control-limit Strategies for a Partially Observed Replacement Problem, International Journal of Systems Science 10:321–331, 1979 (the machine-replacement model of §5).
• S. C. Albright, Structural Results for Partially Observable Markov Decision Processes, Operations Research 27(5):1041–1053, 1979. https://doi.org/10.1287/opre.27.5.1041