Eq. (A 2) — the return increments are Cesàro-convergent to $\Pi\rho = G\mathbf 1$

Proved

JewellMRP.InfiniteStep.return_increment_cesaro

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

average-rewardcesaro-meanmarkov-renewalp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $P$ be an irreducible row-stochastic matrix on a nonempty finite state set with stationary probability vector $\pi$ , let $\Pi$ be the matrix whose rows all equal $\pi$ , and let $V(n)$ be the $n$ -step return of the fixed policy for one-step rewards $\rho$ and arbitrary terminal rewards $V(0)$ . Then

\lim_{n\to\infty}\frac1n\sum_{m=1}^{n}\bigl(V(m) - V(m-1)\bigr) = \Pi\rho, \qquad \text{and} \qquad (\Pi\rho)_i = \sum_{j}\pi_j\rho_j = G \ \text{ for all } i .

So the long-run per-transition increase of the expected return is the system gain $G$ , the same from every starting state.

Formalization Note The paper writes $\lim_{n\to\infty} V(n) - V(n-1) = \Pi\rho$ . For a periodic chain (such as the paper's own example) the increments oscillate and only their Cesàro means converge, so the limit is stated in the Cesàro sense. The statement holds for every terminal-reward vector $V(0)$ .

Preamble

import Mathlib
import Definitions.Def_JewellMRP_InfiniteStep_Model

open Matrix Filter Topology

Formal statement

namespace JewellMRP.InfiniteStep

theorem return_increment_cesaro {S : Type*} [Fintype S] [DecidableEq S] [Nonempty S]
    (P : Matrix S S ℝ) (hP : IsErgodic P) (π : S → ℝ) (hπ : IsStationary P π)
    (ρ V0 : S → ℝ) :
    Tendsto (cesaroMean (fun m => stepReturn P ρ V0 m - stepReturn P ρ V0 (m - 1))) atTop
        (𝓝 (limitMatrix π *ᵥ ρ)) ∧
      limitMatrix π *ᵥ ρ = fun _ => gain π ρ := by sorry

end JewellMRP.InfiniteStep

Source

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

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 2) — the return increments are Cesàro-convergent to Πρ=G1\Pi\rho = G\mathbf 1Πρ=G1

Eq. (A 2) — the return increments are Cesàro-convergent to $\Pi\rho = G\mathbf 1$