Normalization of the excursion and its continuous height

The joint shape/lifetime law pulls back a measurable product scaling event. This does not substitute an excursion-dependent scale into a fixed-scale almost-sure assertion.

theorem BGW.StableTrees.ae_excursionHeight_normalize {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (e : Excursion) ∂excursionMeasure θ, ∀ (t : NNReal), (excursionHeight θ e) (e.lifetime * t) = ↑e.lifetime ^ (1 - 1 / θ) * (excursionHeight θ (normalizeExc θ e)) t

Normalization of the pair under N: H(e)(ζ t) = ζ^(1-1/θ) H(normalizeExc θ e)(t).