Increment paths and the natural past

This file defines the path of increments after a deterministic time, proves its Borel measurability, and identifies the σ-algebra of a restricted path with the σ-algebra generated by its evaluations, the setting of the simple Markov property (J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter I).

noncomputable def BGW.Skorokhod.shiftIncrement {T s : ℝ} (hs : 0 ≤ s) (hsT : s ≤ T) (f : D T ℝ) : D (T - s) ℝ

The increment path after the deterministic time s: t ↦ f (s + t) - f s on [0, T - s].

Equations

• BGW.Skorokhod.shiftIncrement hs hsT f = { toFun := fun (t : ↑(Set.Icc 0 (T - s))) => f ⟨s + ↑t, ⋯⟩ - f ⟨s, ⋯⟩, isCadlag' := ⋯ }

theorem BGW.Skorokhod.measurable_shiftIncrement {T s : ℝ} (hs : 0 ≤ s) (hsT : s ≤ T) : Measurable (shiftIncrement hs hsT)

shiftIncrement is Borel measurable.

theorem BGW.Skorokhod.comap_restrict_eq_iSup_comap_eval {T s : ℝ} (hsT : s ≤ T) : MeasurableSpace.comap (restrict hsT) inferInstance = ⨆ (t : { t : ↑(Set.Icc 0 T) // ↑t ≤ s }), MeasurableSpace.comap (fun (f : D T ℝ) => f ↑t) inferInstance

Natural-past identification: the σ-algebra pulled back by restrict hsT is the σ-algebra generated by the evaluations at times ≤ s (both sides are σ-algebras on D T ℝ).