Read-back: matthews_lower

Let $V$ be a finite, nonempty type (with decidable equality) and let $P$ be a $V \times V$ real matrix assumed stochastic ($P(x,y) \ge 0$ everywhere and $\sum_y P(x,y) = 1$ for every row $x$) and "irreducible" in the sense that for every pair $x, y \in V$ there is some natural number $t \ge 0$ with $(P^t)(x,y) > 0$ — since $t = 0$ is permitted and $P^0$ is the identity, the diagonal case is automatic. For a length-$t$ vertex sequence $\omega = (\omega_0, \dots, \omega_t)$ let its weight be $\prod_{i=0}^{t-1} P(\omega_i, \omega_{i+1})$ (equal to $1$ when $t = 0$). Two custom quantities appear. (i) For $a, b \in V$, the "expected hitting time" $h(a,b) = \sum_{t=0}^{\infty} u_t(a,b)$, where $u_t(a,b)$ is the total weight of all length-$t$ sequences starting at $\omega_0 = a$ that avoid $b$ at every index including index $0$ — probabilistically, $u_t$ is the chance that the walk started at $a$ has not visited $b$ through time $t$, so $h(a,b)$ is the expected first time the walk from $a$ hits $b$ (and $h(a,a)$ would be $0$, though the theorem only ever invokes $h$ at distinct arguments). (ii) The "maximal expected cover time" $t_{\mathrm{cov}} = \sup_{x \in V} C(x)$, where $C(x) = \sum_{t=0}^{\infty} r_t(x)$ and $r_t(x)$ is the total weight of all length-$t$ sequences starting at $x$ for which some vertex $y \in V$ is avoided at every index $0, \dots, t$ — i.e. $r_t(x)$ is the chance the walk from $x$ has not yet visited all of $V$ by time $t$, making $C(x)$ the expected cover time from $x$. The infinite series are Lean tsums, which evaluate to $0$ if the series is not summable, and the supremum over the finite nonempty $V$ is a genuine maximum. Now fix a finite subset $A \subseteq V$ with $|A| \ge 2$, and a real number $m$ with $m \ge 0$, assumed to be a lower bound on all hitting times between distinct elements of $A$: for all $a, b \in A$ with $a \ne b$, $m \le h(a,b)$. The theorem asserts the single non-strict inequality

i.e. $m$ times the harmonic number $H_{|A|-1} = 1 + \tfrac12 + \dots + \tfrac{1}{|A|-1}$ is at most the maximal expected cover time (the sum runs over integers $k$ from $1$ to $|A| - 1$ inclusive; since $|A| \ge 2$ this range is nonempty, and the subtraction is over the natural numbers, which is unproblematic here). The bound involves cover times over the whole state space $V$ but hitting-time hypotheses only within $A$; there is no assumption relating $m$ to hitting times outside $A$, no aperiodicity or reversibility assumption, and $m = 0$ always satisfies the hypotheses (making the conclusion the trivial statement $0 \le t_{\mathrm{cov}}$ in that case).