Identification on surviving excursion age windows

The non-junk a.e.-age clause identifies the universal subsequence limit on each finite surviving-age measure. Uniqueness then identifies the full approximation filter there.

theorem BGW.StableTrees.measurable_excursionHeight_real_age (θ : ℝ) : Measurable fun (p : ℝ × Excursion) => (excursionHeight θ p.2) p.1.toNNReal

Joint real-age evaluation of the continuous excursion height is measurable.

theorem BGW.StableTrees.measurable_heightUniv_excursion_real_age (θ : ℝ) : Measurable fun (p : ℝ × Excursion) => heightUniv θ p.2.path p.1.toNNReal

Joint real-age evaluation of the universal excursion height is measurable.

theorem BGW.StableTrees.ae_heightUniv_eq_excursionHeight_ages {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (S : NNReal) : ∀ᵐ (p : ℝ × Excursion) ∂heightExcursionAgeMeasure θ S, heightUniv θ p.2.path p.1.toNNReal = (excursionHeight θ p.2) p.1.toNNReal

The universal height agrees with the continuous version on surviving age windows.

theorem BGW.StableTrees.ae_tendsto_excursionHeight_ages {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (S : NNReal) : ∀ᵐ (p : ℝ × Excursion) ∂heightExcursionAgeMeasure θ S, Filter.Tendsto (fun (k : ℕ) => heightApprox (heightEps θ k) p.2.path p.1.toNNReal) Filter.atTop (nhds ((excursionHeight θ p.2) p.1.toNNReal))

Universal cutoffs converge to the continuous version on surviving age windows.

theorem BGW.StableTrees.heightApprox_tendstoInMeasure_excursionHeight_ages {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (S : NNReal) : MeasureTheory.TendstoInMeasure (heightExcursionAgeMeasure θ S) (fun (ε : ℝ) (p : ℝ × Excursion) => heightApprox ε p.2.path p.1.toNNReal) (nhdsWithin 0 (Set.Ioi 0)) fun (p : ℝ × Excursion) => (excursionHeight θ p.2) p.1.toNNReal

Full-filter identification with the continuous height on each finite surviving-age window.