Eq. (A 1) — $V(n) - V(n-1) = P^{n-1}\rho$ for constant terminal rewards

Proved

JewellMRP.InfiniteStep.return_increment_eq

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamic-programmingmarkov-renewalp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $P$ be an irreducible row-stochastic matrix on a nonempty finite state set, $\rho$ a vector of one-step expected rewards, and $V(0)$ a constant terminal-reward vector ( $V_i(0) = V_j(0)$ for all $i, j$ ). Let $V(n)$ be the $n$ -step expected return of the fixed policy, $V(n) = \rho + P V(n-1)$ . Then for every $n \ge 1$

V(n) - V(n-1) = P^{n-1}\rho .

This is the first step of Appendix A: the increments of the return are the images of $\rho$ under the powers of $P$ .

Formalization Note The paper prints (A 1) with no condition on $V(0)$ . Iterating (I 16) gives $V(n) - V(n-1) = P^{n-1}(\rho + P V(0) - V(0))$ , so (A 1) holds exactly when $P V(0) = V(0)$ , which for an irreducible $P$ means that $V(0)$ is constant; that hypothesis is added here. It covers the paper's example, where $V(0) = 0$ .

Preamble

import Mathlib
import Definitions.Def_JewellMRP_InfiniteStep_Model

open Matrix Filter Topology

Formal statement

namespace JewellMRP.InfiniteStep

theorem return_increment_eq {S : Type*} [Fintype S] [DecidableEq S] [Nonempty S]
    (P : Matrix S S ℝ) (hP : IsErgodic P) (ρ V0 : S → ℝ) (hV0 : ∀ i j, V0 i = V0 j)
    (n : ℕ) (hn : 1 ≤ n) :
    stepReturn P ρ V0 n - stepReturn P ρ V0 (n - 1) = (P ^ (n - 1)) *ᵥ ρ := by sorry

end JewellMRP.InfiniteStep

Source

Jewell, Markov-Renewal Programming. II: Infinite Return Models, Example, Oper. Res. 11 (1963), p. 966, Eq. (A 1)

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Eq. (A 1) — V(n)−V(n−1)=Pn−1ρV(n) - V(n-1) = P^{n-1}\rhoV(n)−V(n−1)=Pn−1ρ for constant terminal rewards

Eq. (A 1) — $V(n) - V(n-1) = P^{n-1}\rho$ for constant terminal rewards