Strict contraction of a submultiplicative sequence implies exponential decay

Proved

MarkovChainCLT.exponential_decay_of_submultiplicative

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

analysismarkov-chainmixingprobability

Let $(r_n)_{n\ge 0}$ be a sequence of real numbers satisfying $0\le r_n\le 1$ and the submultiplicative inequality $r_{m+n}\le r_m r_n$ . Suppose there are an integer $N\ge 1$ and a number $q\in(0,1)$ such that $r_N\le q$ . Then there exist constants $c\ge 0$ and $\theta>0$ for which

r_n\le c e^{-\theta n}\qquad(n\ge 1).

This isolates the deterministic analytic step that converts a strict maximal-correlation contraction at one lag into a quantitative exponential mixing rate. It is reusable for mixing coefficients and operator norms once their submultiplicativity has been established.

Preamble

import Mathlib

Formal statement

namespace MarkovChainCLT

theorem exponential_decay_of_submultiplicative
    (r : ℕ → ℝ)
    (hr_nonneg : ∀ n, 0 ≤ r n)
    (hr_one : ∀ n, r n ≤ 1)
    (hr_mul : ∀ m n, r (m + n) ≤ r m * r n)
    (N : ℕ) (hN : 1 ≤ N)
    (q : ℝ) (hq_pos : 0 < q) (hq_lt : q < 1)
    (hrN : r N ≤ q) :
    ∃ c θ : ℝ, 0 ≤ c ∧ 0 < θ ∧
      ∀ n : ℕ, 1 ≤ n → r n ≤ c * Real.exp (-θ * n) := by sorry

end MarkovChainCLT

Source

Richard C. Bradley, Basic Properties of Strong Mixing Conditions: A Survey and Some Open Questions, Probability Surveys 2 (2005), pp. 118–119, Theorem 3.3(1), https://arxiv.org/abs/math/0511078. This theorem formalizes the submultiplicative real-sequence step underlying the stated exponential rho-mixing conclusion.

View graph