Prove2Me

ρ(n)≤2φ(n)\rho(n)\le 2\sqrt{\varphi(n)} (Cogburn--Ibragimov inequality)

Proved
MarkovChainCLT.rhoMixingCoef_le_two_mul_sqrt_phiMixingCoef

by Gabewhigham · Sep 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

markov-chainsmixingprobability

Let Y=(Yn)n≥0Y=(Y_n)_{n\ge 0} be a sequence of random variables on a probability space (Ω,F,P)(\Omega,\mathcal F,P), and for a lag nn let

φ(n)=sup⁡k sup⁡{ ∣P(B∣A)−P(B)∣ : A∈σ(Y0,…,Yk), P(A)≠0, B∈σ(Yj:j≥k+n) }\varphi(n)=\sup_k\ \sup\bigl\{\,|P(B\mid A)-P(B)|\ :\ A\in\sigma(Y_0,\dots,Y_k),\ P(A)\neq 0,\ B\in\sigma(Y_j: j\ge k+n)\,\bigr\}

be the uniform (φ\varphi-) mixing coefficient and let ρ(n)\rho(n) be the maximal-correlation (ρ\rho-) mixing coefficient, the supremum of ∣corr⁡(U,V)∣|\operatorname{corr}(U,V)| over square-integrable UU measurable for the past σ(Y0,…,Yk)\sigma(Y_0,\dots,Y_k) and VV measurable for the future σ(Yj:j≥k+n)\sigma(Y_j : j\ge k+n).

Then the two coefficients are comparable through

ρ(n) ≤ 2 φ(n)(n≥0).\rho(n)\ \le\ 2\,\sqrt{\varphi(n)}\qquad (n\ge 0).

Equivalently, at the level of two σ\sigma-fields A,B\mathcal A,\mathcal B, this is the classical inequality ρ(A,B)≤2[φ(A,B)]1/2\rho(\mathcal A,\mathcal B)\le 2[\varphi(\mathcal A,\mathcal B)]^{1/2} of Cogburn and Ibragimov: for U∈L2(A)U\in L^2(\mathcal A) and V∈L2(B)V\in L^2(\mathcal B),

∣Cov⁡(U,V)∣ ≤ 2φ(A,B) Var⁡(U) Var⁡(V).|\operatorname{Cov}(U,V)|\ \le\ 2\sqrt{\varphi(\mathcal A,\mathcal B)}\ \sqrt{\operatorname{Var}(U)}\,\sqrt{\operatorname{Var}(V)} .

Taking the supremum over lags kk on both sides and using monotonicity of the square root gives the stated form for sequences.

This is the bridge from uniform mixing to maximal-correlation mixing: it turns the summability hypothesis ∑nφ(n)<∞\sum_n\sqrt{\varphi(n)}<\infty of the Billingsley uniform-mixing central limit theorem into the summability hypothesis ∑nρ(n)<∞\sum_n\rho(n)<\infty of the Ibragimov ρ\rho-mixing central limit theorem.

Preamble
import Definitions.Def_MixingCoefficients

open MeasureTheory ProbabilityTheory

/-- The Cogburn-Ibragimov comparison of the maximal-correlation and uniform mixing
coefficients of a sequence. -/
Formal statement
theorem MarkovChainCLT.rhoMixingCoef_le_two_mul_sqrt_phiMixingCoef
    {Ω E : Type*} [MeasurableSpace Ω] [MeasurableSpace E]
    (P : Measure Ω) [IsProbabilityMeasure P] (Y : ℕ → Ω → E) (n : ℕ) :
    rhoMixingCoef P Y n ≤ 2 * Real.sqrt (phiMixingCoef P Y 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/0511078v1, Section 1.1, eq. (1.13): rho(A,B) <= 2[phi(A,B)]^{1/2}[phi(B,A)]^{1/2} <= 2[phi(A,B)]^{1/2}, attributed there to Cogburn (1960) and Ibragimov (1962); see also J. L. Doob, Stochastic Processes (1953), p. 222, Lemma 7.1.

View graph