Scaling invariance of the local stable law and its excursion intensity.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters IV and VIII.

theorem BGW.StableTrees.measurable_scaleLoc (θ : ℝ) (c : ↑(Set.Ioi 0)) : Measurable (scaleLoc θ c)

Fixed space-time scaling is measurable on the local path carrier.

theorem BGW.StableTrees.map_scaleLoc_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (c : ↑(Set.Ioi 0)) : MeasureTheory.Measure.map (scaleLoc θ c) ↑(stableLocalLaw θ) = ↑(stableLocalLaw θ)

The stable local path law is invariant under its canonical space-time scaling.

theorem BGW.StableTrees.map_excursionScale_excursionMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (c : ↑(Set.Ioi 0)) : MeasureTheory.Measure.map (excursionScale θ c) (excursionMeasure θ) = ENNReal.ofReal (↑c ^ (1 / θ)) • excursionMeasure θ

Scaling of N (carrier convention S_c: path c^{1/θ} e(t/c), lifetime c ζ): (S_c)_* N = c^{1/θ} • N for every c > 0.