Occupation restart at a supremum contact

The deterministic reflected restart identifies the occupation increment with the occupation of the centered shifted path, at every contact time.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VI.

theorem BGW.StableTrees.supReflected_shift_of_contact {f : Skorokhod.DLoc} (hf : ↑f 0 = 0) {s : NNReal} (hs : supReflected f s = 0) (t : NNReal) : supReflected f (s + t) = supReflected (Skorokhod.DLoc.shift s f) t

At a contact time, the centered shifted path has the same future reflection.

theorem BGW.StableTrees.supRunning_shift_of_contact {f : Skorokhod.DLoc} (hf : ↑f 0 = 0) {s : NNReal} (hs : supReflected f s = 0) (t : NNReal) : supRunning f (s + t) = supRunning f s + supRunning (Skorokhod.DLoc.shift s f) t

The running supremum adds its contact value to that of the centered future path.

theorem BGW.StableTrees.supOccupation_shift_of_contact {ε : ℝ} (hε : 0 < ε) {f : Skorokhod.DLoc} (hf : ↑f 0 = 0) {s : NNReal} (hs : supReflected f s = 0) (t : NNReal) : supOccupation ε f (s + t) - supOccupation ε f s = supOccupation ε (Skorokhod.DLoc.shift s f) t

Occupation approximations split exactly at every supremum contact time.