Transfer of height approximation limits to the unit excursion law

The unit prefix density transfers existence of an approximation limit. A measurable prefix representative is extracted from convergence in measure before changing the law.

theorem BGW.StableTrees.unitPrefix_absolutelyContinuous_excursion {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) (ht0 : 0 < t) (ht1 : t < 1) : (unitPrefix θ t).AbsolutelyContinuous (MeasureTheory.Measure.map (excursionRestrict t) ((excursionMeasure θ).restrict {e : Excursion | t < e.lifetime}))

Unit prefixes are absolutely continuous with respect to the corresponding surviving excursion prefixes.

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

Existence of an excursion approximation limit implies existence of a unit-law limit. The excursion convergence hypothesis remains an independent obligation.