Height modulus and vanishing adjacent jumps

The regenerated count and short-gap bounds control every short upward variation. K09 on a deterministic grid and H03 continuity control the grid endpoint values. An enclosing-grid argument bounds the full interpolated modulus. Monotonicity in the time scale gives the two-limit statement. Adjacent jumps use the modulus on the longer horizon T + 1.

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

The forest-height modulus is eventually small on a sufficiently fine fixed time scale.

theorem BGW.StableTrees.HeightTightness.forestHeight_modulus {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {T η : ℝ} (hT : 0 < T) (hη : 0 < η) : Filter.Tendsto (fun (δ : ℝ) => Filter.limsup (fun (n : ℕ) => (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | η < heightOscillation B n T δ ω}) Filter.atTop) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Height modulus (DLG Theorem 2.3.1 route).

theorem BGW.StableTrees.HeightTightness.maxHeightJump_tendstoInMeasure {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {T : ℝ} (hT : 0 < T) : MeasureTheory.TendstoInMeasure (↑(DiscreteForest.offspringSeqLaw μ)) (fun (n : ℕ) (ω : ℕ → ℕ) => maxHeightJump B n T ω) Filter.atTop fun (x : ℕ → ℕ) => 0

The largest adjacent height jump vanishes in probability on the height scale.