Continuous height versions under the excursion measure

The measurable non-junk event transfers from every jump mark to the excursion measure. The deterministic prefix graph then holds simultaneously at all surviving horizons.

theorem BGW.StableTrees.ae_exists_isExcursionHeightVersion {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (e : Excursion) ∂excursionMeasure θ, ∃ (g : C(NNReal, ℝ)), IsExcursionHeightVersion θ e g

Under the excursion measure every excursion has an a.e.-age height version (the non-junk branch of excursionHeight).

theorem BGW.StableTrees.ae_heightPrefixAE_excursionRestrict {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (e : Excursion) ∂excursionMeasure θ, ∀ a < e.lifetime, ∀ (t : ↑(Set.Icc 0 ↑a)), (heightPrefixAE θ a (excursionRestrict a e)) t = (excursionHeight θ e) ⟨↑t, ⋯⟩

Graph identity under N, simultaneously for all horizons a < ζ: the a.e.-time prefix map applied to the restricted excursion is the excursion height on [0,a].

theorem BGW.StableTrees.ae_restrict_heightPrefixAE_excursionRestrict {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) : ∀ᵐ (e : Excursion) ∂(excursionMeasure θ).restrict {e : Excursion | a < e.lifetime}, ∀ (t : ↑(Set.Icc 0 ↑a)), (heightPrefixAE θ a (excursionRestrict a e)) t = (excursionHeight θ e) ⟨↑t, ⋯⟩

Graph identity under N ↾ {a < ζ} for a fixed horizon a.

theorem BGW.StableTrees.ae_heightPrefixAE_tailExcursionLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (e : Excursion) ∂↑(tailExcursionLaw θ), ∀ a < e.lifetime, ∀ (t : ↑(Set.Icc 0 ↑a)), (heightPrefixAE θ a (excursionRestrict a e)) t = (excursionHeight θ e) ⟨↑t, ⋯⟩

Graph identity under the tail law N(· | ζ > 1), simultaneously for all horizons a < ζ (in particular every a ≤ 1), with the same Borel map heightPrefixAE θ a.