Transferring excursion factorization through the exponential clock

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

theorem BGW.StableTrees.lintegral_supRunning_supReflected_excursion_factors {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) {F G : ℝ → ENNReal} (hF : Measurable F) (hG : Measurable G) : ∫⁻ (p : Skorokhod.DLoc × ℝ), F (supRunning p.1 p.2.toNNReal) * G (supReflected p.1 p.2.toNNReal) ∂expClockLaw θ q = (∫⁻ (f : Skorokhod.DLoc), ∫⁻ (x : NNReal), expNeg (ENNReal.ofReal q * passagePast x f) * G ↑x ∂lebNN ∂↑(stableLocalLaw θ)) * ∫⁻ (e : Excursion), excursionDiscount q F e ∂excursionMeasure θ

The two excursion factors for the supremum and drawdown, before normalization.