Maximal-correlation submultiplicativity from the Markov projection property

Proved

MarkovChainCLT.rhoMixingCoef_submultiplicative_of_condExp_future

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

conditional-expectationmarkov-chainsmixingprobability

Let $Y$ be a measurable process on a probability space. Assume the following Markov projection property: whenever $V$ is square-integrable and measurable with respect to the future beginning at time $k+m+n$ , its conditional expectation given the history through time $k+m$ is already measurable with respect to the future beginning at time $k+m$ (in particular, this holds if that conditional expectation depends only on the state at time $k+m$ ). Then the maximal-correlation mixing coefficients are submultiplicative:

\rho(m+n) \le \rho(m)\rho(n).

The statement includes all zero-variance cases through the convention in the definition of rhoMixingCoef.

Preamble

import Definitions.Def_MixingCoefficients
import Theorems.Thm_MarkovChainCLT_rhoMixingCoef_nonneg_le_one_of_finite
import Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
import Mathlib.Probability.CondVar
import Mathlib.MeasureTheory.Integral.MeanInequalities

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory
open MarkovChainCLT

Formal statement

theorem MarkovChainCLT.rhoMixingCoef_submultiplicative_of_condExp_future
    {Ω E : Type*} [mΩ : MeasurableSpace Ω] [mE : MeasurableSpace E]
    (P : @Measure Ω mΩ) [IsProbabilityMeasure P] (Y : ℕ → Ω → E)
    (hY : ∀ i, Measurable (Y i))
    (hcond : ∀ (k m n : ℕ) (V : Ω → ℝ),
      Measurable[processSigma Y (Set.Ici (k + (m + n)))] V →
      MemLp V 2 P →
      Measurable[processSigma Y (Set.Ici (k + m))]
        (MeasureTheory.condExp (m₀ := mΩ)
          (processSigma Y (Set.Iic (k + m))) P V)) :
    ∀ m n : ℕ,
      rhoMixingCoef P Y (m + n) ≤ rhoMixingCoef P Y m * rhoMixingCoef P Y n := by sorry

Source

Richard C. Bradley, Basic Properties of Strong Mixing Conditions. A Survey and Some Open Questions, arXiv:math/0511078 (updated survey version arXiv:1403.4895), p. 4, equations (1.10)–(1.11). This theorem isolates the conditional-expectation projection argument used to obtain equation (1.11).

View graph