Trajectory measures with s-finite initial laws

The Ionescu--Tulcea trajectory measure can start from an s-finite measure. Its joint law of a finite prefix and the following coordinate is the composition-product of the prefix law and the next transition kernel. This identity lets finite transport plans be glued without normalization.

The result and proof generalize Mathlib's ProbabilityTheory.Kernel.map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure, which assumes a probability initial law.

instance ProbabilityTheory.Kernel.trajMeasure.instSFinite {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] {κ : (n : ℕ) → Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} [∀ (n : ℕ), IsMarkovKernel (κ n)] {μ₀ : MeasureTheory.Measure (X 0)} [MeasureTheory.SFinite μ₀] : MeasureTheory.SFinite (trajMeasure μ₀ κ)

An s-finite initial law gives an s-finite trajectory measure.

instance ProbabilityTheory.Kernel.trajMeasure.instIsFiniteMeasure {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] {κ : (n : ℕ) → Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} [∀ (n : ℕ), IsMarkovKernel (κ n)] {μ₀ : MeasureTheory.Measure (X 0)} [MeasureTheory.IsFiniteMeasure μ₀] : MeasureTheory.IsFiniteMeasure (trajMeasure μ₀ κ)

A finite initial law gives a finite trajectory measure.

theorem ProbabilityTheory.Kernel.map_frestrictLe_trajMeasure_compProd_of_sFinite {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] {κ : (n : ℕ) → Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} [∀ (n : ℕ), IsMarkovKernel (κ n)] {μ₀ : MeasureTheory.Measure (X 0)} [MeasureTheory.SFinite μ₀] (n : ℕ) : (MeasureTheory.Measure.map (Preorder.frestrictLe n) (trajMeasure μ₀ κ)).compProd (κ n) = MeasureTheory.Measure.map (fun (x : (i : ℕ) → X i) => (Preorder.frestrictLe n x, x (n + 1))) (trajMeasure μ₀ κ)

For an s-finite initial law, the joint law of the prefix through time n and the next coordinate is the composition-product of the prefix law and the transition kernel at n.