Constancy of the auxiliary clock off supremum contact

With no negative jumps of the original path, reflection at the supremum is lower semicontinuous. On a compact interval with no contact its minimum is positive, so every sufficiently small occupation cutoff is constant there. The same holds for its limit.

References

• J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

theorem BGW.StableTrees.lowerSemicontinuous_supReflected {f : Skorokhod.DLoc} (hf : ∀ (u : NNReal), Function.leftLim (↑f) u ≤ ↑f u) : LowerSemicontinuous (supReflected f)

Reflection is lower semicontinuous when the original path has no negative jumps.

theorem BGW.StableTrees.supOccupation_eq_of_gap {ε : ℝ} (f : Skorokhod.DLoc) {s t : NNReal} (hst : s ≤ t) (hgap : ∀ u ∈ Set.Icc s t, ε ≤ supReflected f u) : supOccupation ε f t = supOccupation ε f s

An occupation cutoff below every reflected value on an interval has equal endpoint values.