Reversal of increments on Skorokhod space

The reversed-increment path evaluates to f T - f ((T-u)-). Its càdlàg property uses left-continuity of the left-limit function and right-continuity of the original path. The map is the one of the duality lemma in J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter II, Lemma 2.

noncomputable def BGW.Skorokhod.reverseIncrementsFun {T : ℝ} (hT : 0 ≤ T) (f : D T ℝ) : ↑(Set.Icc 0 T) → ℝ

The reversed-increment function u ↦ f T - f ((T-u)-).

Equations

• BGW.Skorokhod.reverseIncrementsFun hT f u = f ⟨T, ⋯⟩ - Function.leftLim ⇑f ⟨T - ↑u, ⋯⟩

theorem BGW.Skorokhod.isCadlag_reverseIncrementsFun {T : ℝ} (hT : 0 ≤ T) (f : D T ℝ) : IsCadlag (reverseIncrementsFun hT f)

The reversed path is càdlàg, including at both endpoints.

noncomputable def BGW.Skorokhod.reverseIncrements {T : ℝ} (hT : 0 ≤ T) (f : D T ℝ) : D T ℝ

The time reversal of increments R f (u) = f T - f ((T-u)-), with f (0-) = f 0.

Equations

• BGW.Skorokhod.reverseIncrements hT f = { toFun := BGW.Skorokhod.reverseIncrementsFun hT f, isCadlag' := ⋯ }

theorem BGW.Skorokhod.reverseIncrements_apply {T : ℝ} (hT : 0 ≤ T) (f : D T ℝ) (u : ↑(Set.Icc 0 T)) : (reverseIncrements hT f) u = f ⟨T, ⋯⟩ - Function.leftLim ⇑f ⟨T - ↑u, ⋯⟩

Pointwise formula (definitional).

theorem BGW.Skorokhod.measurable_reverseIncrements {T : ℝ} (hT : 0 ≤ T) : Measurable (reverseIncrements hT)

reverseIncrements is Borel measurable.