Bounds and submultiplicativity of rho for a stationary Markov chain

Open

MarkovChainCLT.rhoMixingCoef_chain_bounds_submultiplicative

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

markov-chainmaximal-correlationmixingprobability

Let $(X_n)_{n\ge0}$ be the stationary Markov chain with transition kernel $P$ and invariant probability law $\mu$ , and let $\rho(n)$ be its maximal-correlation mixing coefficient. Then

0\le\rho(n)\le1,\qquad\rho(m+n)\le\rho(m)\rho(n)\quad(m,n\ge0).

The range bound is the Cauchy--Schwarz bound for correlation. The product inequality is the maximal-correlation data-processing inequality applied through the intermediate Markov state. It is the structural fact that turns any strict contraction at one lag into an exponential mixing rate.

Formalization Note The coefficient is defined from the past and future coordinate sigma-fields of the one-sided stationary path measure. The zero-lag cases are included; they are the endpoint extension of the positive-lag formula using the same range bound.

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_bounds_submultiplicative
    {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P]
    (μ : Measure X) [IsProbabilityMeasure μ]
    (hμ : Kernel.Invariant P μ) :
    (∀ n : ℕ,
      0 ≤ rhoMixingCoef (chainMeasure P μ) (fun i ω => ω i) n ∧
        rhoMixingCoef (chainMeasure P μ) (fun i ω => ω i) n ≤ 1) ∧
      ∀ 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) reduces past--future rho to two-coordinate maximal correlation for stationary Markov chains, and equation (1.11) states rho(m+n) <= rho(m)rho(n). The bound 0 <= rho <= 1 follows from the maximal-correlation definition (1.3), pp. 2--3.

View graph