Scale invariance of normalized shapes and excursion tail rectangles

References

• L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997), 377–403.

theorem BGW.StableTrees.normalizeExc_excursionScale (θ : ℝ) (c : ↑(Set.Ioi 0)) (e : Excursion) : normalizeExc θ (excursionScale θ c e) = normalizeExc θ e

Normalization removes every positive space-time scale.

theorem BGW.StableTrees.shape_tail_of_scaling (θ : ℝ) (ν : MeasureTheory.Measure Excursion) (hν : ∀ (c : ↑(Set.Ioi 0)), MeasureTheory.Measure.map (excursionScale θ c) ν = ENNReal.ofReal (↑c ^ (1 / θ)) • ν) {A : Set Excursion} (hA : MeasurableSet A) (t : ℝ) (ht : 0 < t) : ν ({e : Excursion | normalizeExc θ e ∈ A} ∩ {e : Excursion | t < ↑e.lifetime}) = ENNReal.ofReal (t ^ (-(1 / θ))) * ν ({e : Excursion | normalizeExc θ e ∈ A} ∩ {e : Excursion | 1 < ↑e.lifetime})

Scaling alone determines shape-tail rectangle masses from threshold one.

theorem BGW.StableTrees.excursionMeasure_shape_tail_rectangle {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {A : Set Excursion} (hA : MeasurableSet A) (t : ℝ) (ht : 0 < t) : (excursionMeasure θ) ({e : Excursion | normalizeExc θ e ∈ A} ∩ {e : Excursion | t < ↑e.lifetime}) = ENNReal.ofReal (t ^ (-(1 / θ)) / Real.Gamma (1 - 1 / θ)) * ↑(unitExcursionLaw θ) A

Shape rectangles: N(normalizeExc ∈ A, ζ > t) = t^{-α} N(normalizeExc ∈ A, ζ > 1) = (t^{-α}/Γ(1-α)) · unitExcursionLaw(A).