Functional processes inherit $\alpha$-mixing (finite measure): $0 \le \alpha_g(n) \le \alpha(n)$

Let $P$ be a finite measure on $\Omega$, let $Y = \{Y_i\}_{i \ge 0}$ be a sequence of random elements of $\mathsf{X}$, and let $g : \mathsf{X} \to \mathsf{E}$ be measurable. Write $\alpha(n)$ for the strong ($\alpha$-) mixing coefficient of $Y$ at lag $n$ and $\alpha_g(n)$ for that of the functional process $\{g(Y_i)\}_{i \ge 0}$. Then

Since $g$ is measurable, $\sigma(g(Y_i) : i \in S) \subseteq \sigma(Y_i : i \in S)$, so the family of event (or variable) pairs over which $\alpha_g(n)$ is a supremum is a subfamily of the one defining $\alpha(n)$; the inequality is monotonicity of the supremum, and nonnegativity holds because every member of the family is an absolute value.

Why finiteness is needed. The coefficients are defined as suprema of sets of reals, and in Lean the supremum of a set that is not bounded above is $0$ by convention. For a general (non-finite) measure the family defining $\alpha(n)$ can be unbounded — making $\alpha(n) = 0$ — while the smaller family defining $\alpha_g(n)$ stays bounded with a strictly positive supremum, and the inequality then fails. Finiteness of $P$ makes both families bounded above (by $P(\Omega) + P(\Omega)^2$, respectively $1 + P(\Omega)$), which is exactly what makes the comparison of suprema legitimate. In the Markov chain application $P$ is the law of the chain, a probability measure, so the hypothesis is free.

This is the step "by an earlier remark $\alpha_f(n) \le \alpha(n)$ for all $n \ge 1$" in Jones's proof of Corollary 1, which lets a mixing central limit theorem stated for a general stationary sequence be applied to the functional process $\{f(X_n)\}$ of a Markov chain.