Excursion small-depth estimate

The forward excursion Markov property bounds the small future-infimum depth at a positive age. The coefficient is the finite excursion survival mass at that age.

theorem BGW.StableTrees.exists_excursion_small_depth_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (s r : NNReal) (ε : ℝ), 0 < s → 0 < r → 0 < ε → ((excursionMeasure θ).restrict {e : Excursion | s + r < e.lifetime}) {e : Excursion | ↑e.path s < futureInf e.path (s + r) s + ε} ≤ (excursionMeasure θ) {e : Excursion | s < e.lifetime} * ENNReal.ofReal (C * ε * ↑r ^ (-1 / θ))

A small future-infimum depth under the excursion measure has a linear cutoff bound.