Documentation

BGW.StableTrees.HeightTightnessUniformModulus

Uniform modulus control over all height laws #

For each fixed index, continuity gives a small modulus in probability. Combining these bounds over finitely many initial indices with the eventual regeneration estimate gives one scale valid uniformly over every scaling index.

theorem BGW.StableTrees.HeightTightness.exists_pos_uniform_height_modulus_probability_small {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {T : NNReal} (hT : 0 < T) {η ε : ℝ} (hη : 0 < η) (hε : 0 < ε) :
∃ (δ : ℝ), 0 < δ ∧ ∀ (n : ℕ), (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | η < heightOscillation B n (↑T) δ ω} ≤ ε

The asymptotic height modulus extends uniformly to all scaling indices, including the finitely many initial path laws.