Restarting a trajectory measure from its finite prefix recovers it

Proved

MarkovChainCLT.traj_comp_map_frestrict_trajMeasure

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

disintegrationmarkov-kerneltrajectory-measure

Let an inhomogeneous Markov trajectory start from $\lambda$ . Map its full path law to the prefix through time $j$ , then restart the Ionescu–Tulcea trajectory kernel from that random prefix. The resulting full path law is the original trajectory measure:

\operatorname{traj}_j\circ_m(\operatorname{trajMeasure}(\lambda,\kappa)\circ\operatorname{frestrictLe}_j^{-1}) =\operatorname{trajMeasure}(\lambda,\kappa).

This is the disintegration/reconstruction identity needed to lift fixed-prefix conditional-expectation formulas to a random initial law.

Preamble

import Definitions.Def_MarkovChainPathMeasure

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

Formal statement

theorem MarkovChainCLT.traj_comp_map_frestrict_trajMeasure
    {X : ℕ → Type*} [∀ i, MeasurableSpace (X i)]
    (kappa : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1)))
    [∀ n, IsMarkovKernel (kappa n)]
    (lam : Measure (X 0)) [IsProbabilityMeasure lam] (j : ℕ) :
    (Kernel.traj kappa j) ∘ₘ ((Kernel.trajMeasure lam kappa).map (frestrictLe j)) =
      Kernel.trajMeasure lam kappa := by sorry

Source

Mathlib, Probability/Kernel/IonescuTulcea/Traj.lean, theorems `Kernel.traj_map_frestrictLe` and `Kernel.traj_comp_partialTraj`, at mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f.

View graph