Appendix A, p. 966 — an ergodic chain has a unique, positive stationary vector and $P^n$ is Cesàro-summable to $\Pi$

Proved

JewellMRP.InfiniteStep.stationary_cesaro_limit

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

cesaro-meanmarkov-chainp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1stationary-distribution

Let $P$ be an irreducible row-stochastic matrix on a nonempty finite state set $S$ . Then there is a probability vector $\pi$ with $\pi P = \pi$ such that

every entry of $\pi$ is strictly positive,
$\pi$ is the only stationary probability vector of $P$ , and
the Cesàro means of the powers of $P$ converge entrywise to the matrix $\Pi$ whose rows all equal $\pi$ :

\lim_{n\to\infty} \frac1n \sum_{k=0}^{n-1} P^k = \Pi .

This is the Markov-chain fact on which Appendix A rests: it identifies the limiting per-step reward $\Pi\rho$ and makes the matrix $\Pi$ used in the fundamental matrix well defined.

Formalization Note The paper says " $P^{n-1}$ converges or is Cesàro-summable"; ordinary convergence fails for periodic chains, so the statement is the Cesàro limit, which holds for every irreducible chain.

Preamble

import Mathlib
import Definitions.Def_JewellMRP_InfiniteStep_Model

open Matrix Filter Topology

Formal statement

namespace JewellMRP.InfiniteStep

theorem stationary_cesaro_limit {S : Type*} [Fintype S] [DecidableEq S] [Nonempty S]
    (P : Matrix S S ℝ) (hP : IsErgodic P) :
    ∃ π : S → ℝ, IsStationary P π ∧ (∀ i, 0 < π i) ∧
      (∀ π' : S → ℝ, IsStationary P π' → π' = π) ∧
      Tendsto (fun n : ℕ => (n : ℝ)⁻¹ • ∑ k ∈ Finset.range n, P ^ k) atTop
        (𝓝 (limitMatrix π)) := by sorry

end JewellMRP.InfiniteStep

Source

Jewell, Markov-Renewal Programming. II: Infinite Return Models, Example, Oper. Res. 11 (1963), p. 966, Appendix A (after Eq. (A 1)), citing Kemeny and Snell [13]

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 — an ergodic chain has a unique, positive stationary vector and PnP^nPn is Cesàro-summable to Π\PiΠ

Appendix A, p. 966 — an ergodic chain has a unique, positive stationary vector and $P^n$ is Cesàro-summable to $\Pi$