Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Eqs. (A 4)–(A 7) — the infinite-step return is V(n)≈Gn+WV(n) \approx Gn + WV(n)≈Gn+W with G=πρG = \pi\rhoG=πρ and Cesàro bias W=(Z−Π)ρ+ΠV(0)W = (Z-\Pi)\rho + \Pi V(0)W=(Z−Π)ρ+ΠV(0)

Proved
JewellMRP.InfiniteStep.infinite_step_gain_bias

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

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

Consider a Markov-renewal program operated under a fixed stationary policy whose embedded chain has transition matrix P=(pij)P = (p_{ij})P=(pij​) on a nonempty finite state set, assumed irreducible (ergodic; periodicity is allowed). Let π\piπ be its stationary probability vector, Π\PiΠ the matrix all of whose rows equal π\piπ, ρ\rhoρ the vector of one-step expected rewards and V(0)V(0)V(0) the vector of terminal rewards. Let V(n)V(n)V(n) be the expected nnn-step return, V(n)=ρ+PV(n−1)V(n) = \rho + PV(n-1)V(n)=ρ+PV(n−1), let

G=∑iπiρi(A 6)G = \sum_{i}\pi_i\rho_i \qquad \text{(A 6)}G=i∑​πi​ρi​(A 6)

be the system gain and Wi(n)=Vi(n)−GnW_i(n) = V_i(n) - GnWi​(n)=Vi​(n)−Gn the bias after nnn steps. Then

  1. the matrix I−P+ΠI - P + \PiI−P+Π is invertible, so the fundamental matrix Z=(I−P+Π)−1Z = (I - P + \Pi)^{-1}Z=(I−P+Π)−1 (A 7) is well defined, and
  2. the biases converge in the Cesàro sense to (Z−Π)ρ+ΠV(0)(Z - \Pi)\rho + \Pi V(0)(Z−Π)ρ+ΠV(0):
lim⁡n→∞1n∑m=1nW(m)=(Z−Π)ρ+ΠV(0).\lim_{n\to\infty}\frac1n\sum_{m=1}^{n} W(m) = (Z - \Pi)\rho + \Pi V(0).n→∞lim​n1​m=1∑n​W(m)=(Z−Π)ρ+ΠV(0).

Componentwise, Vi(n)≈Gn−G+∑jzijρj+∑jπjVj(0)V_i(n) \approx Gn - G + \sum_j z_{ij}\rho_j + \sum_j \pi_j V_j(0)Vi​(n)≈Gn−G+∑j​zij​ρj​+∑j​πj​Vj​(0): the expected return grows linearly at rate GGG, independent of the initial state, with a state-dependent offset given by the fundamental matrix. This is the asymptotic form (1) that the paper's policy-improvement algorithm for the infinite-step model relies on.

Formalization Note Two printed slips are corrected. (i) The paper writes the limit as [Z−Π]ρ+V(0)[Z - \Pi]\rho + V(0)[Z−Π]ρ+V(0); iterating (I 16) the terminal rewards contribute PnV(0)P^nV(0)PnV(0), whose Cesàro limit is ΠV(0)\Pi V(0)ΠV(0). The two coincide when V(0)V(0)V(0) is constant, in particular in the paper's example (V(0)=0V(0) = 0V(0)=0), and only ΠV(0)\Pi V(0)ΠV(0) is consistent with the paper's own equation (4). (ii) The paper writes an ordinary limit while stating that Pn−1P^{n-1}Pn−1 "converges or is Cesàro-summable"; for periodic chains, such as the paper's example, W(n)W(n)W(n) oscillates, so the limit is taken in the Cesàro sense 1n∑m=1nW(m)\frac1n\sum_{m=1}^n W(m)n1​∑m=1n​W(m). The stationary vector π\piπ is quantified over all stationary probability vectors of PPP, which under irreducibility is exactly one.

Preamble
import Mathlib
import Definitions.Def_JewellMRP_InfiniteStep_Model

open Matrix Filter Topology
Formal statement
namespace JewellMRP.InfiniteStep

theorem infinite_step_gain_bias {S : Type*} [Fintype S] [DecidableEq S] [Nonempty S]
    (P : Matrix S S ℝ) (hP : IsErgodic P) (π : S → ℝ) (hπ : IsStationary P π)
    (ρ V0 : S → ℝ) :
    IsUnit (1 - P + limitMatrix π) ∧
      Tendsto (cesaroMean (biasSeq P π ρ V0)) atTop
        (𝓝 ((fundamentalMatrix P π - limitMatrix π) *ᵥ ρ + limitMatrix π *ᵥ V0)) := by sorry

end JewellMRP.InfiniteStep
Source
Jewell, Markov-Renewal Programming. II: Infinite Return Models, Example, Oper. Res. 11 (1963), pp. 966-967, Eqs. (A 4)-(A 6); p. 952, Eqs. (A 5)-(A 7)
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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me