Continuation-kernel integration preserves prefix-event integrals

Proved

MarkovChainCLT.setIntegral_continuation_trajMeasure

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

conditional-expectationdisintegrationset-integraltrajectory-measure

Let $\mu$ be an Ionescu–Tulcea trajectory measure and let $f$ be an integrable measurable path functional. For every event $S$ determined by the prefix through time $j$ , integrating the continuation expectation of $f$ over $S$ gives the original integral of $f$ over $S$ :

\int_S\left[\int f(y)\,\operatorname{traj}_j(\operatorname{prefix}_j x,dy)\right]\mu(dx) =\int_S f(x)\,\mu(dx).

This is the set-integral disintegration identity that characterizes conditional expectation under a trajectory measure with 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.setIntegral_continuation_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 : ℕ)
    {f : (Π n, X n) → ℝ} (mf : Measurable f)
    (hf : Integrable f (Kernel.trajMeasure lam kappa))
    (s : Set (Π n, X n)) (hs : MeasurableSet[piLE j] s) :
    ∫ x in s, (∫ y, f y ∂Kernel.traj kappa j (frestrictLe j x))
        ∂Kernel.trajMeasure lam kappa =
      ∫ x in s, f x ∂Kernel.trajMeasure lam kappa := by sorry

Source

Mathlib, Probability/Kernel/IonescuTulcea/Traj.lean, theorem `Kernel.condExp_traj`, together with `Kernel.traj_map_frestrictLe` and `Kernel.traj_comp_partialTraj`, at mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f.

View graph