p. 955: a change of policy indicated by the test quantity strictly increases the gain rate, $g^{z_2} > g^{z_1}$

Proved

JewellMRP.GainRate.strict_improvement

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

average-rewardmarkov-renewalp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1policy-iteration

Let a Markov-renewal program be ergodic with positive mean sojourn times. Let $z_1$ be a stationary policy, $(g_1, v_1)$ a solution of its value-determination equations (13), and let $z_2$ be an improvement step of $z_1$ with respect to $v_1$ : in each state $i$ , $z_2(i)$ maximizes the test quantity

\frac{1}{\nu^z_i}\Big\{\rho^z_i + \sum_{j} p^z_{ij} v_{1,j} - v_{1,i}\Big\}

over the alternatives $z$ , and $z_2(i) = z_1(i)$ when $z_1(i)$ already attains the maximum. If $z_2 \ne z_1$ , then for all stationary probability vectors $\pi_1$ , $\pi_2$ of the chains of $z_1$ and $z_2$ ,

g^{z_1} = \frac{\sum_i \pi_{1,i}\rho^{z_1(i)}_i}{\sum_k \pi_{1,k}\nu^{z_1(k)}_k} \;<\; \frac{\sum_i \pi_{2,i}\rho^{z_2(i)}_i}{\sum_k \pi_{2,k}\nu^{z_2(k)}_k} = g^{z_2}.

Since there are finitely many stationary policies, this strict monotonicity is what forces the algorithm of Fig. 2 to terminate.

Preamble

import Mathlib
import Definitions.Def_JewellMRP_GainRate_MRP
import Definitions.Def_JewellMRP_GainRate_PolicyIteration

Formal statement

namespace JewellMRP.GainRate
theorem strict_improvement {N : ℕ} [NeZero N] {α : Type*} (M : MRP N α)
    (hM : M.IsErgodic) (z₁ z₂ : Fin N → α) (g₁ : ℝ) (v₁ : Fin N → ℝ)
    (h₁ : M.SolvesValueDetermination z₁ g₁ v₁) (hstep : M.IsImprovementStep z₁ v₁ z₂)
    (hne : z₂ ≠ z₁) (π₁ π₂ : Fin N → ℝ)
    (hπ₁ : IsStationaryDist (M.policyMatrix z₁) π₁)
    (hπ₂ : IsStationaryDist (M.policyMatrix z₂) π₂) :
    M.gainRate z₁ π₁ < M.gainRate z₂ π₂ := by sorry
end JewellMRP.GainRate

Source

Jewell, Markov-Renewal Programming. II: Infinite Return Models, Example, Oper. Res. 11 (1963), p. 955 ("one shows that g^{z_2} > g^{z_1}"), with Fig. 2 (p. 956)

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

p. 955: a change of policy indicated by the test quantity strictly increases the gain rate, gz2>gz1g^{z_2} > g^{z_1}gz2​>gz1​

p. 955: a change of policy indicated by the test quantity strictly increases the gain rate, $g^{z_2} > g^{z_1}$