Functional processes inherit $\rho$-mixing: $0 \le \rho_g(n) \le \rho(n)$

⚠️ DEPRECATED — this statement is FALSE as written

Do not attempt to prove this theorem: it has a counterexample. Deprecated by its submitter (LukeBernese). Use refMarkovChainCLT.rhoMixingCoef_comp_nonneg_le_of_finite instead, which is the same statement with the missing [IsFiniteMeasure P] hypothesis.

Why it is false. The mixing coefficients are defined as sSup of a set 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 $\rho(n)$ can be unbounded — forcing $\rho(n) = 0$ — while the smaller family defining $\rho_g(n)$ stays bounded with a strictly positive supremum. Then $\rho_g(n) > \rho(n)$ and the inequality fails.

Explicit counterexample. Take $\Omega = \mathbb{N}$ with the full $\sigma$-algebra and $P$ the counting measure, $Y_i = \mathrm{id}$ for all $i$, and $g(k) = [k = 0]$ into $\{0,1\}$. The family for $Y$ contains $|P(A \cap B) - P(A)P(B)| = |(N{+}1) - (N{+}1)^2| \to \infty$ at $A = B = \{0,\dots,N\}$, so it is unbounded and $\rho(n) = 0$. The functional family, generated by $\{\emptyset, \{0\}, \mathbb{N} \setminus \{0\}, \mathbb{N}\}$, contains the value $1$ at $A = \{0\}$, $B = \mathbb{N}$ (since $P(\mathbb{N}) = \infty$ has toReal = 0), so $\rho_g(n) \ge 1 > 0 = \rho(n)$.

With [IsFiniteMeasure P] every candidate value is bounded by $P(\Omega) + P(\Omega)^2$, both families are bounded above, and the comparison of suprema is legitimate. In the Markov chain application the measure is the law of the chain, a probability measure, so the added hypothesis costs nothing.

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

The upper bound is the standard observation used throughout the Markov chain CLT literature: since $g$ is measurable, $\sigma(g(Y_i) : i \in S) \subseteq \sigma(Y_i : i \in S)$ for every index set $S$, so the supremum defining $\rho_g(n)$ ranges over a subfamily of the pairs used for $\rho(n)$. The lower bound records that a mixing coefficient is a supremum over a family containing the trivial (zero) witness, hence nonnegative.

This is exactly the step "by an earlier remark $\rho_f(n) \le \rho(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.