Almost sure identification of the universal limsup #
The chosen sequence converges on every required rational slice and almost every age. Each finite limit equals the literal real limsup defining the universal height.
theorem
BGW.StableTrees.ae_heightUniv_eq_height
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
:
∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (q : ℚ), 0 ≤ q → heightUniv θ f (↑q).toNNReal = height θ f (↑q).toNNReal
Under the stable law, heightUniv is H02's height at every rational time, a.s.
theorem
BGW.StableTrees.ae_tendsto_heightUniv_excursion
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
:
∀ᵐ (e : Excursion) ∂excursionMeasure θ, ∀ (q : ℚ),
0 < q →
(↑q).toNNReal < e.lifetime →
Filter.Tendsto (fun (k : ℕ) => heightApprox (heightEps θ k) e.path (↑q).toNNReal) Filter.atTop
(nhds (heightUniv θ e.path (↑q).toNNReal))
Under N, the approximations converge along heightEps θ to heightUniv at every rational
age before the lifetime.
theorem
BGW.StableTrees.ae_tendsto_heightUniv_unit
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
:
∀ᵐ (e : Excursion) ∂↑(unitExcursionLaw θ), ∀ (q : ℚ),
0 < q →
q < 1 →
Filter.Tendsto (fun (k : ℕ) => heightApprox (heightEps θ k) e.path (↑q).toNNReal) Filter.atTop
(nhds (heightUniv θ e.path (↑q).toNNReal))
Under the unit law, the same at every rational age q < 1.
theorem
BGW.StableTrees.ae_age_heightUniv_eq_height
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(S : NNReal)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 ↑S), ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), heightUniv θ f s.toNNReal = height θ f s.toNNReal
At Lebesgue-a.e. age, heightUniv is H02's height under the stable law.
theorem
BGW.StableTrees.ae_age_tendsto_heightUniv_unit
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 1), ∀ᵐ (e : Excursion) ∂↑(unitExcursionLaw θ), Filter.Tendsto (fun (k : ℕ) => heightApprox (heightEps θ k) e.path s.toNNReal) Filter.atTop
(nhds (heightUniv θ e.path s.toNNReal))
At Lebesgue-a.e. age s < 1, the same under the unit law.