A shifted continuation integral factors through the current state

Proved

MarkovChainCLT.continuation_integral_future_factor_current_state

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

conditional-expectationfactorizationmarkov-propertytrajectory-kernel

Fix a homogeneous Markov kernel $P$ , a present time $j$ , a future offset $n$ , and a measurable path functional $v$ . Continue a trajectory from an observed prefix through time $j$ , shift the resulting path to time $j+n$ , and integrate $v$ . This continuation integral depends on the observed prefix only through its final state:

\int v\bigl((y_{j+n+\ell})_{\ell\ge0}\bigr)\,\operatorname{traj}_j(\operatorname{prefix}_j\omega,dy) =r(\omega_j)

for a measurable function $r$ on the state space. This is the strong Markov restart/factorization identity needed to make the finite-past conditional expectation simultaneously future-measurable.

Preamble

import Definitions.Def_MarkovChainPathMeasure
import Theorems.Thm_MarkovChainCLT_traj_map_shift_eq_comap

open Filter Finset Function MeasurableSpace MeasureTheory Preorder ProbabilityTheory
open Filtration
open scoped ENNReal NNReal Topology ProbabilityTheory
open MarkovChainCLT

Formal statement

theorem MarkovChainCLT.continuation_integral_future_factor_current_state
    {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P]
    (j n : ℕ) (v : (ℕ → X) → ℝ) (hv : Measurable v) :
    ∃ r : X → ℝ, Measurable r ∧
      ∀ omega : ℕ → X,
        (∫ y, v (fun l => y (j + n + l))
          ∂Kernel.traj (BanditAlgorithm.markovChainStep P) j (frestrictLe j omega)) =
        r (omega j) := by sorry

Source

Mathlib, Probability/Kernel/IonescuTulcea/Traj.lean, trajectory map/restart identities, together with the mission theorem `MarkovChainCLT.traj_map_shift_eq_comap`; Bradley, On Mixing Properties of Reversible Markov Chains, arXiv:1403.4895v1, p. 4, Markov reduction eq. (1.10).

View graph