Height approximation limits under the excursion and unit laws

Interior increment prefixes have absolutely continuous laws, so compact representatives transfer H02's full-filter convergence to each interior excursion window. This and a uniform first-moment estimate at the excursion start give the full-filter limit. Prefix absolute continuity then transfers its existence to the unit law.

theorem BGW.StableTrees.heightApprox_shift_tendstoInMeasure_excursion {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (s r : NNReal) (hs : 0 < s) : MeasureTheory.TendstoInMeasure ((excursionMeasure θ).restrict {e : Excursion | s + r < e.lifetime}) (fun (ε : ℝ) (e : Excursion) => heightApprox ε (Skorokhod.DLoc.shift s e.path) r) (nhdsWithin 0 (Set.Ioi 0)) fun (e : Excursion) => height θ (Skorokhod.DLoc.shift s e.path) r

Full-filter height approximation on every excursion window starting at a positive age.

theorem BGW.StableTrees.exists_heightApprox_tendstoInMeasure_excursion {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) (ht : 0 < t) : ∃ (L : Excursion → ℝ), Measurable L ∧ MeasureTheory.TendstoInMeasure ((excursionMeasure θ).restrict {e : Excursion | t < e.lifetime}) (fun (ε : ℝ) (e : Excursion) => heightApprox ε e.path t) (nhdsWithin 0 (Set.Ioi 0)) L

Approximation under N on the survival event {t < lifetime}: convergence in N-measure to some measurable limit.

theorem BGW.StableTrees.exists_heightApprox_tendstoInMeasure_unit {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) (ht0 : 0 < t) (ht1 : t < 1) : ∃ (L : Excursion → ℝ), Measurable L ∧ MeasureTheory.TendstoInMeasure (↑(unitExcursionLaw θ)) (fun (ε : ℝ) (e : Excursion) => heightApprox ε e.path t) (nhdsWithin 0 (Set.Ioi 0)) L

Approximation under the unit law at ages t < 1.