Read-back of MarkovMixing.product_chain_mixing

The objects the statement quantifies over

The statement is universally quantified over the following data, all of which must be supplied before any conclusion is asserted.

A natural number $n$ (an implicit argument) together with a proof that $2 \le n$. A family of types $W_0, W_1, \dots, W_{n-1}$ indexed by $i \in \{0,\dots,n-1\}$ (implicit; the types may live in any universe), each of which is assumed to be finite, to have decidable equality, and to be nonempty. For each index $i$ a square real matrix $P_i$ whose rows and columns are indexed by $W_i$, i.e. a function $P_i : W_i \times W_i \to \mathbb{R}$. For each index $i$ a real-valued function $\pi_i : W_i \to \mathbb{R}$. Three further real numbers $\gamma$, $c_0$, $\varepsilon$.

Throughout, write

$$\mathcal{X} \;=\; \prod_{j=0}^{n-1} W_j$$

for the product state space (a finite, nonempty type with decidable equality, since each factor is).

The hypotheses, with every custom notion expanded

1. $2 \le n$. In particular $n \ne 0$, so $\mathrm{Fin}\,n$ is nonempty and every "for all $i$" hypothesis below has at least two instances; none of them is vacuous.

2. Each $P_i$ is stochastic (IsStochastic): for all $x, y \in W_i$, $P_i(x,y) \ge 0$, and for every $x \in W_i$, $\sum_{y \in W_i} P_i(x,y) = 1$.

3. Each $P_i$ is irreducible (Irreducible, the definition local to this development, not the ring-theoretic Irreducible of Mathlib): for all $x, y \in W_i$ there exists a natural number $t$ with $(P_i^{\,t})(x,y) > 0$. Note that $t = 0$ is permitted and $P_i^{0}$ is the identity matrix, so every instance with $x = y$ is satisfied automatically by $t = 0$; the content of the hypothesis is the case $x \ne y$.

4. Each state space has at least two points: $2 \le \#W_i$ for every $i$.

5. Each $\pi_i$ is stationary for $P_i$ (IsStationary), which unfolds to two things: (a) $\pi_i$ is a probability distribution (IsDist), i.e. $\pi_i(x) \ge 0$ for all $x$ and $\sum_{x \in W_i} \pi_i(x) = 1$; and (b) $\pi_i$ is a left fixed vector, $\sum_{x \in W_i} \pi_i(x) P_i(x,y) = \pi_i(y)$ for every $y \in W_i$.

6. Each pair $(P_i, \pi_i)$ satisfies detailed balance (DetailedBalance): for all $x, y \in W_i$,

$$\pi_i(x)\, P_i(x,y) \;=\; \pi_i(y)\, P_i(y,x).$$

Given hypotheses 2 and 5(a), this hypothesis already implies part (b) of hypothesis 5 (sum hypothesis 6 over $x$ and use that the rows of $P_i$ sum to $1$), so the left-fixed-vector half of the stationarity assumption is redundant here; the distribution half is not.

7. $0 < \gamma$.

8. Uniform spectral gap: for every $i$, $\gamma \le \operatorname{gap}(P_i)$, where the gap is defined as

$$\operatorname{gap}(P_i) \;=\; 1 - \lambda_2(P_i), \qquad \lambda_2(P_i) \;=\; \sup\{\lambda \in \mathbb{R} \;:\; \lambda \text{ is a real eigenvalue of } P_i \text{ and } \lambda \ne 1\},$$

and "$\lambda$ is a real eigenvalue of $P_i$" means: there exists a function $f : W_i \to \mathbb{R}$ which is not identically zero with $\sum_{y} P_i(x,y) f(y) = \lambda f(x)$ for all $x$ (a right eigenvector). Only real eigenvalues are considered; complex eigenvalues of $P_i$ play no role in this definition. The exclusion is of the value $1$, not of one copy of the eigenvalue $1$: if $1$ were an eigenvalue of multiplicity greater than one, it would still be excluded entirely.

9. $0 < c_0$.

10. Uniform lower bound on the stationary masses: for every $i$,

$$c_0 \;\le\; \sqrt{\ \inf_{x \in W_i} \pi_i(x)\ }.$$

Since $W_i$ is finite and nonempty, the infimum is an actual minimum over $W_i$.

11. $0 < \varepsilon$ and $\varepsilon < 1$ (strict on both sides).

The two conclusions

Let $Q$ denote the product chain built from the family $P$ (productChain): the matrix on $\mathcal{X} \times \mathcal{X}$ given by

$$Q(x,y) \;=\; \frac{1}{n} \sum_{i=0}^{n-1} C_i(x,y), \qquad C_i(x,y) \;=\; \begin{cases} P_i(x_i, y_i) & \text{if } y_j = x_j \text{ for every } j \ne i,\\[2pt] 0 & \text{otherwise.}\end{cases}$$

(That is: pick a coordinate $i$ uniformly at random and move that coordinate according to $P_i$, leaving the others fixed. Note that when $x = y$ every index $i$ satisfies the side condition, so $Q(x,x) = \frac1n\sum_i P_i(x_i,x_i)$.)

Let $\pi$ denote the product function $\pi(x) = \prod_{i=0}^{n-1} \pi_i(x_i)$ on $\mathcal{X}$. Nothing in the statement asserts that $\pi$ is stationary for $Q$; it is simply the reference function fed to the mixing-time definition.

The quantity being bounded is the continuous-time mixing time $T := \mathrm{contMixingTime}(Q, \pi, \varepsilon)$, a real number defined as

$$T \;=\; \inf\ \{\, t \in \mathbb{R} \;:\; 0 \le t \ \text{ and } \ D(t) \le \varepsilon \,\},$$

where

$$D(t) \;=\; \max_{x \in \mathcal{X}} \ \sup_{A \subseteq \mathcal{X}} \left| \sum_{y \in A} H_t(x,y) \;-\; \sum_{y \in A} \pi(y) \right|,$$

the inner supremum ranging over all finite subsets $A$ of $\mathcal{X}$ (all subsets, since $\mathcal{X}$ is finite; $A = \varnothing$ is included, so the inner quantity is $\ge 0$), and where $H_t$ is the heat kernel

$$H_t(x,y) \;=\; \sum_{k=0}^{\infty} \frac{e^{-t}\, t^{k}}{k!}\, (Q^{k})(x,y),$$

an infinite series (a tsum) in the real numbers. The outer maximum is over the nonempty finite type $\mathcal{X}$.

The theorem asserts the conjunction of the following two claims.

(A) An upper bound, asserted unconditionally under the hypotheses above:

$$T \;\le\; \frac{1}{2\gamma}\, n \,\log n \;+\; \frac{1}{\gamma}\, n \, \log\!\left(\frac{1}{c_0\,\varepsilon}\right),$$

where $\log$ is the natural logarithm and $n$ is coerced from a natural number to a real. (Grouping is as written: $((2\gamma)^{-1} \cdot n) \cdot \log n$ and $(\gamma^{-1} \cdot n) \cdot \log(1/(c_0\varepsilon))$.)

(B) A conditional lower bound: if additionally $\operatorname{gap}(P_i) = \gamma$ for every $i$ (exact equality, for all coordinates), then

$$\frac{n}{2\gamma}\Bigl(\log n \;-\; \log\bigl(8 \log \tfrac{1}{1-\varepsilon}\bigr)\Bigr) \;\le\; T.$$

The antecedent of (B) is strictly stronger than hypothesis 8, which it subsumes; under that antecedent hypothesis 8 carries no extra information. If the antecedent fails for the given family, conjunct (B) holds trivially and only (A) has content. Conversely, the antecedent is satisfiable (e.g. take all $P_i$ equal), so (B) is not vacuous as a general claim.

Junk-value and degenerate-branch conventions

The following total-function conventions are in force; for each, I state whether the stated hypotheses make the degenerate branch reachable.

• Infimum of an empty or unbounded set of reals (sInf). The mixing time $T$ is an infimum over $S = \{t \in \mathbb{R} : 0 \le t,\ D(t) \le \varepsilon\}$. This set is bounded below by $0$ by construction, so the "unbounded below" junk branch is unreachable. However, if $S$ is empty — i.e. if no nonnegative time brings $D(t)$ down to $\varepsilon$ — the convention gives $T = 0$. No hypothesis in the statement asserts that $S$ is nonempty, so as written the branch is not syntactically excluded; whether it is actually reachable depends on the mathematical consequences of hypotheses 2–11. In that branch, claim (A) reduces to "$0 \le$ the right-hand side" and claim (B) to "the left-hand side $\le 0$".

• Supremum of an empty or unbounded set of reals (sSup), inside $\lambda_2$. If a matrix $P_i$ had no real eigenvalue other than $1$ (or an unbounded such set), $\lambda_2(P_i)$ would be $0$ by convention and $\operatorname{gap}(P_i)$ would be $1$. Nothing in the statement rules this branch out by fiat; it is excluded only through the mathematical content of hypotheses 2, 3, 6 and 10 (a stochastic matrix that is irreducible in the above sense and reversible with respect to a strictly positive $\pi_i$ has a full real spectrum in $[-1,1]$ with $1$ simple, so the set is nonempty and bounded). The reader should note that if this branch were reached, $\operatorname{gap}$ would take the value $1$ rather than being undefined, and hypothesis 8 would then merely say $\gamma \le 1$.

• Infimum over an empty index type, in $\inf_x \pi_i(x)$. Unreachable: each $W_i$ carries a Nonempty instance (and $2 \le \#W_i$), so the infimum is a genuine minimum over a nonempty finite set.

• Square root of a negative number. Real.sqrt returns $0$ on nonpositive inputs. Combined with $c_0 > 0$, hypothesis 10 therefore forces $\min_x \pi_i(x) > 0$; more precisely it forces

$$\pi_i(x) \;\ge\; \min_{x'} \pi_i(x') \;\ge\; c_0^2 \;>\; 0 \quad\text{for every } i \text{ and every } x \in W_i.$$

So hypothesis 10 is a genuine strict-positivity assumption on every stationary weight, and the "$\sqrt{\text{negative}} = 0$" branch is unreachable given $c_0 > 0$. It also forces $c_0 \le \sqrt{1/2}$, since $\pi_i$ sums to $1$ over a set of at least $2$ points, so $\min_x \pi_i(x) \le 1/2$.

• Logarithm of a nonpositive number. Real.log returns $0$ on nonpositive inputs. Each occurrence has a strictly positive argument under the hypotheses, so this branch is unreachable: $\log n$ has $n \ge 2 > 0$; $\log(1/(c_0\varepsilon))$ has $c_0 \varepsilon > 0$; $\log\frac{1}{1-\varepsilon}$ has $1 - \varepsilon > 0$ because $\varepsilon < 1$; and $\log\bigl(8\log\frac{1}{1-\varepsilon}\bigr)$ has a positive argument because $\varepsilon > 0$ gives $\frac{1}{1-\varepsilon} > 1$ and hence $\log\frac1{1-\varepsilon} > 0$. Note that the values may still be negative: $\log(1/(c_0\varepsilon)) > 0$ always here (since $c_0\varepsilon < \sqrt{1/2} < 1$), while $\log\bigl(8\log\frac1{1-\varepsilon}\bigr)$ is negative for small $\varepsilon$ (precisely when $\varepsilon < 1 - e^{-1/8} \approx 0.1175$), which makes the left-hand side of (B) larger.

• Division by zero / inverse of zero. Real division and inversion return $0$ at $0$. All divisors here are nonzero: $n^{-1}$ in the definition of $Q$ has $n \ge 2$; $(2\gamma)^{-1}$, $\gamma^{-1}$ and $n/(2\gamma)$ have $\gamma > 0$; $1/(c_0\varepsilon)$ has $c_0, \varepsilon > 0$; $1/(1-\varepsilon)$ has $\varepsilon < 1$; the $1/k!$ in the heat kernel is never a division by zero. So no junk-division branch is reachable.

• Sum of a non-summable family (tsum). The heat-kernel entries are defined by an infinite series which, if not summable, would be assigned the value $0$. For each fixed real $t$ and each finite matrix $Q$ the series converges absolutely, so this branch is unreachable. At $t = 0$ the convention $0^0 = 1$ makes $H_0$ the identity matrix.

• Natural-number subtraction, floors, ceilings. None occur. $T$ is a real number, not a natural number; no rounding is applied to either bound.

• Suprema over $\mathcal{X}$ and over subsets. Both the outer maximum over starting states and the inner supremum over subsets range over nonempty finite index sets ($\mathcal{X}$ is nonempty since every $W_j$ is, and the empty subset always exists), so no empty-supremum convention is invoked.

Satisfiability

The hypothesis package is satisfiable, so the theorem is not vacuous: take $n = 2$, $W_0 = W_1$ a two-element type, $P_0 = P_1 = \begin{pmatrix} 1/2 & 1/2 \\ 1/2 & 1/2\end{pmatrix}$, $\pi_0 = \pi_1$ uniform, $\gamma = 1$, $c_0 = 1/2$, $\varepsilon = 1/2$; all of hypotheses 1–11 hold (and the antecedent of (B) holds as well).