Passage-time tails from the Laplace transform #
Markov's inequality applied to 1 - exp(-T / y) yields the stable power tail needed for
dyadic left-slope estimates. The passage law is read on its finite nonnegative carrier.
theorem
BGW.StableTrees.measure_passageTime_gt_le
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(x : NNReal)
{y : ℝ}
(hy : 0 < y)
:
↑(stableLocalLaw θ) {f : Skorokhod.DLoc | y < ↑(passageTime x f)} ≤ ENNReal.ofReal (↑x * y ^ (-1 / θ) / (1 - Real.exp (-1)))
A polynomial upper bound for strict passage tails, uniform in the level and threshold.
theorem
BGW.StableTrees.measure_passageIncrement_gt_le
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(a b : NNReal)
{y : ℝ}
(hy : 0 < y)
:
↑(stableLocalLaw θ) {f : Skorokhod.DLoc | y < ↑(passageTime (a + b) f) - ↑(passageTime a f)} ≤ ENNReal.ofReal (↑b * y ^ (-1 / θ) / (1 - Real.exp (-1)))
Stationary passage increments satisfy the same polynomial tail bound.