Appendix A, p. 966 — $I + \sum_{j=1}^{n-1}(P^j - \Pi)$ is Cesàro-summable to the fundamental matrix $Z$

Proved

JewellMRP.InfiniteStep.fundamental_matrix_cesaro

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

cesaro-meanfundamental-matrixmarkov-chainp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $P$ be an irreducible row-stochastic matrix on a nonempty finite state set, $\pi$ its stationary probability vector, $\Pi$ the matrix all of whose rows equal $\pi$ , and $Z = (I - P + \Pi)^{-1}$ . Put

A(n) = I + \sum_{j=1}^{n-1}\bigl(P^j - \Pi\bigr), \qquad n \ge 1 .

Then the Cesàro means of $A(n)$ converge to $Z$ :

\lim_{n\to\infty}\frac1n\sum_{m=1}^{n} A(m) = Z .

This identifies the fundamental matrix of Kemeny and Snell as the (Cesàro) sum of the deviations of the powers of $P$ from their limit, which is how $Z$ enters the limiting bias.

Formalization Note The paper says the sequence "converges or is Cesàro-summable"; for periodic chains only the Cesàro limit exists, and that is what is stated. $A(1) = I$ (empty sum).

Preamble

import Mathlib
import Definitions.Def_JewellMRP_InfiniteStep_Model

open Matrix Filter Topology

Formal statement

namespace JewellMRP.InfiniteStep

theorem fundamental_matrix_cesaro {S : Type*} [Fintype S] [DecidableEq S] [Nonempty S]
    (P : Matrix S S ℝ) (hP : IsErgodic P) (π : S → ℝ) (hπ : IsStationary P π) :
    Tendsto (cesaroMean (fun n : ℕ => 1 + ∑ j ∈ Finset.Ico 1 n, (P ^ j - limitMatrix π)))
      atTop (𝓝 (fundamentalMatrix P π)) := by sorry

end JewellMRP.InfiniteStep

Source

Jewell, Markov-Renewal Programming. II: Infinite Return Models, Example, Oper. Res. 11 (1963), p. 966, Appendix A (before Eq. (A 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

Appendix A, p. 966 — I+∑j=1n−1(Pj−Π)I + \sum_{j=1}^{n-1}(P^j - \Pi)I+∑j=1n−1​(Pj−Π) is Cesàro-summable to the fundamental matrix ZZZ

Appendix A, p. 966 — $I + \sum_{j=1}^{n-1}(P^j - \Pi)$ is Cesàro-summable to the fundamental matrix $Z$