Appendix A, p. 966 — $Z = [I-(P-\Pi)]^{-1}$ exists and satisfies $PZ = ZP$ , $\pi Z = \pi$ , $I - Z = \Pi - PZ$

Proved

JewellMRP.InfiniteStep.fundamental_matrix_relations

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

fundamental-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, and $\Pi$ the matrix all of whose rows equal $\pi$ . Then the matrix $I - (P - \Pi)$ is invertible, and its inverse, the fundamental matrix $Z = (I - P + \Pi)^{-1}$ , satisfies

PZ = ZP, \qquad \pi Z = \pi, \qquad I - Z = \Pi - PZ .

These are the algebraic relations of the Kemeny–Snell fundamental matrix that Appendix A uses to identify the limiting bias vector.

Preamble

import Mathlib
import Definitions.Def_JewellMRP_InfiniteStep_Model

open Matrix Filter Topology

Formal statement

namespace JewellMRP.InfiniteStep

theorem fundamental_matrix_relations {S : Type*} [Fintype S] [DecidableEq S] [Nonempty S]
    (P : Matrix S S ℝ) (hP : IsErgodic P) (π : S → ℝ) (hπ : IsStationary P π) :
    IsUnit (1 - (P - limitMatrix π)) ∧
      P * fundamentalMatrix P π = fundamentalMatrix P π * P ∧
      π ᵥ* fundamentalMatrix P π = π ∧
      1 - fundamentalMatrix P π = limitMatrix π - P * 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)); p. 952, Eq. (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

Appendix A, p. 966 — Z=[I−(P−Π)]−1Z = [I-(P-\Pi)]^{-1}Z=[I−(P−Π)]−1 exists and satisfies PZ=ZPPZ = ZPPZ=ZP, πZ=π\pi Z = \piπZ=π, I−Z=Π−PZI - Z = \Pi - PZI−Z=Π−PZ

Appendix A, p. 966 — $Z = [I-(P-\Pi)]^{-1}$ exists and satisfies $PZ = ZP$ , $\pi Z = \pi$ , $I - Z = \Pi - PZ$