Compact sets of anchored paths with prescribed moduli

A common modulus at one positive scale bounds paths anchored at zero. A sequence of vanishing modulus tolerances gives equicontinuity. Arzelà-Ascoli then yields a compact subset of the continuous path space containing every such path.

theorem BGW.StableTrees.HeightTightness.exists_isCompact_of_height_moduli (T : NNReal) (δ : ℕ → ℝ) (hδ : ∀ (j : ℕ), 0 < δ j) : ∃ (K : Set C(↑(Set.Icc 0 ↑T), ℝ)), IsCompact K ∧ ∀ (f : C(↑(Set.Icc 0 ↑T), ℝ)), f ⟨0, ⋯⟩ = 0 → (∀ (j : ℕ) (s t : ↑(Set.Icc 0 ↑T)), |↑s - ↑t| ≤ δ j → |f s - f t| ≤ 1 / (↑j + 1)) → f ∈ K

Anchored paths with a common vanishing modulus envelope lie in one compact set.