Discrete height and occupation in two limits

The stopped band estimate, ladder-count tightness and the vanishing ceiling error give the height approximation. Finite-time reversal restores forest heights.

theorem BGW.StableTrees.DiscreteHeightApprox.limsup_add_le_ennreal {α : Type u_1} (f : Filter α) (u v : α → ENNReal) : Filter.limsup (fun (i : α) => u i + v i) f ≤ Filter.limsup u f + Filter.limsup v f

Addition is compatible with upper limits of nonnegative extended-real sequences.

theorem BGW.StableTrees.DiscreteHeightApprox.revSeq_involutive (k : ℕ) : Function.Involutive (revSeq k)

Applying finite-prefix reversal twice restores the sequence.

theorem BGW.StableTrees.DiscreteHeightApprox.measurable_bandCount (k : ℕ) (a : ℝ) : Measurable fun (ω : ℕ → ℕ) => bandCount ω k a

Every fixed finite reflected-band count is measurable.

theorem BGW.StableTrees.DiscreteHeightApprox.occupation_error_twoLimit {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) (t : NNReal) {η : ℝ} (hη : 0 < η) : Filter.Tendsto (fun (ε : ℝ) => Filter.limsup (fun (n : ℕ) => ↑(DiscreteForest.offspringSeqLaw μ) {ω : ℕ → ℕ | η < |scaledHeight B n ω t - discreteOccupation B n ε ω t|}) Filter.atTop) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Two-limit estimate. For a stable domain (μ, θ, B), a fixed t and η > 0: limsup_{ε↓0} limsup_n P(|(B_n/n) H_{⌊nt⌋} - discrete ε-occupation| > η) = 0. No renewal-error hypothesis; ties are weak records; t = 0 is trivial.