Scaling the marked excursion measure

Time dilation is an order isomorphism, so it commutes with the infima defining passage times and the suprema defining their left endpoints. Excursion cuts scale with these endpoints.

(J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV and Chapter VIII.)

theorem BGW.StableTrees.ae_excursionPointMeasure_scaleLoc {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (c : ↑(Set.Ioi 0)) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), excursionPointMeasure (scaleLoc θ c f) = MeasureTheory.Measure.map (fun (p : NNReal × Excursion) => ((↑c).toNNReal ^ (1 / θ) * p.1, excursionScale θ c p.2)) (excursionPointMeasure f)

Marked scaling (convention scaleLoc θ c f t = c^{1/θ} f (t/c), excursionScale θ c e t = c^{1/θ} e (t/c)): for each c > 0, a.s. the point measure of scaleLoc θ c f is the image of that of f under (x, e) ↦ (c^{1/θ} x, S_c e). (Taking c = 1/c' gives the path c'^{-1/θ} X_{c' ·} and the map (c'^{-1/θ} x, S_{1/c'} e).)