Exact scaling of excursion height approximations

Positive space-time dilation transports interval infima and multiplies occupation time by the time dilation. No sequence identification or probability law enters this calculation.

theorem BGW.StableTrees.futureInf_scaleLoc (θ : ℝ) (c : ↑(Set.Ioi 0)) (f : Skorokhod.DLoc) {s t : NNReal} (hst : s ≤ t) : futureInf (scaleLoc θ c f) ((↑c).toNNReal * t) ((↑c).toNNReal * s) = ↑c ^ (1 / θ) * futureInf f t s

Positive stable scaling transports a future infimum on the corresponding time window.

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

The height occupation approximation obeys exact space-time scaling at every cutoff.