Scaling of the auxiliary clock

Deterministic scaling of the occupations and convergence in mean identify the clock under stable path dilation. The selected cutoff sequence need not be preserved by dilation.

References

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

theorem BGW.StableTrees.supRunning_scaleLoc (θ : ℝ) (c : ↑(Set.Ioi 0)) (f : Skorokhod.DLoc) (t : NNReal) : supRunning (scaleLoc θ c f) t = ↑c ^ (1 / θ) * supRunning f (t / (↑c).toNNReal)

The running supremum commutes with positive stable path dilation.

theorem BGW.StableTrees.supReflected_scaleLoc (θ : ℝ) (c : ↑(Set.Ioi 0)) (f : Skorokhod.DLoc) (t : NNReal) : supReflected (scaleLoc θ c f) t = ↑c ^ (1 / θ) * supReflected f (t / (↑c).toNNReal)

Reflection at the supremum commutes with stable path dilation.

theorem BGW.StableTrees.supOccupation_scaleLoc (θ ε : ℝ) (c : ↑(Set.Ioi 0)) (f : Skorokhod.DLoc) (t : NNReal) : supOccupation ε (scaleLoc θ c f) t = ↑c / ↑c ^ (1 / θ) * supOccupation (ε / ↑c ^ (1 / θ)) f (t / (↑c).toNNReal)

Scaling changes the occupation cutoff and contributes the local-time homogeneity factor.