Reversal of a pinned bridge path

The bridge reversal evaluates to the negative of the left limit at the reversed time. Unlike reversal of increments, it does not subtract the terminal value; on paths ending at zero the two operations coincide (J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter II, Lemma 2, for the reversal of increments).

noncomputable def BGW.Skorokhod.reverseBridgeFun (f : D 1 ℝ) : ↑(Set.Icc 0 1) → ℝ

The bridge reversal function s ↦ -f((1-s)-), defined on every path of D 1 ℝ (with f(0-) = f 0). On paths with f 1 = 0 it agrees with reverseIncrementsFun at T = 1; it preserves positive jumps (the sign flips together with the time).

Equations

• BGW.Skorokhod.reverseBridgeFun f s = -Function.leftLim ⇑f ⟨1 - ↑s, ⋯⟩

theorem BGW.Skorokhod.isCadlag_reverseBridgeFun (f : D 1 ℝ) : IsCadlag (reverseBridgeFun f)

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

noncomputable def BGW.Skorokhod.reverseBridge (f : D 1 ℝ) : D 1 ℝ

The bridge reversal as a totalized map on D 1 ℝ.

Equations

• BGW.Skorokhod.reverseBridge f = { toFun := BGW.Skorokhod.reverseBridgeFun f, isCadlag' := ⋯ }

theorem BGW.Skorokhod.reverseBridge_apply (f : D 1 ℝ) (s : ↑(Set.Icc 0 1)) : (reverseBridge f) s = -Function.leftLim ⇑f ⟨1 - ↑s, ⋯⟩

Pointwise formula (definitional).

theorem BGW.Skorokhod.reverseBridge_eq_reverseIncrements {f : D 1 ℝ} (hf : f ⟨1, ⋯⟩ = 0) : reverseBridge f = reverseIncrements ⋯ f

Agreement with the increment reversal on paths ending at 0.

theorem BGW.Skorokhod.measurable_reverseBridge : Measurable reverseBridge

reverseBridge is Borel measurable.

theorem BGW.Skorokhod.leftLim_reverseBridge (f : D 1 ℝ) (hf : f ⟨1, ⋯⟩ = Function.leftLim ⇑f ⟨1, ⋯⟩) (t : ↑(Set.Icc 0 1)) : Function.leftLim (⇑(reverseBridge f)) t = -f ⟨1 - ↑t, ⋯⟩

Left limits transform reversal into evaluation at the reversed time, provided the original path has no terminal jump.