Joint approximation limits on age windows

All product measures used here are finite. The excursion product is restricted to survival, and its joint limit is obtained by the Cauchy criterion rather than a measurable choice of limits.

theorem BGW.StableTrees.measurable_heightApprox_age_excursion (ε : ℝ) : Measurable fun (p : ℝ × Excursion) => heightApprox ε p.2.path p.1.toNNReal

Joint age/path measurability of an excursion approximation.

theorem BGW.StableTrees.measurable_heightApprox_age_stable (ε : ℝ) : Measurable fun (p : ℝ × Skorokhod.DLoc) => heightApprox ε p.2 p.1.toNNReal

Joint age/path measurability of a stable-path approximation.

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

Existence of a joint limit on a finite surviving excursion age window.

theorem BGW.StableTrees.exists_heightApprox_tendstoInMeasure_stable_ages {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (S : NNReal) : ∃ (L : ℝ × Skorokhod.DLoc → ℝ), Measurable L ∧ MeasureTheory.TendstoInMeasure ((MeasureTheory.volume.restrict (Set.Ioo 0 ↑S)).prod ↑(stableLocalLaw θ)) (fun (ε : ℝ) (p : ℝ × Skorokhod.DLoc) => heightApprox ε p.2 p.1.toNNReal) (nhdsWithin 0 (Set.Ioi 0)) L

Existence of a joint limit on a bounded stable-path age window.

theorem BGW.StableTrees.exists_heightApprox_tendstoInMeasure_unit_ages {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (L : ℝ × Excursion → ℝ), Measurable L ∧ MeasureTheory.TendstoInMeasure ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod ↑(unitExcursionLaw θ)) (fun (ε : ℝ) (p : ℝ × Excursion) => heightApprox ε p.2.path p.1.toNNReal) (nhdsWithin 0 (Set.Ioi 0)) L

Existence of a joint limit on the unit-law age window (0,1).