Prove2Me

The rho-mixing coefficients of a stationary Markov chain are submultiplicative

Proved
MarkovChainCLT.rhoMixingCoef_chain_submultiplicative

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

data-processingmarkov-chainmaximal-correlationmixingprobability

Let (Xn)n≥0(X_n)_{n\ge0} be the stationary Markov chain with transition kernel PP and invariant probability law μ\mu. Its maximal-correlation mixing coefficients obey

ρ(m+n)≤ρ(m)ρ(n)(m,n≥0).\rho(m+n)\le\rho(m)\rho(n)\qquad(m,n\ge0).

This is the multiplicative data-processing inequality for maximal correlation. The Markov property makes the past and the remote future conditionally independent through an intermediate state, so correlation across two consecutive time gaps contracts by at most the product of the two individual contraction factors.

Formalization Note The zero-lag endpoint is included together with the positive-lag formula and uses the standard range property of maximal correlation.

Preamble
import Definitions.Def_MarkovErgodicity
import Definitions.Def_MarkovChainPathMeasure
import Definitions.Def_MixingCoefficients

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory
Formal statement
theorem MarkovChainCLT.rhoMixingCoef_chain_submultiplicative
    {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P]
    (μ : Measure X) [IsProbabilityMeasure μ]
    (hμ : Kernel.Invariant P μ) :
    ∀ m n : ℕ,
      rhoMixingCoef (chainMeasure P μ) (fun i ω => ω i) (m + n) ≤
        rhoMixingCoef (chainMeasure P μ) (fun i ω => ω i) m *
          rhoMixingCoef (chainMeasure P μ) (fun i ω => ω i) n := by sorry
Source
Richard C. Bradley, On Mixing Properties of Reversible Markov Chains, arXiv:1403.4895v1, p. 4, equations (1.10)--(1.11), https://arxiv.org/abs/1403.4895. Equation (1.10) is the Markov reduction to two-coordinate maximal correlation, and equation (1.11) gives rho(m+n) <= rho(m)rho(n).

View graph