The homogeneous chain measure is a trajectory measure

Proved

MarkovChainCLT.chainMeasure_eq_trajMeasure

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

ionescu-tulceamarkov-chaintrajectory-measure

For a Markov kernel $P$ and initial probability law $\lambda$ , the homogeneous path law constructed as chainMeasure is equal to Mathlib's Ionescu–Tulcea trajectory measure for the homogeneous transition family induced by $P$ :

\operatorname{chainMeasure}(P,\lambda)=\operatorname{trajMeasure}(\lambda,\operatorname{markovChainStep}(P)).

This identification makes the generic trajectory-kernel conditional-expectation API available for homogeneous Markov chains.

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.chainMeasure_eq_trajMeasure {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P]
    (lam : Measure X) [IsProbabilityMeasure lam] :
    chainMeasure P lam = Kernel.trajMeasure lam (BanditAlgorithm.markovChainStep P) := by sorry

Source

Mathlib, Probability/Kernel/IonescuTulcea/Traj.lean, definition `Kernel.trajMeasure`, and this mission's `Definitions.Def_MarkovChainPathMeasure`, definitions `chainMeasure` and `BanditAlgorithm.markovChainKernel`, at mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f.

View graph