Increment tails without height continuity #
The ladder-time transform bounds a fresh height. The erasure decomposition bounds the negative increment separately, yielding a uniform exponential bound on the absolute increment.
theorem
BGW.StableTrees.measure_supLocalTime_gt_le_exp
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(s v : NNReal)
{q : ℝ}
(hq : 0 ≤ q)
:
↑(stableLocalLaw θ) {f : Skorokhod.DLoc | ↑v < supLocalTime θ f s} ≤ ENNReal.ofReal (Real.exp (q * ↑s - ↑v * q ^ (1 - 1 / θ)))
The ladder-time transform bounds the tail of the supremum clock.
theorem
BGW.StableTrees.map_height_eq_map_supLocalTime
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
{s : NNReal}
(hs : 0 < s)
:
MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => height θ f s) ↑(stableLocalLaw θ) = MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => supLocalTime θ f s) ↑(stableLocalLaw θ)
Fixed-time reversal gives the same height and supremum-clock laws.