1. Alpha Mixing🔗

Created: 2026-08-04 · Last updated: 2026-08-12

This note is the first in a series that will discuss the α mixing coefficient, or strong mixing coefficient. It's a convenient measure of dependence between random variables. My main reference the book E. Rio (2017).

Probability space.

To properly define the coefficient in Lean, we first introduce a probability space Ω with measure ℙ.

The types of the elements of Ω are left unspecified: they could be real values or something more exotic.

Definition of α-mixing coefficient

The α-mixing coefficient between two σ-algebras 𝓐 and 𝓑 is defined by \alpha(\mathcal{A} , \mathcal{B}) := 2\sup\{|\mathbb{P}(A \cap B) - \mathbb{P}(A)\mathbb{P}(B)| : (A,B) \in \mathcal{A} \times \mathcal{B}\}.

By default, the measure of a set, ℙ A say, is an extended non-negative real number ([0,∞], ℝ≥0∞ or ENNReal for short). Substractions on [0,∞] are not always well-defined. Thus, the slightly convoluted definition below: we cast everything to real numbers, take its absolute value, and then cast the result back up to ENNReal. The α-mixing coefficient is also ENNReal as the supremum of a possibly (as far as Lean knows) empty set.

The α-mixing coefficient measures the dependence between 𝓐 and 𝓑. For instance, α(𝓐, 𝓑) is zero iff 𝓐 and 𝓑 are independent.

On the other end of the spectrum, the maximum value is 1/2. We start with an intermediate lemma to handle a simple arithmetic operation in ENNReal.

Now the nice lemma with the ugly proof.