Markov conditional expectation admits a current-state version

Open

MarkovChainCLT.chain_condExp_future_bridge

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

conditional-expectationmarkov-chainsmixingprobability

For a Markov chain with path law chainMeasure P lam, let $V$ be a square-integrable random variable determined by the trajectory from time $j+n$ onward. Then the conditional expectation $\mathbb E[V\mid\mathcal F_{\le j}]$ has a version $W$ that is measurable both with respect to the past through time $j$ and with respect to the future from time $j$ onward. Equivalently, the Markov property permits the conditional expectation to be represented by a measurable function of the current state $X_j$ . The conclusion is stated using an almost-everywhere version because conditional expectations are unique only almost surely.

Preamble

import Definitions.Def_MarkovChainPathMeasure
import Definitions.Def_MixingCoefficients
import Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

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

Formal statement

theorem MarkovChainCLT.chain_condExp_future_bridge
    {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P]
    (lam : Measure X) [IsProbabilityMeasure lam]
    (j n : ℕ) (V : (ℕ → X) → ℝ)
    (hVm : Measurable[processSigma (fun i (ω : ℕ → X) => ω i) (Set.Ici (j + n))] V)
    (hV : MemLp V 2 (chainMeasure P lam)) :
    ∃ W : (ℕ → X) → ℝ,
      Measurable[processSigma (fun i (ω : ℕ → X) => ω i) (Set.Iic j)] W ∧
      Measurable[processSigma (fun i (ω : ℕ → X) => ω i) (Set.Ici j)] W ∧
      W =ᵐ[chainMeasure P lam]
        MeasureTheory.condExp
          (processSigma (fun i (ω : ℕ → X) => ω i) (Set.Iic j))
          (chainMeasure P lam) V := by sorry

Source

Richard C. Bradley, Basic Properties of Strong Mixing Conditions. A Survey and Some Open Questions, arXiv:1403.4895, p. 4, equation (1.10); G. L. Jones, On the Markov Chain Central Limit Theorem, Probability Surveys 1 (2004), Section 2; standard Markov conditional-expectation property.

View graph