Uniform short-gap estimates

Each regenerated gap has the first-upcrossing cutoff probability. A finite union bound and the small-time first-hit estimate control all of the first L gaps.

theorem BGW.StableTrees.HeightTightness.heightUpcrossingStop_le_natCast_iff (q m : ℕ) (ω : ℕ → ℕ) : heightUpcrossingStop q ω ≤ ↑m ↔ ∃ k ≤ m, q ≤ DiscreteForest.forestHeight ω k

A first crossing occurs by m exactly when that height is reached by m.

theorem BGW.StableTrees.HeightTightness.heightRegenerationGap_probability (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (q i m : ℕ) : (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | heightRegenerationGap q i ω ≤ m} = (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | ∃ k ≤ m, q ≤ DiscreteForest.forestHeight ω k}

Every regenerated gap has the first-height-hit probability at a finite cutoff.

theorem BGW.StableTrees.HeightTightness.heightRegenerationGap_union_probability_le (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (q L m : ℕ) : (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | ∃ i < L, heightRegenerationGap q i ω ≤ m} ≤ ↑L * (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | ∃ k ≤ m, q ≤ DiscreteForest.forestHeight ω k}

A finite union bound for short gaps among the first L regenerated crossings.

theorem BGW.StableTrees.HeightTightness.exists_pos_eventually_short_gap_probability_small {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {η ε : ℝ} (hη : 0 < η) (hε : 0 < ε) (L : ℕ) : ∃ (x : ℝ), 0 < x ∧ ∀ᶠ (n : ℕ) in Filter.atTop, (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | ∃ i < L, heightRegenerationGap ⌊η * ↑n / B n⌋₊ i ω ≤ ⌊↑n * x⌋₊} ≤ ε

Uniform eventual small-time control for all of the first finitely many gaps.