Maximal-correlation submultiplicativity from a two-sided conditional-expectation representative

Proved

MarkovChainCLT.rhoMixingCoef_submultiplicative_of_condExp_bridge

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. Suppose that for every square-integrable future random variable $V$ , its conditional expectation given the history through the intermediate time $k+m$ has a version $W$ that is measurable both with respect to that history and with respect to the future beginning at $k+m$ . Then the maximal-correlation coefficients satisfy

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

This version-based formulation is insensitive to the almost-everywhere choice of conditional-expectation representative and is the form naturally supplied by the Markov property, where $W$ can be chosen as a measurable function of the state at time $k+m$ .

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_bridge
    {Ω 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 →
      ∃ W : Ω → ℝ,
        Measurable[processSigma Y (Set.Iic (k + m))] W ∧
        Measurable[processSigma Y (Set.Ici (k + m))] W ∧
        W =ᵐ[P] 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 version-invariant conditional-expectation argument behind equation (1.11).

View graph