Conditional expectation under a trajectory measure given a finite prefix

Proved

MarkovChainCLT.condExp_trajMeasure

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

conditional-expectationdisintegrationmarkov-kerneltrajectory-measure

For an Ionescu–Tulcea trajectory with initial law $\lambda$ , transition family $\kappa$ , and an integrable measurable path functional $f$ , conditioning on the coordinates through time $j$ is integration against the continuation kernel started from the observed prefix:

\mathbb E[f\mid\mathcal F_{\le j}](x) =\int f(y)\,\operatorname{traj}_j(\operatorname{frestrictLe}_j x,dy) \quad\text{a.e.}

Unlike Mathlib's fixed-prefix formula, this version is stated under the full trajectory measure with a random initial state. It is a reusable Markov disintegration theorem.

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.condExp_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)) :
    (Kernel.trajMeasure lam kappa)[f | piLE j] =ᵐ[Kernel.trajMeasure lam kappa]
      fun x => ∫ y, f y ∂Kernel.traj kappa j (frestrictLe j x) := 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