Dynamic Programming

Motivation

Chapter I of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) opens the book with a multi-stage allocation process: a resource is divided, stage after stage, between two activities, each of which yields an immediate return and leaves behind a depleted remainder that is re-divided at the next stage. The chapter uses this process as its prototype for "a number of multi-stage processes, of diverse origin, but similar analytic structure" (§ 8, p. 11), and the techniques it introduces here — the functional equation of the infinite process, successive approximations, approximation in policy space, transfer of convexity and concavity through the recurrence, and a stability estimate — reappear throughout the book and in the later theory of Markov decision processes.

When the number of stages is large, Bellman replaces the finite sequence of recurrences by a single equation for the infinite process. As the book stresses (p. 11), this replacement is only useful once one knows that the equation has a solution and possesses "no extraneous solutions". This mission formalizes that existence and uniqueness theorem and the chapter's main structural results that rest on it.

Setting

A quantity $x \ge 0$ is split into $y \in [0,x]$, assigned to a first activity with return $g(y)$, and $x - y$, assigned to a second activity with return $h(x-y)$. After the stage the first allocation has been reduced to $ay$ and the second to $b(x-y)$, and the process continues with the quantity $ay + b(x-y)$. Writing

$$T(f,y) = g(y) + h(x-y) + f\big(ay + b(x-y)\big),$$

the total return $f(x)$ of the infinite process satisfies the allocation equation (Bellman's (8.1))

$$f(x) = \max_{0 \le y \le x} T(f,y), \qquad x \ge 0.$$

The standing hypotheses of Chapter I, Theorem 1 are:

1. $g$ and $h$ are continuous on $[0,\infty)$ and $g(0) = h(0) = 0$;
2. with $m(x) = \max_{0 \le y \le x} \max(|g(y)|, |h(y)|)$ and $c = \max(a,b)$, the series $\sum_{n=0}^\infty m(c^n x)$ converges for every $x \ge 0$;
3. $0 \le a < 1$ and $0 \le b < 1$.

The successive approximations from an initial function $f_0$ are $f_{N+1}(x) = \max_{0 \le y \le x} T(f_N, y)$. A policy is a function $y_0(x)$ with $0 \le y_0(x) \le x$; its return is the total of the stage returns obtained by using $y_0$ at every stage.

In Lean all objects live in the namespace BellmanDP.Allocation: allocT is $T$, allocM is $m$, AllocationHyp g h a b bundles the three hypotheses, IsAllocationSolution g h a b f is the equation with the maximum attained, allocIter is the sequence $f_N$, and policyReturn is the return of a policy.

Formalization targets

Goal: Chapter I, Theorem 1

Under the three hypotheses, there is a function $f$ with

$$f(x) = \max_{0 \le y \le x}\big[g(y) + h(x-y) + f(ay + b(x-y))\big] \quad (x \ge 0), \qquad f(0) = 0,\ f \text{ continuous at } 0,$$

this $f$ is continuous on $[0,\infty)$, and every solution continuous at $0$ with value $0$ there coincides with $f$ on $[0,\infty)$.

Milestones

1. Theorem 2 — from any $f_0$ continuous on $[0,\infty)$ with $f_0(0) = 0$, the successive approximations converge to $f$ uniformly on every finite interval.
2. Theorem 3 — started from the return of a continuous policy, the successive approximations increase monotonically and converge to $f$ uniformly on every finite interval.
3. Lemma 1 — if $G(x,y)$ is jointly concave on $x,y \ge 0$, then $x \mapsto \max_{0 \le y \le x} G(x,y)$ is concave.
4. Theorem 4 — if $g$ and $h$ are convex, $f$ is convex and for each $x$ the maximum is attained at $y = 0$ or $y = x$.
5. Theorem 5 — if $g$ and $h$ are strictly concave, $f$ is strictly concave and the maximizing $y$ is unique for every $x$.
6. Theorem 9 — for the general equation $f(x) = \max_{0\le y\le x}[u(x,y) + f(ay+b(x-y))]$, the continuous solutions for returns $u$ and $v$ satisfy $|f(x) - F(x)| \le \sum_{n \ge 0} D(c^n x)$, where $D(z)$ is the maximum of $|u - v|$ over $0 \le y \le x \le z$.

Significance

Theorem 1 is what gives meaning to "the solution" of the allocation equation, which every later result of the chapter refers to. Without the side condition at $0$ uniqueness fails: when $g = h = 0$, every constant function and the indicator of $(0,\infty)$ solve the equation. Theorems 2 and 3 turn the existence proof into computational procedures (value iteration and policy improvement), and Theorem 3's monotonicity is the prototype of the policy-improvement property. Theorems 4 and 5 are the first structural results on optimal policies — all-or-nothing allocation under convex returns, a unique interior-or-boundary allocation under strictly concave returns — and Theorem 9 bounds the error made by replacing a return function with a simpler approximation.

These are classical results with published proofs in the book. No machine-checked version of any of them is known to this mission; the work is to formalize the proofs, building reusable infrastructure for functional equations of the form $f(x) = \max_{y \in D(x)}[r(x,y) + f(\tau(x,y))]$ with a contracting transition $\tau$.

Difficulty

The equation is not a contraction in the supremum norm on $[0,\infty)$: $g$ and $h$ may be unbounded, so no global Banach fixed-point argument applies. Control comes instead from the shrinking of the argument, $ay + b(x-y) \le cx$, which propagates a local estimate near $0$ out to every finite interval, and the summability hypothesis (1b) is what makes the resulting series converge uniformly on bounded sets. Uniqueness cannot come from a norm estimate either; it rests on continuity at $0$ alone. The maximum in the equation must be shown to be attained, which requires continuity of the limit function; the book notes (p. 13) that the monotone argument for nonnegative $g,h$ gives only a supremum. For Theorems 4 and 5, convexity and concavity must be carried through each approximation and preserved in the limit, and strict concavity must be recovered for the limit, where a pointwise limit of strictly concave functions is only concave.

Formalization scope

• Functions are ℝ → ℝ; only their values on $[0,\infty)$ enter any hypothesis or conclusion. Continuity at $0$ is one-sided (ContinuousWithinAt f (Set.Ici 0) 0), and uniqueness is equality on $[0,\infty)$.
• The maximum in the equation is encoded as IsGreatest of $\{T(f,y) : 0 \le y \le x\}$, so a solution attains its maximum at every $x \ge 0$. The maxima inside definitions ($m$, $f_{N+1}$, the triangle maximum of Theorem 9) are real suprema (sSup) of images of compact nonempty sets of continuous functions, which equal the book's maxima under the stated hypotheses.
• The later theorems refer to "the solution" of Theorem 1 by quantifying over solutions that are continuous at $0$ and vanish there; they never quantify over arbitrary solutions of the equation, for which the conclusions are false.
• Theorem 3's "converges uniformly" is stated uniformly on every finite interval $[0,R]$, the sense in which Theorem 2 and the series (11.10) used in its proof converge. Its initial function is defined explicitly as the series of stage returns along the trajectory of the policy.
• Theorem 4's "$y$ will equal $0$ or $x$" is stated as: an endpoint is a maximizer. It does not say every maximizer is an endpoint, which fails for $g = h = 0$.
• Each theorem carries its own parameter range as printed: $0 \le a, b < 1$ for Theorems 1–5, $0 < a, b < 1$ for Theorem 9.
• Not included: Theorem 6 (the policy structure under strict concavity, which uses $f'$ without a hypothesis making $f$ differentiable), Theorems 7 and 8 (explicit solutions), Theorem 10 (the multi-dimensional process), and Theorems 11–12 on Fibonacci search, which form a separate mission.

Welcome contributions: a general existence-and-uniqueness theorem for equations $f(x) = \sup_{y \in D(x)}[r(x,y) + f(\tau(x,y))]$ with $\|\tau(x,y)\| \le c\|x\|$, and a lemma that parametric maxima over $[0,x]$ of continuous functions are continuous in $x$.

Selected references

• R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics edition, 2010. https://doi.org/10.2307/j.ctv1nxcw0f — Chapter I, §§ 8–14 and 18, pp. 11–29.
• R. Bellman, "On the theory of dynamic programming", Proceedings of the National Academy of Sciences 38 (1952), 716–719. https://doi.org/10.1073/pnas.38.8.716

Motivation

In a Walrasian pure exchange economy, agents trade a fixed stock of $l$ commodities, and a price vector $p\in\mathbb R^l$ is a general equilibrium when aggregate excess demand vanishes. Existence of equilibrium (Arrow–Debreu, 1954) says nothing about how prices reach it. The classical tâtonnement model of Samuelson (1947), $dp_i/ds = c_i Z_i(p)$, is not derived from any optimization principle, and Scarf (1960) gave economies in which it is not globally stable; see also Smale's survey Dynamics in General Equilibrium Theory (JSTOR 1817235) and the chaotic tâtonnement examples of Bala–Majumdar (JSTOR 25054664).

Lindgren (doi:10.3390/analytics1010003) proposes instead that the economy as a whole chooses a price path by dynamic programming: it minimizes a running cost combining a quadratic transaction cost for price changes and the agents' aggregate minimal expenditure. From the resulting Hamilton–Jacobi–Bellman (HJB) equation the paper derives an evolution equation for the price velocity and a condition under which the value function acts as a Lyapunov function: the equilibrium is approached when price adjustments are large enough. This mission formalizes those derivations.

Setting

There are $l$ commodities and $n$ agents. Prices are vectors $p=(p_1,\dots,p_l)\in\mathbb R^l$, and the paper's implicit summation $x^iy_i=\sum_{i=1}^l x_iy_i$ is written $\langle x,y\rangle$. Agent $j$ has an expenditure function $e_j(p)$ (minimal cost of reaching a fixed utility level), and the market weighs agents with constants $\lambda_j>0$; the aggregate expenditure is

$$E(p)=\lambda^je_j(p)=\sum_{j=1}^n\lambda_je_j(p).$$

The economy controls the price velocity $v=dp/ds$ and minimizes the cost functional (eq. (7))

$$\int_t^T\Big(\tfrac12 m\langle v,v\rangle+E(p)\Big)\,ds,\qquad m>0,$$

whose value function is $J(t,p)$. The Hamiltonian (eq. (8)) is

$$H(v)=\tfrac12 m\langle v,v\rangle+E(p)+\langle\nabla J,v\rangle ,$$

the optimal policy (eq. (9)) is $v=-\tfrac1m\nabla J$, and the HJB equation (eq. (10)) reads

$$\frac{\partial J}{\partial t}=\frac1{2m}\langle\nabla J,\nabla J\rangle-E(p).$$

Here $\nabla$ always denotes the gradient with respect to prices. Shephard's lemma identifies the Hicksian demand of agent $j$ with $h^j=\nabla e_j$. For the stability analysis the paper runs time forward, which reverses the sign of the HJB equation: $\partial J/\partial s=-\frac1{2m}\langle\nabla J,\nabla J\rangle+E(p)$.

Formalization targets

Goal — Lyapunov stability condition (Section 3)

If $J$ is $C^1$ and solves the time-reversed HJB equation, and the price path follows the optimal policy $\dot p(s)=v(s)=-\frac1m\nabla J(s,p(s))$, then on any interval $[t,T]$ on which

$$E(p(s))<\tfrac32\,m\,\langle v(s),v(s)\rangle,$$

the function $s\mapsto J(s,p(s))$ is strictly decreasing; if moreover $J(T,p(T))=0$, it is strictly positive on $[t,T)$.

Milestones

1. Eq. (4): under the normalization $\langle p,p\rangle=1$, $\langle p,\dot p\rangle=0$.
2. Eq. (9): for $m>0$, $v$ minimizes $H$ if and only if $mv=-\nabla J$.
3. Eq. (10): the HJB equation $-\partial_tJ=\min_vH$ takes the explicit form above.
4. Eq. (12): for a $C^2$ solution of (10), $v=-\frac1m\nabla J$ satisfies

$$m\frac{\partial v_i}{\partial t}+\tfrac12 m\,\nabla_i\langle v,v\rangle=\nabla_iE .$$

5. Eq. (14): with Shephard's lemma, the right-hand side becomes $\sum_j\lambda_jh^j_i$.
6. Eq. (19): along the optimal path, $\dfrac{dJ}{ds}=E(p)-\tfrac32 m\langle v,v\rangle$.

Significance

The paper's contribution is the claim that price dynamics derived from an optimization principle are nonlinear and only conditionally stable, with stability requiring sufficiently fast price changes; the author connects this to volatility clustering in financial time series. The derivations in the paper are formal calculations with the regularity of $J$ left implicit. Formalizing them pins down exactly which smoothness assumptions each step needs (for instance, eq. (12) uses equality of mixed partial derivatives, hence a $C^2$ value function), and which facts are imported from outside (the HJB equation itself, Shephard's lemma). The resulting statements are reusable calculus facts about HJB equations with quadratic control cost.

Difficulty

Each step is a short computation on paper; the formal difficulty is in the calculus infrastructure: partial derivatives of functions on $\mathbb R\times\mathbb R^l$, symmetry of second derivatives, the chain rule along a curve, and turning a pointwise negative derivative into strict monotonicity on a closed interval. The HJB equation is taken as a hypothesis on $J$ rather than derived from the definition of the value function, because the paper asserts it without proof and a rigorous derivation would require viscosity-solution theory.

Formalization scope

All declarations live in the namespace LindgrenPriceDynamics. Prices are functions Fin l → ℝ; partial derivatives are Fréchet derivatives applied to standard basis vectors, and time derivatives are one-variable derivatives in the time argument. The value function is a function J : ℝ → (Fin l → ℝ) → ℝ whose joint regularity is stated for the uncurried map on ℝ × (Fin l → ℝ). The standing assumption $m>0$ is kept; positivity of $\lambda_j$ and $e_j$ is not needed by any stated conclusion and is not imposed. Prices are not restricted to the positive orthant. The goal's large-velocity hypothesis is satisfiable (e.g. $l=1$, $J=ap^2+cs$, $E=2a^2p^2/m+c$ with small $c>0$ on a bounded interval), so the goal is not vacuous.

Selected references

• J. Lindgren, General Equilibrium with Price Adjustments — A Dynamic Programming Approach, Analytics 1 (2022) 27–34. https://doi.org/10.3390/analytics1010003
• S. Smale, Dynamics in General Equilibrium Theory, American Economic Review 66 (1976) 288–294. https://www.jstor.org/stable/1817235
• H. Scarf, Some Examples of Global Instability of the Competitive Equilibrium, International Economic Review 1 (1960) 157–172.
• A. Mas-Colell, M. Whinston, J. Green, Microeconomic Theory, Oxford University Press, 1995.
• V. Bala, M. Majumdar, Chaotic Tatonnement, Economic Theory 2 (1992) 437–445. https://www.jstor.org/stable/25054664

Motivation

Approximate policy iteration and policy-gradient methods stop when they can no longer find a direction of improvement. Kakade and Langford (ICML 2002) asked what such a stopping point guarantees. Their algorithm, conservative policy iteration, halts at a policy $\pi$ for which no policy can improve much on $\pi$ as measured under a restart distribution $\mu$; the quantity that is small is the optimal policy advantage $\mathrm{OPT}(\mathbb A_{\pi,\mu})$. Theorem 6.2 of the paper translates this local condition into a global statement: the performance of $\pi$ is close to optimal, with a loss controlled by how well $\mu$ covers the states an optimal policy visits.

The bound is the origin of the distribution mismatch coefficient $\|d_{\pi^*,\tilde\mu}/\mu\|_\infty$, which reappears in the analysis of approximate dynamic programming (concentrability coefficients, Munos 2003), of conservative and trust-region methods, and of the convergence of policy gradient methods (Agarwal, Kakade, Lee, Mahajan 2021), where it governs the rate. The performance difference lemma (Lemma 6.1) used in its proof has become a standard tool of reinforcement learning theory.

Setting

A finite Markov decision process has a finite nonempty state set $S$, a finite nonempty action set $A$, transition probabilities $P(s';s,a)$ (for each $s,a$ a probability distribution over $s'$), a reward function $\mathcal R:S\times A\to[0,R]$ with $R>0$, and a discount factor $0\le\gamma<1$. A stochastic policy $\pi(a;s)$ is, for each state $s$, a probability distribution over actions. A state distribution is a probability vector $\mu$ on $S$.

The normalized value function is $V_\pi(s)=(1-\gamma)E[\sum_{t\ge0}\gamma^t\mathcal R(s_t,a_t)\mid\pi,s]$, where $s_0=s$, $a_t\sim\pi(\cdot;s_t)$ and $s_{t+1}\sim P(\cdot;s_t,a_t)$. The state–action value is $Q_\pi(s,a)=(1-\gamma)\mathcal R(s,a)+\gamma\sum_{s'}P(s';s,a)V_\pi(s')$ and the advantage is $A_\pi(s,a)=Q_\pi(s,a)-V_\pi(s)$. The discounted future state distribution from $\mu$ is

$$d_{\pi,\mu}(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s;\pi,\mu),\qquad s_0\sim\mu,$$

and the performance of $\pi$ from $\mu$ is $\eta_\mu(\pi)=\sum_s\mu(s)V_\pi(s)$.

The policy advantage of $\pi'$ with respect to $\pi$ and $\mu$ is $\mathbb A_{\pi,\mu}(\pi')=\sum_sd_{\pi,\mu}(s)\sum_a\pi'(a;s)A_\pi(s,a)$: the expected advantage of $\pi'$ over $\pi$ on the states $\pi$ itself visits. Its maximum over all stochastic policies is $\mathrm{OPT}(\mathbb A_{\pi,\mu})=\max_{\pi'}\mathbb A_{\pi,\mu}(\pi')$ (Definition 4.3). An optimal policy $\pi^*$ satisfies $V_\pi(s)\le V_{\pi^*}(s)$ for every policy $\pi$ and every state $s$. For nonnegative $f,g$ on $S$, $\|f/g\|_\infty=\max_sf(s)/g(s)$ (p. 5).

Formalization targets

Goal: Theorem 6.2 (p. 6)

If $\mathrm{OPT}(\mathbb A_{\pi,\mu})<\varepsilon$ and $\pi^*$ is optimal, then for every state distribution $\tilde\mu$

$$\eta_{\tilde\mu}(\pi^*)-\eta_{\tilde\mu}(\pi)\le\frac{\varepsilon}{1-\gamma}\left\|\frac{d_{\pi^*,\tilde\mu}}{d_{\pi,\mu}}\right\|_\infty\le\frac{\varepsilon}{(1-\gamma)^2}\left\|\frac{d_{\pi^*,\tilde\mu}}{\mu}\right\|_\infty.$$

The goal states both inequalities and the outer bound. The evaluation distribution $\tilde\mu$ is arbitrary and unrelated to the restart distribution $\mu$; taking $\tilde\mu=D$, the start distribution, gives Corollary 4.5 (p. 5).

Milestone: Lemma 6.1 (p. 6)

For any policies $\tilde\pi$, $\pi$ and any starting distribution $\mu$,

$$\eta_\mu(\tilde\pi)-\eta_\mu(\pi)=\frac{1}{1-\gamma}E_{(a,s)\sim\tilde\pi d_{\tilde\pi,\mu}}\big[A_\pi(s,a)\big].$$

The states are weighted by the future state distribution of the new policy $\tilde\pi$, the advantage is that of the old policy $\pi$.

Significance

Theorem 6.2 is the quality guarantee for conservative policy iteration: combined with the paper's Theorem 4.4 (the algorithm stops with $\mathrm{OPT}(\mathbb A_{\pi,\mu})<2\varepsilon$ after polynomially many calls), it bounds the suboptimality of the returned policy for any target distribution, independently of the size of the state space except through the mismatch coefficient. It also explains the role of the restart distribution: a more uniform $\mu$ makes $\|d_{\pi^*,\tilde\mu}/\mu\|_\infty$ small. Lemma 6.1 is used throughout later theory, from trust-region policy optimization to the global convergence of policy gradient methods.

Both results are proved in the paper, with short arguments. The contribution of this mission is a machine-checked version of the infinite-horizon discounted statement in the paper's normalization, with the $\|\cdot\|_\infty$ ratios handled exactly, including states where a denominator vanishes. Neither the discounted performance difference lemma for stochastic policies nor the distribution mismatch bound is known to be formalized in Mathlib; a finite-horizon performance difference identity has been formalized separately and is a different statement.

Difficulty

The mathematics is short; the difficulty is in the infinite-horizon bookkeeping. The value function and $d_{\pi,\mu}$ are infinite series, and Lemma 6.1 relates the series of two different policies: its natural one-line argument uses the Bellman equation for $V_\pi$, which is not the definition here, together with interchanges of infinite sums over time with finite sums over states and actions, each of which needs summability. Theorem 6.2 then needs two facts that are not stated as results in the paper: that $\mathrm{OPT}(\mathbb A_{\pi,\mu})$ equals $\sum_sd_{\pi,\mu}(s)\max_aA_\pi(s,a)$ (the supremum over policies is attained by a greedy policy, and $\max_aA_\pi(s,a)\ge0$), and that $d_{\pi,\mu}(s)\ge(1-\gamma)\mu(s)$. Reading the $\ell_\infty$ ratio with real division would give a false statement when a denominator is zero; the statement avoids this.

Formalization scope

States and actions are finite nonempty types; policies and kernels are real-valued functions π s a (the paper's $\pi(a;s)$) and P s a s' (the paper's $P(s';s,a)$), with their distribution properties as explicit hypotheses. The published definitions IsTransitionKernel, IsPolicy, InducedTransition, OccupationDist, InducedReward and PolicyValue from the Foundations of Machine Learning series are reused; $V_\pi$ is $(1-\gamma)$ times PolicyValue, the defining series. $\mathrm{OPT}$ is the supremum of the policy advantages over stochastic policies, which is the paper's maximum. Optimality of $\pi^*$ is relative to stationary stochastic policies, the paper's policy class; the existence of an optimal policy (the paper's "well known result", p. 2) is not part of this mission.

Every hypothesis is explicit: rewards in $[0,R]$ with $R>0$, $0\le\gamma<1$, $P$ a kernel, $\pi$ and $\pi^*$ stochastic policies, $\mu$ and $\tilde\mu$ state distributions. Each $\|f/g\|_\infty$ bound is stated multiplicatively: "$X\le K\|f/g\|_\infty$" is "$X\le KC$ for every $C$ with $f(s)\le Cg(s)$ for all $s$". When some $g(s)=0<f(s)$ no such $C$ exists and the bound is empty, which matches $\|f/g\|_\infty=+\infty$; no full-support assumption is made on $\mu$ or $\tilde\mu$. The hypothesis $\mathrm{OPT}(\mathbb A_{\pi,\mu})<\varepsilon$ is on the supremum itself, not on the closed form $\sum_sd_{\pi,\mu}(s)\max_aA_\pi(s,a)$, which is a step of the proof; a formalization that assumed the closed form, or that divided by $d_{\pi,\mu}$ in real arithmetic, would not be this theorem. The proof of the theorem uses only that $\pi^*$ is a policy; optimality is kept as a hypothesis because the paper states it.

The proof on p. 7 twice writes $d_{\pi,\mu}(s)\le(1-\gamma)\mu(s)$; the inequality it uses, and the one stated on p. 5, is $d_{\pi,\mu}(s)\ge(1-\gamma)\mu(s)$. This slip is in the proof, not in the statement. Pages are PDF pages; the paper has no printed page numbers.

Useful reusable infrastructure: summability and Bellman equations for the normalized discounted value, $d_{\pi,\mu}$ as a probability distribution with $d_{\pi,\mu}\ge(1-\gamma)\mu$, and attainment of $\mathrm{OPT}$ by a greedy policy. Contributions of any of these as separate lemmas are welcome.

Selected references

• S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning (ICML), 2002. https://dl.acm.org/doi/10.5555/645531.656005
• R. Munos, Error Bounds for Approximate Policy Iteration, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041903
• A. Agarwal, S. Kakade, J. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, Journal of Machine Learning Research 22(98), 2021. https://jmlr.org/papers/v22/19-736.html
• J. Schulman, S. Levine, P. Abbeel, M. Jordan, P. Moritz, Trust Region Policy Optimization, ICML 2015. https://arxiv.org/abs/1502.05477

Motivation

The periodic-review inventory problem with a fixed ordering cost is one of the basic models of operations research. A firm reviews its stock once per period, may order at a cost $K$ per order plus a unit cost, and then faces a random demand; unmet demand is backlogged. Scarf (1960) and Iglehart (1963) showed that for this model an $(s, S)$ policy is optimal: order up to $S$ whenever the stock falls below $s$, and otherwise do nothing. That result tells a manager what shape a good policy has, but not which pair $(s, S)$ to use.

Veinott and Wagner, Computing Optimal (s, S) Inventory Policies (Management Science 11 (1965) 525–552), gave the first practical algorithm for computing an optimal pair when demand is discrete. The algorithm rests on a closed form, their Eq. (11), for the discounted cost of an arbitrary stationary $(s, S)$ policy, obtained by a renewal argument in their Section 3. The same closed form, in the undiscounted limit, is the classical expression of the long-run average cost of an $(s, S)$ policy used throughout inventory theory textbooks.

Timeline:

• 1958: Arrow, Karlin and Scarf collect the early dynamic inventory models.
• 1960: Scarf proves optimality of $(s, S)$ policies in the finite-horizon model via $K$-convexity.
• 1963: Iglehart extends optimality to the infinite-horizon model.
• 1965: Veinott and Wagner derive the renewal closed form (10)–(11) and the bounds and search procedure built on it.

Setting

Demands $\xi_1, \xi_2, \dots$ are independent random variables on $\{0, 1, 2, \dots\}$ with common distribution $\varphi$, $\varphi(k) = \Pr(\xi_t = k)$. Write $\varphi^i$ for the $i$-fold convolution of $\varphi$ ($\varphi^0$ is the point mass at $0$) and $\Phi^i(k) = \sum_{t=0}^{k}\varphi^i(t)$ for its distribution function, so $\Phi^0 \equiv 1$.

In period $t$ the stock before ordering is $X_t \in \mathbb Z$ and the stock after ordering is $Y_t \ge X_t$; then $X_{t+1} = Y_t - \xi_t$. With the unit purchase cost eliminated as in the paper's Eq. (2), the cost of period $t$ is $K\delta(Y_t - X_t) + G_\alpha(Y_t)$, where $K \ge 0$ is the set-up cost, $\delta(0) = 0$, $\delta(z) = 1$ for $z > 0$, and $G_\alpha : \mathbb Z \to \mathbb R$ is the one-period cost. Period $t$ is discounted by $\alpha^{t-1}$ with $0 \le \alpha < 1$.

A stationary $(s, S)$ policy, for integers $s \le S$, sets $Y_t = S$ if $X_t < s$ and $Y_t = X_t$ otherwise. Its total expected discounted cost from $X_1 = x$ is

$$f(x \mid s, S) = \sum_{t=1}^{\infty} \alpha^{t-1} E\bigl[K\delta(Y_t - X_t) + G_\alpha(Y_t)\bigr],$$

and its equivalent cost per period is $a_\alpha(x \mid s, S) = (1 - \alpha) f(x \mid s, S)$.

The renewal quantities are

$$m_\alpha(k) = \sum_{i=1}^{\infty}\alpha^i\varphi^i(k), \qquad M_\alpha(k) = \sum_{i=1}^{\infty}\alpha^i\Phi^i(k),$$

the latter being the discount renewal function,

$$L_\alpha(x, d) = G_\alpha(x) + \sum_{i=1}^{\infty}\sum_{k=0}^{d}\alpha^i G_\alpha(x - k)\varphi^i(k), \qquad r_\alpha(d) = \sum_{i=1}^{\infty}\alpha^i\bigl[\Phi^{i-1}(d) - \Phi^i(d)\bigr].$$

If $T(d)$ is the first period in which cumulative demand exceeds $d$, then $L_\alpha(x, d)$ is the expected discounted one-period cost over periods $1, \dots, T(d)$ from stock $x$ without ordering, and $r_\alpha(d) = E[\alpha^{T(d)}]$.

Formalization targets

Goal: Eq. (11)

With $D = S - s$,

$$a_\alpha(x \mid s, S) = \begin{cases} \dfrac{L_\alpha(S, D) + K}{1 + M_\alpha(D)} & x < s, \\[2ex] (1 - \alpha)L_\alpha(x, x - s) + \dfrac{L_\alpha(S, D) + K}{1 + M_\alpha(D)}\, r_\alpha(x - s) & x \ge s. \end{cases}$$

Milestones

1. Appendix §1: $M_\alpha(k) < \infty$ for $0 \le \alpha \le 1$ with $\alpha\varphi(0) < 1$.
2. Eq. (8): $L_\alpha(x, d) = G_\alpha(x) + \sum_{j=0}^{d} G_\alpha(x - j)m_\alpha(j)$.
3. Eq. (9): $r_\alpha(d) = \alpha - (1 - \alpha)M_\alpha(d)$.
4. The renewal equation $f(S) = L_\alpha(S, D) + Kr_\alpha(D) + f(S)r_\alpha(D)$.
5. $f(x) = K + f(S)$ for $x < s$.
6. $f(x) = L_\alpha(x, x - s) + Kr_\alpha(x - s) + f(S)r_\alpha(x - s)$ for $x \ge s$.
7. Eq. (10): the closed form of $f$ with denominator $1 - r_\alpha(D)$.

Significance

Eq. (11) turns the cost of an $(s, S)$ policy, an infinite series over the trajectories of a controlled Markov chain, into a finite expression in $G_\alpha$, $K$ and the renewal sequence $m_\alpha$, which the paper computes by a one-line recursion. Everything in the paper's Section 4 builds on it: the search for an optimal pair minimizes $a_\alpha(\cdot \mid s, S)$ over a finite box, and the undiscounted limit $\alpha \to 1$ gives the long-run average cost $(L_1(S, D) + K)/(1 + M_1(D))$.

The result is classical and proved in the paper. What this mission adds is a machine-checked derivation from the definition of the policy's expected cost, including the renewal step, which the paper states in one sentence ("a renewal of the process takes place"). It also produces a reusable Lean layer: discrete convolution powers, the discount renewal function, and the law of an $(s, S)$-controlled inventory chain. To the best of our knowledge none of these is formalized in Mathlib or on the platform.

Difficulty

The paper's argument conditions on the random time $T(D)$ at which the process renews and uses the strong Markov property at that time. In the formalization, $f$ is defined as a sum over periods of expectations under the law of $X_t$. Relating that sum to one that splits at the random time $T(D)$ requires either a stopping-time decomposition of the chain or an explicit accounting of the law of $X_t$ before and after the first order. Neither is a direct computation. A second difficulty is the interchange of the infinite sum over periods with the sum over states $y \in \mathbb Z$, which has infinitely many states reachable (demand is unbounded below). The renewal equation (milestone 4) alone does not determine $f(S)$ without the fact that $r_\alpha(D) < 1$ for $\alpha < 1$, which comes from (9).

Formalization scope

• Namespace VeinottWagnerSS.RenewalCost. Stock levels are integers, demands natural numbers; $x - s$ and $D = S - s$ enter $L_\alpha$, $M_\alpha$, $r_\alpha$ through Int.toNat, which is exact because the statements assume $s \le x$ or $s \le S$.
• Reduced model. The primitives are $G_\alpha$, $K$, $\alpha$ and $\varphi$, as in the paper's Eq. (2): the unit purchase cost is set to $0$ and the holding–penalty cost is replaced by $G_\alpha$.
• Demand is a real function $\varphi : \mathbb N \to \mathbb R$, non-negative and summing to $1$.
• The cost $f$ is the expected discounted cost of the controlled chain: the law of $X_t$ is built recursively from $X_1 = x$ and the transition $\Pr(X_{t+1} = z \mid X_t = y) = \varphi(Y(y) - z)$. It is not defined by (10) or by the renewal equations, and not as the solution of a fixed-point equation. A formalization in which any of milestones 4–7 or the goal holds by definition is ruled out.
• Series are real tsums. $L_\alpha$ is defined by the series (7) and $r_\alpha$ by the first line of (9), i.e. through the law $\Pr[T(d) = i] = \Phi^{i-1}(d) - \Phi^i(d)$; the paper's derivations of these series from $T(d)$ are not formalized. For $\alpha < 1$ all series converge for every $G_\alpha$, because after period $1$ the stock after ordering lies in the finite set $\{S\} \cup [s, \max(x, S)]$.
• Hypotheses. Milestones 1–3 assume $0 \le \alpha \le 1$ and $\alpha\varphi(0) < 1$, the paper's standing assumption on p. 533. Milestones 4–7 and the goal assume $0 \le \alpha < 1$, $K \ge 0$ and $s \le S$. The paper's standing assumptions that $G_\alpha$ is convex and tends to $+\infty$ as $|y| \to \infty$ are not imposed: the statements hold for every $G_\alpha$ when $\alpha < 1$, and the paper's derivation does not use them. This is a disclosed generalization.
• Printed slips. None found in the formalized statements.
• Not formalized: the recursion (A1) for $m_\alpha$, the limit (12) as $\alpha \to 1$, and the stationary analysis (13)–(20).

Contributions welcome: proofs of the milestones, general lemmas on discrete renewal sequences and convolution powers, and a first-passage decomposition for integer-valued Markov chains, which is reusable beyond this mission.

Selected references

• A. F. Veinott Jr. and H. M. Wagner, Computing Optimal (s, S) Inventory Policies, Management Science 11(5), 525–552, 1965. https://doi.org/10.1287/mnsc.11.5.525
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• 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
• K. J. Arrow, S. Karlin and H. Scarf, Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.

Motivation

Approximate policy iteration and policy gradient methods are the two classical families of reinforcement learning algorithms that work with approximate, sampled information instead of an exact model. Kakade and Langford (ICML 2002) observed that neither family answers three basic questions: is there a performance measure that is guaranteed to improve at every step, how hard is it to verify that an update improves it, and what performance is reached after a reasonable number of updates. Greedy approximate policy iteration can make the policy worse when the value estimates are slightly wrong at a few states, and policy gradient methods can stall on plateaus where estimating the gradient needs an enormous number of samples.

Their answer is conservative policy iteration: instead of jumping to a greedy policy, move only a controlled fraction of the way toward it, with a step size chosen from an estimate of how much the greedy policy helps. The paper proves that this update improves a restart-distribution performance measure monotonically, terminates after a number of iterations that depends only on the reward range and the target accuracy, and stops at a policy that the greedy oracle can no longer improve by much. The idea is the direct ancestor of trust-region and proximal policy optimization methods (TRPO, Schulman et al. 2015; PPO, Schulman et al. 2017), whose improvement bounds are refinements of the paper's Theorem 4.1.

Setting

A finite Markov decision process has a finite nonempty set of states $S$, a finite nonempty set of actions $A$, transition probabilities $P(s';s,a)$ (for each state $s$ and action $a$, a probability distribution over next states $s'$), a reward function $\mathcal R : S\times A\to[0,R]$ with $R>0$, and a discount factor $0\le\gamma<1$. A stochastic policy $\pi(a;s)$ gives, for each state $s$, a probability distribution over actions.

The normalized value of $\pi$ from $s$ is $V_\pi(s) = (1-\gamma)E[\sum_{t\ge0}\gamma^t\mathcal R(s_t,a_t)\mid\pi,s]$, where $s_0=s$, $a_t\sim\pi(\cdot\,;s_t)$, $s_{t+1}\sim P(\cdot\,;s_t,a_t)$; it lies in $[0,R]$. The state-action value is $Q_\pi(s,a) = (1-\gamma)\mathcal R(s,a)+\gamma E_{s'\sim P(s';s,a)}[V_\pi(s')]$ and the advantage is $A_\pi(s,a) = Q_\pi(s,a)-V_\pi(s)\in[-R,R]$.

For a state distribution $\mu$ (a restart distribution), the discounted future state distribution is $d_{\pi,\mu}(s) = (1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s;\pi,\mu)$ (eq. (2.1)), and the performance measure is $\eta_\mu(\pi) = E_{s\sim\mu}[V_\pi(s)]$.

The policy advantage of a policy $\pi'$ with respect to $\pi$ and $\mu$ is

$$\mathbb A_{\pi,\mu}(\pi') = E_{s\sim d_{\pi,\mu}}\big[E_{a\sim\pi'(a;s)}[A_\pi(s,a)]\big],$$

and $\mathrm{OPT}(\mathbb A_{\pi,\mu}) = \max_{\pi'}\mathbb A_{\pi,\mu}(\pi')$. The conservative update (4.1) is $\pi_{new} = (1-\alpha)\pi+\alpha\pi'$ with $\alpha\in[0,1]$. An $\varepsilon$-greedy policy chooser $G_\varepsilon$ (Definition 4.3) returns, for every policy $\pi$, a policy $\pi'$ with $\mathbb A_{\pi,\mu}(\pi')\ge\mathrm{OPT}(\mathbb A_{\pi,\mu})-\varepsilon$.

Conservative policy iteration (§5) starts from any policy and repeats: call $G_\varepsilon(\pi,\mu)$ to get $\pi'$; form an $\frac\varepsilon3$-accurate estimate $\hat{\mathbb A}$ of $\mathbb A_{\pi,\mu}(\pi')$ from $\mu$-restarts; if $\hat{\mathbb A}<\frac{2\varepsilon}3$, stop and return $\pi$; otherwise apply (4.1) with $\alpha = \frac{(1-\gamma)(\hat{\mathbb A}-\varepsilon/3)}{4R}$ and repeat.

Formalization targets

Goal: Theorem 4.4 (p. 5)

With probability at least $1-\delta$, conservative policy iteration (i) strictly improves $\eta_\mu$ with every policy update, (ii) stops after at most $72R^2/\varepsilon^2$ policy updates, and (iii) returns a policy $\pi$ with

$$\mathrm{OPT}(\mathbb A_{\pi,\mu}) < 2\varepsilon.$$

The estimation step is represented by its guarantee: each reached loop's estimate fails to be $\frac\varepsilon3$-accurate with probability at most $\delta/(N+1)$, $N=\lfloor72R^2/\varepsilon^2\rfloor$.

Milestones

Lemma 6.1 (p. 6), the performance difference identity:

$$\eta_\mu(\tilde\pi)-\eta_\mu(\pi) = \frac1{1-\gamma}E_{(a,s)\sim\tilde\pi d_{\tilde\pi,\mu}}[A_\pi(s,a)].$$

Theorem 4.1 (p. 4), with $\varepsilon=\max_s|E_{a\sim\pi'(a;s)}[A_\pi(s,a)]|$ and all $\alpha\in[0,1]$:

$$\eta_\mu(\pi_{new})-\eta_\mu(\pi)\ge\frac{\alpha}{1-\gamma}\Big(\mathbb A-\frac{2\alpha\gamma\varepsilon}{1-\gamma(1-\alpha)}\Big).$$

Corollary 4.2 (p. 5): if $\mathbb A\ge0$, the step size $\alpha=\frac{(1-\gamma)\mathbb A}{4R}$ gives

$$\eta_\mu(\pi_{new})-\eta_\mu(\pi)\ge\frac{\mathbb A^2}{8R}.$$

Significance

Theorem 4.4 is the first guarantee of its kind for approximate reinforcement learning: the number of iterations is bounded by $72R^2/\varepsilon^2$, independent of the number of states and of the restart distribution, and every iteration provably helps. Lemma 6.1 is the standard performance difference lemma, used throughout the analysis of policy optimization, including natural policy gradient and trust-region methods; Theorem 4.1 is the prototype of the "surrogate objective minus a penalty" bound that TRPO refines.

These results are proved in the paper. As far as a search of the platform shows, none is formalized: the platform's finite-horizon performance difference lemma (Foster and Rakhlin's Lemma 13) is a different statement, for episodic problems with non-stationary policies. This mission produces machine-checked versions of the discounted performance difference identity, the conservative improvement bound with its exact constants, and the high-probability termination and quality guarantee of the algorithm, all on top of an explicit infinite-horizon model rather than an assumed Bellman equation.

Difficulty

The obvious argument for the improvement bound expands $\eta_\mu(\pi_{new})$ to first order in $\alpha$; that only gives $\frac{\alpha}{1-\gamma}\mathbb A+O(\alpha^2)$ with an unspecified constant, which cannot fix a step size. The exact bound needs control of how far the state distribution of the mixed policy drifts from that of the old policy, uniformly in time, and the performance difference identity is only useful once the states are weighted by the new policy's distribution. On the formal side, $V_\pi$ and $d_{\pi,\mu}$ are infinite discounted series, so summability, exchanges of sums and the identities $\sum_s d_{\pi,\mu}(s)=1$ and $\sum_a\pi(a;s)A_\pi(s,a)=0$ must all be established from the definitions. For Theorem 4.4, the algorithm is a random process whose policies depend on all earlier estimates; the argument has to be made pathwise on the event that every reached loop is accurate, together with a union bound over the loops that can be reached.

Formalization scope

Policies are functions π : S → A → ℝ with π s a the paper's $\pi(a;s)$, and P s a s' is $P(s';s,a)$; both are constrained by the published predicates IsPolicy and IsTransitionKernel. $V_\pi$ is $(1-\gamma)$ times the published series PolicyValue, so values are normalized as in the paper. $\mathrm{OPT}$ is a real supremum over all stochastic policies; the set is nonempty and bounded, and the maximum is attained. Every theorem carries the standing assumptions of §2: finite nonempty $S$ and $A$, a transition kernel, rewards in $[0,R]$ with $R>0$, $0\le\gamma<1$, and a state distribution $\mu$. In Corollary 4.2, $R$ is any upper bound on the rewards rather than necessarily the attained maximum.

In Theorem 4.4 the run is formalized pathwise, driven by arbitrary real random estimates on a probability space; the conclusion bounds the probability of the failure event by $\delta$. Two deviations from the printed statement are disclosed. First, (ii) is stated for policy updates: the proof bounds updates, and the algorithm calls $G_\varepsilon$ once more than it updates, so "at most $72R^2/\varepsilon^2$ calls" is off by one. Second, the per-loop failure budget is $\delta/(N+1)$, which covers the $N+1$ loops that may be reached. The Hoeffding estimate (5.1) is not formalized: as printed it concerns the $\frac\varepsilon6$-biased target, and its role is taken by the accuracy hypothesis. The step size is clipped at $1$, which never binds when the estimate is accurate. No trivializing reading is available: the accuracy hypothesis is satisfied by a perfect estimator and a $0$-greedy chooser exists, so the theorem is not vacuous, and strict improvement at every update is required, not merely nonnegative change.

Pages are PDF pages; the paper has no printed page numbers.

A complete development needs summability and algebra of discounted occupation measures, the performance difference identity, and a union bound over the loops of a random process; the first two are reusable for any discounted policy-optimization result. Proofs of the milestones in any order are welcome.

Selected references

• S. Kakade and J. Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning (ICML), 2002. https://dl.acm.org/doi/10.5555/645531.656005
• J. Schulman, S. Levine, P. Moritz, M. Jordan, P. Abbeel, Trust Region Policy Optimization, ICML 2015. https://arxiv.org/abs/1502.05477
• J. Schulman, F. Wolski, P. Dhariwal, A. Radford, O. Klimov, Proximal Policy Optimization Algorithms, 2017. https://arxiv.org/abs/1707.06347
• D. J. Foster and A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, 2023. https://arxiv.org/abs/2312.16730

Motivation

A Markov-renewal program is a sequential decision model in which a system moves among finitely many states, the time between transitions is random and may depend on both the current and the next state, and a reward accrues during each sojourn. It generalizes the Markov decision process, where every transition takes one time unit, and is the standard model for maintenance, inventory and queueing control problems in which decisions are made at irregular epochs. W. S. Jewell introduced the model in two companion papers in Operations Research in 1963 (Part I, Part II).

Part II studies returns over an unbounded planning horizon. When the horizon is measured in number of transitions and rewards are not discounted, the expected return of a stationary policy grows linearly, and the paper's policy-improvement algorithm for this model rests on the precise form of that growth: a rate, the gain, and a state-dependent offset, the bias. Appendix A of Part II derives this asymptotic form from the Kemeny–Snell theory of finite Markov chains. This mission formalizes that derivation.

The result is the transition-counting counterpart of Howard's gain–bias analysis for Markov decision processes (R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960), and the fundamental matrix it uses is that of J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.

Setting

Fix a stationary policy. Only the embedded chain and the mean one-step rewards matter for the infinite-step undiscounted model (the paper, p. 961: these processes "depend only on the means"). The data are:

• a finite nonempty state set $S$ and a transition matrix $P = (p_{ij})_{i,j\in S}$ with $p_{ij}\ge 0$ and $\sum_j p_{ij} = 1$;
• the one-step expected rewards $\rho \in \mathbb R^S$ (the paper's (I 17));
• the terminal rewards $V(0)\in\mathbb R^S$.

The chain is ergodic (assumption 2, p. 951): $P$ is irreducible, meaning every state can be reached from every other state with positive probability. $P$ may be periodic. A stationary probability vector is $\pi\in\mathbb R^S$ with $\pi_i\ge 0$, $\sum_i\pi_i = 1$ and $\pi P = \pi$; $\Pi$ denotes the matrix every row of which is $\pi$.

The $n$-step return of the policy is the recursion (I 16) without the maximization:

$$V_i(n) = \rho_i + \sum_{j} p_{ij}V_j(n-1),\qquad n = 1,2,\ldots$$

The system gain is $G = \sum_i \pi_i\rho_i$ (A 6), the bias after $n$ steps is $W_i(n) = V_i(n) - Gn$, and the fundamental matrix is $Z = (I - P + \Pi)^{-1}$ (A 7).

Formalization targets

Goal: gain and Cesàro bias of the infinite-step return

For every irreducible row-stochastic $P$, stationary $\pi$, rewards $\rho$ and terminal rewards $V(0)$: the matrix $I - P + \Pi$ is invertible, and

$$\lim_{n\to\infty}\frac1n\sum_{m=1}^{n} W(m) = (Z - \Pi)\rho + \Pi V(0).$$

This is (A 4) with (A 5)–(A 7), in the form that is true for every ergodic chain and every terminal-reward vector.

Milestones

In order: the stationary vector exists, is unique and positive, and $\frac1n\sum_{k<n}P^k\to\Pi$ (Appendix A); the increment identity $V(n)-V(n-1) = P^{n-1}\rho$ (A 1) for constant $V(0)$; the Cesàro limit $\Pi\rho = G\mathbf 1$ of the increments (A 2); invertibility of $I-(P-\Pi)$ and the relations $PZ = ZP$, $\pi Z = \pi$, $I - Z = \Pi - PZ$; the Cesàro summability of $I+\sum_{j=1}^{n-1}(P^j-\Pi)$ to $Z$; the finite-$n$ bias formula (A 3) for constant $V(0)$; the relative-value equations $W_i + G = \rho_i + \sum_j p_{ij}W_j$ (4) for the limiting bias; and the paper's two-state machine example, where the four stationary policies have gains $70, 50, 80, 60$, the policy $(B,A)$ is optimal for every $n$ with $V_1(n) = 80n+170+(-1)^{n+1}170$, the limiting biases are $\pm170$, and the relative values of (5) are $340$ and $0$.

Stronger: aperiodic chains

If $P$ is moreover primitive (aperiodic), $W(n)$ itself converges to $(Z-\Pi)\rho + \Pi V(0)$. This is included as a supporting statement.

Significance

The asymptotic $V(n)\approx Gn + W$ is what makes average-reward policy improvement work: substituting it into the recursion yields the linear equations (4), whose solution (the relative values) is the test quantity of the paper's algorithm. The gain identifies which stationary policy earns most per transition in the long run, and the bias separates policies of equal gain. The same gain–bias decomposition underlies average-cost dynamic programming, the analysis of Markov reward processes, and the deviation matrix used in sensitivity analysis of Markov chains.

The result is classical and proved on paper. Formalizing it adds, first, a machine-checked account of the fundamental matrix of an irreducible, possibly periodic, finite chain: invertibility of $I - P + \Pi$, its algebraic relations and its Cesàro characterization. Mathlib has irreducible and primitive nonnegative matrices and row-stochastic matrices, but no stationary-vector uniqueness for irreducible chains, no Cesàro ergodic theorem for finite chains, and no fundamental matrix. Second, it fixes two slips of the printed appendix (below) with an exact statement. No machine-checked proof of this result is known.

Difficulty

The obvious argument writes $W(n) = \sum_{k<n}(P^k - \Pi)\rho + P^nV(0)$ and passes to the limit term by term. This fails for periodic chains: $P^k$ does not converge, $P^k - \Pi$ does not tend to zero, and the series $\sum_k (P^k - \Pi)$ does not converge. The paper's own example ($P$ swaps two states) is of this kind, and there $W(n)$ oscillates forever. What survives is Cesàro convergence, and establishing it needs control of all eigenvalues of $P$ of modulus one (they are simple roots of unity for an irreducible stochastic matrix) or an equivalent combinatorial argument. Invertibility of $I - P + \Pi$ requires that $1$ be a simple eigenvalue of $P$ with left eigenvector $\pi$, which is the Perron–Frobenius uniqueness statement for irreducible matrices; positivity of all entries of $P$, or a one-step Doeblin condition, is not available.

Formalization scope

States are a finite type with decidable equality and at least one element; vectors are S → ℝ, matrices Matrix S S ℝ, column vectors act by P *ᵥ v, the row vector $\pi$ by π ᵥ* P. Ergodicity is P ∈ Matrix.rowStochastic ℝ S ∧ P.IsIrreducible. The stationary vector is a hypothesis-constrained parameter (nonnegative, summing to one, $\pi P = \pi$), which is unique by the first milestone. $\Pi$, $G$ and $Z$ are definitions computed from $P$, $\pi$ and $\rho$, never free variables. Cesàro means are $\frac1n\sum_{m=1}^{n}$, equal to $0$ at $n = 0$. Mathlib's matrix inverse is $0$ on singular matrices, so the goal asserts invertibility of $I - P + \Pi$ explicitly.

Two printed slips are corrected, and the milestone texts are kept verbatim:

1. The paper's (A 4)–(A 5) have $+V(0)$ where iterating (I 16) gives $P^nV(0)$, whose Cesàro limit is $\Pi V(0)$. The goal uses $\Pi V(0)$; this is also the only form consistent with the paper's equation (4). Accordingly (A 1) and (A 3), which hold exactly when $PV(0) = V(0)$, carry the hypothesis that $V(0)$ is constant. The paper's example has $V(0) = 0$, where both readings agree.
2. The paper writes ordinary limits while noting that $P^{n-1}$ "converges or is Cesàro-summable". The goal and (A 2) are Cesàro limits; an ordinary limit is false for periodic chains.

The printed $\pi = \{\pi_1,\ldots,\pi_n\}$ uses $n$ for the number of states $N$.

A trivializing formalization is ruled out: $Z$ is not a junk inverse (invertibility is part of the goal), $\pi$ is a genuine stationary probability vector of $P$ rather than an arbitrary vector, $G$ is computed from $\pi$ and $\rho$, and the hypotheses are met by the paper's periodic two-state example.

Needed infrastructure: stationary vectors of irreducible stochastic matrices (existence, positivity, uniqueness), the Cesàro ergodic theorem $\frac1n\sum_{k<n}P^k\to\Pi$, and the fundamental matrix. These are reusable for any finite-chain average-reward result. Contributions proving any milestone, or the aperiodic variant, are welcome.

Selected references

• W. S. Jewell, Markov-Renewal Programming. II: Infinite Return Models, Example, Operations Research 11(6), 949–971, 1963. https://doi.org/10.1287/opre.11.6.949
• W. S. Jewell, Markov-Renewal Programming. I: Formulation, Finite Return Models, Operations Research 11(6), 938–948, 1963. https://doi.org/10.1287/opre.11.6.938
• J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• E. Seneta, Non-negative Matrices and Markov Chains, 2nd ed., Springer, 2006. https://doi.org/10.1007/0-387-32792-4