Set-integral Fubini formula for trajectory continuation

Proved

MarkovChainCLT.setIntegral_trajMeasure_eq_integral_continuation

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

fubinimarkov-kernelset-integraltrajectory-measure

For an Ionescu–Tulcea trajectory measure, a measurable set $S$ , and a function $F$ integrable on $S$ , the set integral can be disintegrated over the random prefix through time $j$ :

\int_S F(z)\,\mu(dz) =\int\left[\int_S F(y)\,\operatorname{traj}_j(x,dy)\right]\mu_j(dx),

where $\mu_j$ is the distribution of the finite prefix. This is the specialized kernel-Fubini identity for restarting a trajectory from its observed prefix.

Preamble

import Definitions.Def_MarkovChainPathMeasure
import Theorems.Thm_MarkovChainCLT_traj_comp_map_frestrict_trajMeasure

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

Formal statement

theorem MarkovChainCLT.setIntegral_trajMeasure_eq_integral_continuation
    {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) → ℝ} {s : Set (Π n, X n)}
    (hs : MeasurableSet s)
    (hF : IntegrableOn F s (Kernel.trajMeasure lam kappa)) :
    ∫ z in s, F z ∂Kernel.trajMeasure lam kappa =
      ∫ x, (∫ y in s, F y ∂Kernel.traj kappa j x)
        ∂((Kernel.trajMeasure lam kappa).map (frestrictLe j)) := by sorry

Source

Mathlib, Probability/Kernel/Composition/IntegralCompProd.lean, theorem `Kernel.setIntegral_comp`, and Probability/Kernel/IonescuTulcea/Traj.lean, trajectory restart identities, at mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f.

View graph