Scaling of the continuous excursion height under the excursion measure

The two universal-subsequence limits are identified through the full-filter limit on finite surviving-age windows. Continuity extends equality from almost every age to every age.

theorem BGW.StableTrees.ae_excursionHeight_scale_ages {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (c : ↑(Set.Ioi 0)) (S : NNReal) : ∀ᵐ (p : ℝ × Excursion) ∂heightExcursionAgeMeasure θ S, (excursionHeight θ (excursionScale θ c p.2)) ((↑c).toNNReal * p.1.toNNReal) = ↑c ^ (1 - 1 / θ) * (excursionHeight θ p.2) p.1.toNNReal

Fixed-scale height equality on each finite surviving excursion age window.

theorem BGW.StableTrees.excursionHeight_scale_of_ae (θ : ℝ) (c : ↑(Set.Ioi 0)) (e : Excursion) (he : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), s.toNNReal < e.lifetime → (excursionHeight θ (excursionScale θ c e)) ((↑c).toNNReal * s.toNNReal) = ↑c ^ (1 - 1 / θ) * (excursionHeight θ e) s.toNNReal) (t : NNReal) : (excursionHeight θ (excursionScale θ c e)) ((↑c).toNNReal * t) = ↑c ^ (1 - 1 / θ) * (excursionHeight θ e) t

Almost-everywhere interior scale equality determines the two continuous heights everywhere.

theorem BGW.StableTrees.ae_excursionHeight_scale {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (c : ↑(Set.Ioi 0)) : ∀ᵐ (e : Excursion) ∂excursionMeasure θ, ∀ (t : NNReal), (excursionHeight θ (excursionScale θ c e)) ((↑c).toNNReal * t) = ↑c ^ (1 - 1 / θ) * (excursionHeight θ e) t

Scaling under N, for each fixed c > 0: H(S_c e)(c t) = c^(1-1/θ) H(e)(t) for all t, N-a.e.