Read-back: MarkovMixing.cutoff_iff_step

The objects being quantified over

The statement is universally quantified over an infinite family of finite state spaces and transition matrices. Explicitly, it fixes:

• an implicit family of types $V_0, V_1, V_2, \dots$ indexed by the natural numbers (written $V : \mathbb{N} \to \mathrm{Type}^*$), together with three typeclass assumptions holding for every index $n$: each $V_n$ is a finite type, each $V_n$ has decidable equality, and each $V_n$ is nonempty;
• a family of real square matrices $P^{(n)} \in \mathbb{R}^{V_n \times V_n}$, one for each $n$ (the entry at row $x$, column $y$ is written $P^{(n)}_{x y}$);
• a family of real-valued functions $\pi^{(n)} : V_n \to \mathbb{R}$, one for each $n$. Nothing in the type of $\pi^{(n)}$ makes it a probability distribution; that is imposed by a hypothesis below.

There is no hypothesis relating $V_n$ to $V_m$ for $n \neq m$, no hypothesis that $|V_n|$ grows, and no hypothesis that the family is nonconstant: a single fixed chain repeated for every $n$ is an admissible instance.

The four standing hypotheses

Each of the following is asserted for every $n \in \mathbb{N}$ (each hypothesis is itself a $\forall n$ statement).

hP — $P^{(n)}$ is stochastic. This unfolds to the conjunction of

$$\forall x, y \in V_n,\ \ P^{(n)}_{x y} \ge 0 \qquad\text{and}\qquad \forall x \in V_n,\ \ \sum_{y \in V_n} P^{(n)}_{x y} = 1 .$$

hirr — $P^{(n)}$ is "irreducible" in the sense of this development. This is a custom predicate (it shadows Mathlib's Irreducible, which is about ring elements; the one used here is MarkovMixing.Irreducible). It unfolds to

$$\forall x, y \in V_n,\ \ \exists\, t \in \mathbb{N},\ \ \bigl((P^{(n)})^{t}\bigr)_{x y} > 0 ,$$

where $(P^{(n)})^t$ is the $t$-fold matrix product and $(P^{(n)})^0$ is the identity matrix. Because $t = 0$ is permitted and $(P^{(n)})^0_{xx} = 1 > 0$, the diagonal instances $x = y$ of this hypothesis are automatically true and impose nothing; the content is entirely in the off-diagonal instances $x \neq y$, for which $t = 0$ gives the entry $0$ and so some $t \ge 1$ must work. In words: every ordered pair of distinct states is connected by a positive-probability path of some finite length.

hap — $P^{(n)}$ is "aperiodic" in the sense of this development. This asserts that for every state $x \in V_n$ the quantity $\mathrm{period}(P^{(n)}, x)$ equals $1$, where

$$\mathrm{period}(P, x) \;=\; \sup\nolimits_{\mathbb{N}} \bigl\{\, d \in \mathbb{N} \ \bigm|\ \forall t \in R(P,x),\ d \mid t \,\bigr\}, \qquad R(P,x) = \{\, t \in \mathbb{N} \ \mid\ t \ge 1 \ \text{and}\ (P^{t})_{x x} > 0 \,\}.$$

The supremum is the supremum in the natural numbers, which is a total operation with the convention that the supremum of an empty set or of a set unbounded above is $0$. Two branches therefore matter:

• If $R(P,x) \neq \varnothing$ (the state $x$ has at least one positive-probability return time), then $0$ does not belong to the set of common divisors — since $0 \mid t$ only for $t = 0$ and every element of $R(P,x)$ is $\ge 1$ — and the set of common divisors is bounded by the least element of $R(P,x)$. In that case the supremum is attained and equals $\gcd R(P,x)$. So the hypothesis reads: the greatest common divisor of the return times of $x$ is $1$.
• If $R(P,x) = \varnothing$ (no $t \ge 1$ has $(P^t)_{xx} > 0$), then every $d \in \mathbb{N}$ vacuously divides every element of the empty set, the set of common divisors is all of $\mathbb{N}$, hence unbounded, and the junk convention returns $\mathrm{period}(P,x) = 0 \ne 1$. So this branch is excluded by hap: assuming hap, every state necessarily has at least one return time, and the greatest common divisor of those return times is $1$.

hπ — $\pi^{(n)}$ is a stationary distribution for $P^{(n)}$. This unfolds to the conjunction of three conditions:

$$\forall x \in V_n,\ \pi^{(n)}_x \ge 0, \qquad \sum_{x \in V_n} \pi^{(n)}_x = 1, \qquad \forall y \in V_n,\ \ \sum_{x \in V_n} \pi^{(n)}_x P^{(n)}_{x y} = \pi^{(n)}_y .$$

(The last is the left vector–matrix product $\pi^{(n)} P^{(n)} = \pi^{(n)}$ written out entrywise.)

These four hypotheses are jointly satisfiable — for instance take every $V_n$ to be a one-point type, $P^{(n)} = (1)$ and $\pi^{(n)} = 1$ — so the theorem is not vacuous.

Note also that the typeclass assumption "$V_n$ is nonempty" is already implied by hπ: if $V_n$ were empty, the sum $\sum_{x \in V_n} \pi^{(n)}_x$ would be $0$, contradicting the requirement that it equal $1$. It is therefore a redundant hypothesis, though it independently rules out one junk branch described below.

The distance and mixing-time notions appearing in the conclusion

Total variation distance $\mathrm{tv}(\mu,\nu)$. For $\mu, \nu : V \to \mathbb{R}$,

$$\mathrm{tv}(\mu,\nu) \;=\; \sup_{A \subseteq V \text{ finite}} \Bigl| \sum_{x \in A} \mu_x - \sum_{x \in A} \nu_x \Bigr| ,$$

the supremum being taken over all subsets $A$ of $V$ (as $V$ is a finite type, this is a supremum over a finite, nonempty collection, hence an attained maximum; the empty subset contributes the value $0$, so $\mathrm{tv} \ge 0$ always). There is no factor of $\tfrac12$ and no $\ell^1$ norm: this is the "maximum discrepancy over events" form.

Row distribution. $\mathrm{row}(P,t,x)$ is the function $y \mapsto (P^t)_{x y}$, i.e. the $x$-th row of the $t$-th matrix power, with $P^0 = I$.

Distance to stationarity at time $t$. For $t \in \mathbb{N}$,

$$d^{(n)}(t) \;=\; \sup_{x \in V_n} \ \mathrm{tv}\bigl(\mathrm{row}(P^{(n)}, t, x),\ \pi^{(n)}\bigr) \;=\; \max_{x \in V_n} \ \max_{A \subseteq V_n} \Bigl| \sum_{y \in A} (P^{(n)})^t_{x y} \ -\ \sum_{y \in A} \pi^{(n)}_y \Bigr| .$$

The outer supremum is over the type $V_n$ itself. This is where nonemptiness matters: a supremum over an empty real-indexed family would return the junk value $0$. Both the explicit Nonempty instance and (redundantly) hπ make that branch unreachable here.

Mixing time at threshold $\varepsilon$. For $\varepsilon \in \mathbb{R}$,

$$t^{(n)}_{\mathrm{mix}}(\varepsilon) \;=\; \inf\nolimits_{\mathbb{N}} \{\, t \in \mathbb{N} \ \mid\ d^{(n)}(t) \le \varepsilon \,\},$$

the infimum being the natural-number infimum, a total operation returning $0$ when the set is empty. So "the mixing time is $0$" conflates two situations: the chain already satisfies $d^{(n)}(0) \le \varepsilon$ at time $0$, and no time whatsoever achieves accuracy $\varepsilon$. Note $d^{(n)}(0) = \max_x \mathrm{tv}(\delta_x, \pi^{(n)}) = 1 - \min_x \pi^{(n)}_x$, so the first situation occurs exactly when $\min_x \pi^{(n)}_x \ge 1 - \varepsilon$, which is perfectly possible for small state spaces; and by standard finite-chain theory the second (empty-set) situation cannot occur for any $\varepsilon > 0$ under the standing hypotheses, since an irreducible aperiodic stochastic matrix with stationary distribution $\pi$ has $d^{(n)}(t) \to 0$ as $t \to \infty$. Since every threshold used below is strictly positive, the empty-infimum branch is unreachable, but the "mixing time equals $0$ because time $0$ already suffices" branch is reachable.

The reference mixing time. $t^{(n)}_{\mathrm{mix}} = t^{(n)}_{\mathrm{mix}}(1/4)$, i.e. the threshold is fixed at $\tfrac14$.

Cutoff. $\mathrm{HasCutoff}(P,\pi)$ unfolds to:

$$\forall \varepsilon \in \mathbb{R},\ \ 0 < \varepsilon \ \Rightarrow\ \varepsilon < 1 \ \Rightarrow\ \lim_{n \to \infty} \frac{t^{(n)}_{\mathrm{mix}}(\varepsilon)}{t^{(n)}_{\mathrm{mix}}(1-\varepsilon)} \;=\; 1 ,$$

where both mixing times are natural numbers cast to $\mathbb{R}$, the limit is along the filter of large $n$, and the convergence is to the point $1$ in the usual topology on $\mathbb{R}$. The quotient is real division with the total-function convention $a/0 = 0$. That branch is reachable: the denominator $t^{(n)}_{\mathrm{mix}}(1-\varepsilon)$ is $0$ exactly when $\min_x \pi^{(n)}_x \ge \varepsilon$, which for a fixed small $\varepsilon$ holds for every chain whose stationary distribution stays bounded away from $0$ — for such families the sequence being tested is identically $0$ and does not converge to $1$. For families with $\min_x \pi^{(n)}_x \to 0$ the denominator is eventually positive for each fixed $\varepsilon$, so the convention only affects finitely many terms and does not affect the limit. The numerator can likewise be $0$ under the analogous condition $\min_x \pi^{(n)}_x \ge 1 - \varepsilon$.

Note that $\mathrm{HasCutoff}$ as defined takes no stochasticity, irreducibility, aperiodicity or stationarity of its own; it is a bare statement about the two families $P$ and $\pi$.

What the theorem asserts

Under the standing hypotheses above, the theorem states a logical equivalence (an "if and only if", not an implication in either direction) between the following two statements.

Left side. $\mathrm{HasCutoff}(P, \pi)$: for every real $\varepsilon$ with $0 < \varepsilon < 1$, the ratio $t^{(n)}_{\mathrm{mix}}(\varepsilon) / t^{(n)}_{\mathrm{mix}}(1-\varepsilon)$ tends to $1$ as $n \to \infty$.

Right side. For every real number $c$ with $c > 0$, the conjunction of two implications holds:

$$\Bigl( c < 1 \ \Rightarrow\ \lim_{n\to\infty} d^{(n)}\bigl(\lfloor c \cdot t^{(n)}_{\mathrm{mix}} \rfloor\bigr) = 1 \Bigr) \ \wedge\ \Bigl( 1 < c \ \Rightarrow\ \lim_{n\to\infty} d^{(n)}\bigl(\lfloor c \cdot t^{(n)}_{\mathrm{mix}} \rfloor\bigr) = 0 \Bigr).$$

Here $t^{(n)}_{\mathrm{mix}}$ is the natural number $t^{(n)}_{\mathrm{mix}}(1/4)$ cast to $\mathbb{R}$, the product $c \cdot t^{(n)}_{\mathrm{mix}}$ is a real number, and $\lfloor \cdot \rfloor$ is the natural-number floor, which is then used as the time argument of $d^{(n)}$. Both limits are along $n \to \infty$ and are convergence in $\mathbb{R}$ to the points $1$ and $0$ respectively. The two conjuncts refer to the same sequence of numbers; only the hypotheses $c < 1$ and $1 < c$ distinguish them.

Spelling out the case analysis in $c$: for $c \in (0,1)$ the second conjunct is vacuously true and the assertion is $d^{(n)}(\lfloor c\, t^{(n)}_{\mathrm{mix}} \rfloor) \to 1$; for $c > 1$ the first conjunct is vacuously true and the assertion is $d^{(n)}(\lfloor c\, t^{(n)}_{\mathrm{mix}} \rfloor) \to 0$; and at $c = 1$ both implications have false premises, so the case $c = 1$ imposes nothing at all. Values $c \le 0$ are excluded by the hypothesis $0 < c$.

Junk-value and edge-case conventions, and whether they are reachable

• Natural-number floor of a negative real. $\lfloor r \rfloor$ for $r < 0$ is defined to be $0$. Unreachable here: $c > 0$ and $t^{(n)}_{\mathrm{mix}} \ge 0$, so the argument $c \cdot t^{(n)}_{\mathrm{mix}}$ is always $\ge 0$.
• Floor truncation. $c \cdot t^{(n)}_{\mathrm{mix}}$ is generally not an integer; the statement evaluates the distance at the integer part, so e.g. for $c$ slightly below $1$ and small $t^{(n)}_{\mathrm{mix}}$ the argument can coincide with $t^{(n)}_{\mathrm{mix}}$ itself, and for any $c$ with $c \cdot t^{(n)}_{\mathrm{mix}} < 1$ the argument is $0$.
• Real division by zero in HasCutoff. $a/0 = 0$. Reachable, as described above, precisely when $t^{(n)}_{\mathrm{mix}}(1-\varepsilon) = 0$, i.e. $\min_x \pi^{(n)}_x \ge \varepsilon$.
• Natural-number infimum of the empty set (in the definition of mixing time) $= 0$. Not reachable for the thresholds actually used ($\varepsilon$, $1-\varepsilon$ with $0<\varepsilon<1$, and $1/4$), because the standing hypotheses force $d^{(n)}(t) \to 0$; but the value $0$ for the mixing time is reachable through the other route, namely $d^{(n)}(0) \le \varepsilon$.
• Natural-number supremum of an unbounded set $= 0$ (in the definition of period). Reachable in general — it is exactly what happens for a state with no return times — but hap rules it out by demanding the value $1$.
• Supremum over an empty index type $= 0$ (in the definition of $d^{(n)}$, whose outer supremum ranges over $V_n$). Unreachable: $V_n$ is assumed nonempty, and hπ independently forces it.
• The inner supremum in the total variation distance ranges over all subsets of a finite type, always including the empty subset, so it is a genuine attained maximum and is never negative.
• Degenerate families. Nothing prevents $t^{(n)}_{\mathrm{mix}} = 0$ for all $n$; in that case $\lfloor c \cdot t^{(n)}_{\mathrm{mix}} \rfloor = 0$ for every $c > 0$, and the right-hand side asks the single sequence $n \mapsto d^{(n)}(0) = 1 - \min_x \pi^{(n)}_x$ to converge to $1$ (from the $c<1$ clause) and to $0$ (from the $c>1$ clause) simultaneously.

Redundancies and vacuity

The hypothesis that each $V_n$ is nonempty is implied by hπ and is therefore redundant as a mathematical assumption. The $x = y$ instances of hirr are automatically true and impose no condition. The case $c = 1$ on the right-hand side imposes no condition. No hypothesis is unsatisfiable, and the hypothesis set as a whole is satisfiable, so the statement is not vacuously true.

The declaration is stated with its proof omitted (the proof body is a placeholder), so nothing is proved here; only the statement above is asserted.