Corollary 1.17 -- existence and uniqueness of the stationary distribution

Let $V$ be a finite, nonempty type (with decidable equality), and let $P$ be a $V \times V$ matrix with real entries. Assume two hypotheses. First, $P$ is stochastic in the sense of the bundle's custom definition: every entry is nonnegative, $P_{x,y} \ge 0$ for all $x, y \in V$, and every row sums to one, $\sum_{y \in V} P_{x,y} = 1$ for every $x \in V$. Second, $P$ is irreducible in the sense of the bundle's custom definition: for every ordered pair $x, y \in V$ there exists a natural number $t \ge 0$ such that $(P^t)_{x,y} > 0$ — note that $t = 0$ is allowed, and since $P^0$ is the identity matrix, the condition is automatically satisfied when $x = y$; the substantive content is only for $x \ne y$. Under these hypotheses, the theorem asserts that there exists a unique function $\pi : V \to \mathbb{R}$ that is stationary for $P$, where stationarity is again the bundle's custom definition and means the conjunction of two conditions: (i) $\pi$ is a probability distribution on $V$, i.e. $\pi(x) \ge 0$ for all $x \in V$ and $\sum_{x \in V} \pi(x) = 1$; and (ii) the row vector $\pi$ is a fixed point of right-multiplication by $P$, i.e. $\sum_{x \in V} \pi(x)\, P_{x,y} = \pi(y)$ for every $y \in V$. "Unique" here is the strong uniqueness quantifier: some $\pi$ satisfying (i) and (ii) exists, and any two functions $V \to \mathbb{R}$ satisfying (i) and (ii) are equal as functions (they agree at every point of $V$).