Every rho-mixing coefficient of a finite measure lies in [0,1]

Proved

MarkovChainCLT.rhoMixingCoef_nonneg_le_one_of_finite

by Zehao Jin · Aug 21, 2026 · Mathlib c5ea003 (Lean v4.30.0)

cauchy-schwarzmaximal-correlationmixingprobability

Let $P$ be a finite measure and let $(Y_i)_{i\ge0}$ be a measurable-space-valued process. For every lag $n$ , its maximal-correlation mixing coefficient satisfies

0\le\rho(n)\le1.

The result remains valid for a finite, not necessarily normalized, measure because the coefficient is a supremum of normalized covariances and Cauchy--Schwarz bounds every candidate by one. Zero variances are handled by the convention that division by zero in the real numbers gives zero.

This theorem supplies the order bounds needed whenever rho coefficients are treated as a real-valued decay sequence.

Preamble

import Definitions.Def_MixingCoefficients
import Mathlib.MeasureTheory.Integral.MeanInequalities

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory

Formal statement

theorem MarkovChainCLT.rhoMixingCoef_nonneg_le_one_of_finite
    {Ω E : Type*} [MeasurableSpace Ω] [MeasurableSpace E]
    (P : Measure Ω) [IsFiniteMeasure P] (Y : ℕ → Ω → E) (n : ℕ) :
    0 ≤ rhoMixingCoef P Y n ∧ rhoMixingCoef P Y n ≤ 1 := by sorry

Source

Richard C. Bradley, On Mixing Properties of Reversible Markov Chains, arXiv:1403.4895v1, pp. 2--3, definition (1.3), https://arxiv.org/abs/1403.4895. The range [0,1] is the Cauchy--Schwarz range of the absolute Pearson correlation whose supremum defines maximal correlation.

View graph