Integrating out an independent exponential clock

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters IV and VI.

theorem BGW.StableTrees.lintegral_expClockLaw (θ : ℝ) {q : ℝ} (hq : 0 < q) {H : Skorokhod.DLoc × ℝ → ENNReal} (hH : Measurable H) : ∫⁻ (p : Skorokhod.DLoc × ℝ), H p ∂expClockLaw θ q = ∫⁻ (t : ℝ) in Set.Ici 0, ENNReal.ofReal (q * Real.exp (-q * t)) * ∫⁻ (f : Skorokhod.DLoc), H (f, t) ∂↑(stableLocalLaw θ)

Integrating over the product clock law is the exponentially weighted resolvent integral.