Continuous unit excursion height, including the terminal trace

The shape/lifetime product supplies one deterministic scale whose unit shapes have continuous height versions. Raw scaling pulls that version back, including its zero at the lifetime.

theorem BGW.StableTrees.exists_isExcursionHeightVersion_of_scale (θ : ℝ) (c : ↑(Set.Ioi 0)) (e : Excursion) (hs : ∃ (g : C(NNReal, ℝ)), IsExcursionHeightVersion θ (excursionScale θ c e) g) (hr : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 ↑e.lifetime), heightUniv θ (excursionScale θ c e).path ((↑c).toNNReal * s.toNNReal) = ↑c ^ (1 - 1 / θ) * heightUniv θ e.path s.toNNReal) : ∃ (g : C(NNReal, ℝ)), IsExcursionHeightVersion θ e g

A version at a fixed scale pulls back whenever the raw heights obey the a.e.-age identity.

theorem BGW.StableTrees.lifetimeLaw_ne_zero_of_height_index {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : lifetimeLaw θ ≠ 0

The positive lifetime mixing measure is nonzero for a valid stable index.

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

Under the unit excursion law (singular w.r.t. N) every excursion has an a.e.-age height version, including the vanishing at the lifetime 1.

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

Graph identity under the unit law, simultaneously for all horizons a < ζ (ζ = 1 a.s.), with the same Borel map heightPrefixAE θ a.