One-sided rise control from discrete regeneration

Integer forest heights increase by at most one in a step. A first crossing therefore reaches its level without overshooting. The shifted-height identity bounds every upward variation within a regenerated gap. A bounded number of crossings and long gaps then give simultaneous one-sided control at all integer times in the horizon, with an exceptional event of arbitrarily small probability on a sufficiently short time scale, uniformly for all large scaling indices.

theorem BGW.StableTrees.HeightTightness.forestHeight_succ_le (ω : ℕ → ℕ) (k : ℕ) : DiscreteForest.forestHeight ω (k + 1) ≤ DiscreteForest.forestHeight ω k + 1

The forest height can increase by at most one in a single discrete step.

theorem BGW.StableTrees.HeightTightness.forestHeight_rise_le_shifted (ω : ℕ → ℕ) {a s t : ℕ} (has : a ≤ s) (hst : s ≤ t) : DiscreteForest.forestHeight ω t ≤ DiscreteForest.forestHeight ω s + DiscreteForest.forestHeight (DiscreteForest.shiftSeq a ω) (t - a)

The shifted height controls every upward variation after the shift time.

theorem BGW.StableTrees.HeightTightness.forestHeight_le_of_le_first_crossing {ω : ℕ → ℕ} {q K k : ℕ} (hK : heightUpcrossingStop q ω = ↑K) (hk : k ≤ K) : DiscreteForest.forestHeight ω k ≤ q

Heights up to and including a first crossing are at most the crossing level.

theorem BGW.StableTrees.HeightTightness.forestHeight_rise_le_in_regeneration_gap {ω : ℕ → ℕ} {q j a b s t : ℕ} (ha : heightRegenerationStop q j ω = ↑a) (hb : heightRegenerationStop q (j + 1) ω = ↑b) (has : a ≤ s) (hst : s ≤ t) (htb : t ≤ b) : DiscreteForest.forestHeight ω t ≤ DiscreteForest.forestHeight ω s + q

Within one regenerated gap, every upward variation is at most its crossing level.

theorem BGW.StableTrees.HeightTightness.forestHeight_short_rise_le_of_gap_bounds {ω : ℕ → ℕ} {q L M d : ℕ} (hfin : heightRegenerationStop q L ω ≠ ⊤) (hL : M < (heightRegenerationStop q L ω).toNat) (hgaps : ∀ j < L, d < heightRegenerationGap q j ω) {s t : ℕ} (hst : s ≤ t) (ht : t ≤ M) (hd : t - s ≤ d) : DiscreteForest.forestHeight ω t ≤ DiscreteForest.forestHeight ω s + 2 * q

Long gaps up to a finite crossing beyond the horizon control all short rises of the height.

theorem BGW.StableTrees.HeightTightness.exists_pos_eventually_short_rise_probability_small {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {η T ε : ℝ} (hη : 0 < η) (hT : 0 ≤ T) (hε : 0 < ε) : ∃ (x : ℝ), 0 < x ∧ ∀ᶠ (n : ℕ) in Filter.atTop, (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | ∃ (s : ℕ) (t : ℕ), s ≤ t ∧ t ≤ ⌊↑n * T⌋₊ ∧ t - s ≤ ⌊↑n * x⌋₊ ∧ DiscreteForest.forestHeight ω s + 2 * ⌊η * ↑n / B n⌋₊ < DiscreteForest.forestHeight ω t} ≤ ε

Uniform eventual control of all short upward variations on an integer horizon.