Integration by parts for the discounted auxiliary clock

References

• J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

theorem BGW.StableTrees.ae_supAuxDiscountedHead_add_tail {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), supAuxDiscountedHead θ q t f + supAuxDiscountedTail θ q t f = supAuxDiscountedTail θ q 0 f

On one full-measure event the head and future tail split the entire discounted clock.

theorem BGW.StableTrees.ae_supAuxDiscountedHead_eq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), supAuxDiscountedHead θ q t f = ∫ (s : ℝ) in Set.Ioc 0 ↑t, Real.exp (-q * s) ∂(supAuxStieltjes θ f).measure

Almost surely the integration-by-parts head equals the Stieltjes head at all times.