Small-depth bounds for the excursion approximation

Kendall's identity and the bounded stable density give a linear survival bound uniform in the time and barrier. It bounds a small infimum depth, and the same bound applies to the killed stable kernel, uniformly in its starting level, on survival to the observation time.

theorem BGW.StableTrees.exists_sizeTailKernel_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (r x : ℝ), 0 < r → 0 < x → sizeTailKernel θ r x ≤ C * x * r ^ (-1 / θ)

A uniform linear survival bound, with the stable time exponent.

theorem BGW.StableTrees.exists_measure_runningInf_gt_neg_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (r : NNReal) (x : ℝ), 0 < r → 0 < x → ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | -x < runningInfLoc f r} ≤ ENNReal.ofReal (C * x * ↑r ^ (-1 / θ))

Uniform small-depth estimate for the running infimum.

theorem BGW.StableTrees.exists_killedStableKernel_small_depth_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (r y : NNReal) (ε : ℝ), 0 < r → 0 < ε → ((killedStableKernel θ) y) {g : Skorokhod.DLoc | 0 < ↑g r ∧ ↑g 0 < futureInf g r 0 + ε} ≤ ENNReal.ofReal (C * ε * ↑r ^ (-1 / θ))

The small-depth bound persists under killing, uniformly in the starting height.