Eq. (4) — the limiting biases satisfy $W_i + G = \rho_i + \sum_j p_{ij} W_j$

Proved

JewellMRP.InfiniteStep.limit_bias_equation

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

average-rewardmarkov-renewalp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1relative-values

Let $P$ be an irreducible row-stochastic matrix on a nonempty finite state set with stationary probability vector $\pi$ , $\Pi$ the matrix all of whose rows equal $\pi$ , $Z = (I - P + \Pi)^{-1}$ , $\rho$ the one-step rewards, $G = \sum_i \pi_i\rho_i$ , and $V(0)$ any terminal-reward vector. Define the limiting bias vector

W = (Z - \Pi)\rho + \Pi V(0).

Then for every state $i$

W_i + G = \rho_i + \sum_{j} p_{ij} W_j .

These are the relative-value equations (4) of the paper, which the policy-improvement algorithm solves instead of computing $\Pi$ and $Z$ .

Formalization Note The paper derives (4) by substituting (A 5) into (I 16); (A 5) is used here in its corrected form $W = (Z-\Pi)\rho + \Pi V(0)$ (see the goal theorem). With the printed $W = (Z-\Pi)\rho + V(0)$ , equation (4) fails unless $(I - P)V(0) = 0$ .

Preamble

import Mathlib
import Definitions.Def_JewellMRP_InfiniteStep_Model

open Matrix Filter Topology

Formal statement

namespace JewellMRP.InfiniteStep

theorem limit_bias_equation {S : Type*} [Fintype S] [DecidableEq S] [Nonempty S]
    (P : Matrix S S ℝ) (hP : IsErgodic P) (π : S → ℝ) (hπ : IsStationary P π)
    (ρ V0 : S → ℝ) :
    let W := (fundamentalMatrix P π - limitMatrix π) *ᵥ ρ + limitMatrix π *ᵥ V0
    ∀ i, W i + gain π ρ = ρ i + ∑ j, P i j * W j := by sorry

end JewellMRP.InfiniteStep

Source

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

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. (4) — the limiting biases satisfy Wi+G=ρi+∑jpijWjW_i + G = \rho_i + \sum_j p_{ij} W_jWi​+G=ρi​+∑j​pij​Wj​

Eq. (4) — the limiting biases satisfy $W_i + G = \rho_i + \sum_j p_{ij} W_j$