Strong mixing coefficients depend only on the law of the sequence

Proved

MarkovChainCLT.alphaMixingCoef_map_pathMap

by Nickrobbins95 · Sep 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainsmixingprobability

Let $(\Omega,\mathcal F,P)$ be a measure space and let $Y = \{Y_i\}_{i\ge 0}$ be a sequence of measurable maps $Y_i : \Omega \to E$ . Write $\widehat Y : \Omega \to E^{\mathbb N}$ , $\widehat Y(\omega) = (Y_i(\omega))_{i \ge 0}$ , for the associated path map, and let $P \circ \widehat Y^{-1}$ denote the law of the whole sequence on the product space $E^{\mathbb N}$ .

Then for every lag $n$ the strong mixing coefficient of $Y$ under $P$ coincides with the strong mixing coefficient of the coordinate process computed under the law of $Y$ :

\alpha_Y(n) \;=\; \alpha_{\mathrm{coord}}(n) \qquad \text{computed under } P \circ \widehat Y^{-1}.

In words: the strong mixing coefficients are a functional of the joint distribution of the sequence alone, and carry no further information about the underlying probability space on which the sequence happens to be realised. This is the formal content of the standard convention that mixing conditions are properties of a process rather than of a particular realisation of it.

The proof is measure-theoretic rather than probabilistic. For each index set $s \subseteq \mathbb N$ the process $\sigma$ -algebra satisfies

\sigma(Y_i : i \in s) \;=\; \widehat Y^{-1}\bigl(\sigma(z \mapsto z_i : i \in s)\bigr),

because forming preimages commutes with suprema of $\sigma$ -algebras. Consequently the pairs $(A,B)$ admissible in the supremum defining $\alpha_Y(n)$ are exactly the $\widehat Y$ -preimages of the pairs admissible for the coordinate process, and the pushforward identity $P(\widehat Y^{-1}C) = (P \circ \widehat Y^{-1})(C)$ makes the corresponding quantities $|P(A\cap B) - P(A)P(B)|$ equal term by term. The two sets of reals whose suprema define the coefficients are therefore literally the same set, so their suprema agree.

No finiteness or probability hypothesis on $P$ is required. Measurability of each $Y_i$ is used only to ensure that the coordinate-side witnesses are measurable for the ambient product $\sigma$ -algebra, which is what licenses the pushforward identity.

Preamble

import Definitions.Def_MixingCoefficients

open MeasureTheory ProbabilityTheory MarkovChainCLT
open scoped ENNReal NNReal Topology ProbabilityTheory

Formal statement

theorem MarkovChainCLT.alphaMixingCoef_map_pathMap {Ω E : Type*} [MeasurableSpace Ω]
    [MeasurableSpace E] (P : Measure Ω) (Y : ℕ → Ω → E) (hY : ∀ i, Measurable (Y i)) (n : ℕ) :
    alphaMixingCoef P Y n
      = alphaMixingCoef (Measure.map (fun ω i => Y i ω) P) (fun i (z : ℕ → E) => z i) n := by sorry

Source

R. C. Bradley, "Basic Properties of Strong Mixing Conditions. A Survey and Some Open Questions", Probability Surveys 2 (2005) 107-144, arXiv math/0511078, Section 1.1 (pp. 108-109), where the mixing coefficients alpha, rho and phi are defined purely from the joint distribution of the process and are therefore invariant under passage to the law; together with G. L. Jones, "On the Markov Chain Central Limit Theorem", Probability Surveys 1 (2004) 299-320, arXiv math/0409112v2, Section 3 (arXiv v2 p. 7), the elementary observation that mixing coefficients are computed from the process sigma-algebras generated by the sequence. This lemma is the measure-theoretic statement underlying that convention, in the encoding of Def_MixingCoefficients used by this mission.

View graph