Raw scaling under the unit law before continuous reconstruction #
Convergence along the rescaled cutoffs is a prefix event. The excursion prefix density transfers this event at almost every age, without presupposing the unit terminal trace.
theorem
BGW.StableTrees.ae_tendsto_rescaled_heightUniv_ages
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(c : ↑(Set.Ioi 0))
(S : NNReal)
:
∀ᵐ (p : ℝ × Excursion) ∂heightExcursionAgeMeasure θ S, Filter.Tendsto (fun (n : ℕ) => heightApprox (heightEps θ n / ↑c ^ (1 / θ)) p.2.path p.1.toNNReal) Filter.atTop
(nhds (heightUniv θ p.2.path p.1.toNNReal))
Rescaled universal cutoffs converge at almost every surviving excursion age.
theorem
BGW.StableTrees.ae_tendsto_heightUniv_unit_of_prefix
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(t : NNReal)
(ht0 : 0 < t)
(ht1 : t < 1)
(δ : ℕ → ℝ)
(hN :
∀ᵐ (e : Excursion) ∂(excursionMeasure θ).restrict {e : Excursion | t < e.lifetime}, Filter.Tendsto (fun (n : ℕ) => heightApprox (δ n) e.path t) Filter.atTop (nhds (heightUniv θ e.path t)))
:
∀ᵐ (e : Excursion) ∂↑(unitExcursionLaw θ), Filter.Tendsto (fun (n : ℕ) => heightApprox (δ n) e.path t) Filter.atTop (nhds (heightUniv θ e.path t))
A convergent cutoff sequence with its universal-height limit transfers through prefix laws.
theorem
BGW.StableTrees.ae_age_tendsto_rescaled_heightUniv_unit
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(c : ↑(Set.Ioi 0))
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 1), ∀ᵐ (e : Excursion) ∂↑(unitExcursionLaw θ), Filter.Tendsto (fun (n : ℕ) => heightApprox (heightEps θ n / ↑c ^ (1 / θ)) e.path s.toNNReal) Filter.atTop
(nhds (heightUniv θ e.path s.toNNReal))
At almost every unit age the rescaled cutoff sequence has the universal-height limit.