Eqs. (A 4)–(A 7) — the infinite-step return is with and Cesàro bias
ProvedJewellMRP.InfiniteStep.infinite_step_gain_biasConsider a Markov-renewal program operated under a fixed stationary policy whose embedded chain has transition matrix on a nonempty finite state set, assumed irreducible (ergodic; periodicity is allowed). Let be its stationary probability vector, the matrix all of whose rows equal , the vector of one-step expected rewards and the vector of terminal rewards. Let be the expected -step return, , let
be the system gain and the bias after steps. Then
- the matrix is invertible, so the fundamental matrix (A 7) is well defined, and
- the biases converge in the Cesàro sense to :
Componentwise, : the expected return grows linearly at rate , 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 ; iterating (I 16) the terminal rewards contribute , whose Cesàro limit is . The two coincide when is constant, in particular in the paper's example (), and only is consistent with the paper's own equation (4). (ii) The paper writes an ordinary limit while stating that "converges or is Cesàro-summable"; for periodic chains, such as the paper's example, oscillates, so the limit is taken in the Cesàro sense . The stationary vector is quantified over all stationary probability vectors of , which under irreducibility is exactly one.
import Mathlib import Definitions.Def_JewellMRP_InfiniteStep_Model open Matrix Filter Topology
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
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.