Exponential tail for a fresh infimum depth

The first-passage Laplace transform gives the strict tail. Approaching the barrier from below gives the weak tail, without assumptions about atoms of the infimum law.

theorem BGW.StableTrees.measure_depth_gt_le_exp {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (r : NNReal) {b : NNReal} (hb : 0 < b) {q : ℝ} (hq : 0 ≤ q) : ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | ↑b < -runningInfLoc f r} ≤ ENNReal.ofReal (Real.exp (q * ↑r - ↑b * q ^ (1 / θ)))

The strict infimum-depth tail is controlled by the first-passage Laplace transform.

theorem BGW.StableTrees.measure_depth_ge_le_exp {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (r b : NNReal) {q : ℝ} (hq : 0 ≤ q) : ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | ↑b ≤ -runningInfLoc f r} ≤ ENNReal.ofReal (Real.exp (q * ↑r - ↑b * q ^ (1 / θ)))

The weak infimum-depth tail, including the zero barrier, has the same exponential bound.