Small-time estimates for the first height upcrossing

Forest ladder times have the canonical walk passage law. Passage convergence keeps positive tree levels away from time zero. Combining this with the survival union bound and then choosing a small tree level gives the eventual small-time bound for the first height upcrossing.

theorem BGW.StableTrees.HeightTightness.map_scaled_ladderTime (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (l n : ℕ) : MeasureTheory.Measure.map (fun (ω : ℕ → ℕ) => ↑(DiscreteForest.ladderTime ω l) / ↑n) ↑(DiscreteForest.offspringSeqLaw μ) = walkPassageLaw μ l n

The rescaled ladder time of the offspring forest has the canonical walk passage law.

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

At a positive limiting tree level, the scaled ladder times stay away from zero in probability, eventually in the scaling index.

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

The scaled first height upcrossing has uniformly vanishing mass near time zero, in the eventual form needed for the renewal argument.