Read-back: Def_mm_basic (namespace MarkovMixing)

Throughout, $V$ is an arbitrary type assumed finite (with decidable equality), and all matrices are $V \times V$ matrices with real entries, viewed as functions of two arguments: $P\,x\,y$ is written $P(x,y)$ below. Sums $\sum_x$ range over all elements of the finite type $V$.

IsStochastic. For a real matrix $P$ indexed by $V$, the predicate IsStochastic $P$ asserts the conjunction of two conditions: every entry is nonnegative, $\forall x, y \in V,\ 0 \le P(x,y)$; and every row sums to one, $\forall x \in V,\ \sum_{y \in V} P(x,y) = 1$. (Rows, not columns: the sum for fixed first index $x$ runs over the second index $y$.) If $V$ is empty, both conditions hold vacuously.

IsDist. For a function $\mu : V \to \mathbb{R}$, the predicate IsDist $\mu$ asserts that $\mu(x) \ge 0$ for every $x \in V$ and that $\sum_{x \in V} \mu(x) = 1$. If $V$ is empty the sum is $0$, so no $\mu$ on an empty type satisfies this.

IsStationary. For a real matrix $P$ indexed by $V$ and a function $\pi : V \to \mathbb{R}$, the predicate IsStationary $P\ \pi$ asserts that $\pi$ satisfies IsDist (entrywise nonnegative with total mass $1$, as above) and that the row vector $\pi$ multiplied on the right by $P$ equals $\pi$; componentwise, $\sum_{x \in V} \pi(x)\, P(x,y) = \pi(y)$ for every $y \in V$. No stochasticity assumption on $P$ is part of this definition.

Irreducible. For a real matrix $P$ indexed by $V$, the predicate Irreducible $P$ asserts: for every pair of states $x, y \in V$ there exists a natural number $t \ge 0$ such that the $(x,y)$ entry of the matrix power $P^t$ is strictly positive, $0 < (P^t)(x,y)$. The exponent $t = 0$ is allowed; since $P^0$ is the identity matrix, the case $x = y$ is always witnessed by $t = 0$ regardless of $P$, so the definition only imposes a genuine condition on pairs $x \ne y$.

returnSet. For a real matrix $P$ indexed by $V$ and a state $x \in V$, returnSet $P\ x$ is the set of natural numbers

$$\mathcal{R}(P,x) = \{\, t \in \mathbb{N} \mid t \ge 1 \ \text{and}\ 0 < (P^t)(x,x) \,\},$$

i.e. the set of strictly positive times $t$ at which the diagonal entry of $P^t$ at $x$ is strictly positive. Time $t = 0$ is explicitly excluded.

period. For a real matrix $P$ indexed by $V$ and a state $x \in V$, period $P\ x$ is defined as the supremum, taken in the natural numbers, of the set of common divisors of the return set:

$$\operatorname{period}(P,x) = \sup\,\{\, d \in \mathbb{N} \mid d \text{ divides every } t \in \mathcal{R}(P,x) \,\},$$

where $\mathcal{R}(P,x)$ is the returnSet just described. This supremum is Lean's supremum on $\mathbb{N}$, which returns $0$ for a set that is empty or unbounded. Consequently: if $\mathcal{R}(P,x)$ is nonempty, the common divisors form a bounded set and the value is the greatest common divisor of all return times; but if $\mathcal{R}(P,x)$ is empty (the state never returns), then every natural number vacuously divides every element, the divisor set is all of $\mathbb{N}$, which is unbounded, and the defined period is $0$, not $\infty$.

Aperiodic. For a real matrix $P$ indexed by $V$, the predicate Aperiodic $P$ asserts that $\operatorname{period}(P,x) = 1$ for every state $x \in V$, with period as defined above (in particular, a state with empty return set has period $0$ and so witnesses failure of this predicate).

lazy. For a real matrix $P$ indexed by $V$, lazy $P$ is the matrix $\tfrac{1}{2} I + \tfrac{1}{2} P$, where $I$ is the $V \times V$ identity matrix; entrywise, $(\operatorname{lazy} P)(x,y) = \tfrac{1}{2}[x = y] + \tfrac{1}{2} P(x,y)$.

Harmonic. For a real matrix $P$ indexed by $V$ and a function $h : V \to \mathbb{R}$, the predicate Harmonic $P\ h$ asserts that for every $x \in V$,

$$h(x) = \sum_{y \in V} P(x,y)\, h(y),$$

i.e. $h$ equals the result of applying $P$ to $h$ (rows of $P$ averaging the values of $h$). No assumption is made that $P$ is stochastic.

DetailedBalance. For a real matrix $P$ indexed by $V$ and a function $\pi : V \to \mathbb{R}$, the predicate DetailedBalance $P\ \pi$ asserts that for every pair $x, y \in V$,

$$\pi(x)\, P(x,y) = \pi(y)\, P(y,x).$$

Nothing here requires $\pi$ to be a distribution or $P$ to be stochastic.

timeReversal. For a real matrix $P$ indexed by $V$ and a function $\pi : V \to \mathbb{R}$, timeReversal $P\ \pi$ is the $V \times V$ real matrix whose $(x,y)$ entry is

$$\frac{\pi(y)\, P(y,x)}{\pi(x)}.$$

Since real division in Lean is total with $a/0 = 0$, at any state $x$ with $\pi(x) = 0$ the entire row $x$ of this matrix is identically $0$. No positivity or stationarity hypothesis on $\pi$ is imposed by the definition.

graphWalk. For a simple graph $G$ on the finite vertex type $V$ (with decidable adjacency), graphWalk $G$ is the $V \times V$ real matrix whose $(x,y)$ entry is $\deg_G(x)^{-1}$ (the reciprocal of the degree of $x$ in $G$, i.e. the number of neighbors of $x$) when $x$ and $y$ are adjacent in $G$, and $0$ otherwise. If $x$ is an isolated vertex, no $y$ is adjacent to it and its row is identically $0$ (the expression $0^{-1}$, which in Lean would equal $0$, is never actually taken since adjacency forces $\deg_G(x) \ge 1$); such a row sums to $0$, and the definition itself asserts no stochasticity.

uniformDist. For a finite type $V$ (here taken as an explicit argument with its own finiteness assumption, with no decidable-equality requirement), uniformDist $V$ is the constant function $V \to \mathbb{R}$ sending every element to $|V|^{-1}$, the reciprocal of the cardinality of $V$. If $V$ is empty, the cardinality is $0$ and, by Lean's convention $0^{-1} = 0$, the function is the (vacuous) constant $0$.

groupWalk. For a finite group $G$ and an arbitrary function $\mu : G \to \mathbb{R}$, groupWalk $\mu$ is the $G \times G$ real matrix whose $(a,b)$ entry is $\mu(b \cdot a^{-1})$ — the value of $\mu$ at the product of $b$ with the inverse of $a$, in that order (so the increment multiplies on the left: this is the entry for stepping from $a$ to $b = (b a^{-1})\,a$). The definition places no requirement that $\mu$ be nonnegative or sum to $1$.