Weighted occupation resolvent at the supremum

Exponential-clock independence factors the weighted occupation resolvent exactly.

theorem BGW.StableTrees.integral_resolvent_exp_neg_supRunning {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam ε : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) (hε : 0 < ε) : ∫ (f : Skorokhod.DLoc), ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-q * t) * (Real.exp (-lam * supRunning f t.toNNReal) * supOccKernel ε (supReflected f t.toNNReal)) ∂↑(stableLocalLaw θ) = q⁻¹ * (ε⁻¹ * (1 - Real.exp (-(ε * q ^ (1 / θ))))) * ∫ (p : Skorokhod.DLoc × ℝ), Real.exp (-lam * supRunning p.1 p.2.toNNReal) ∂expClockLaw θ q

ε-level exact identity. For q, ε > 0, λ ≥ 0: with g_ε the occupation kernel, E ∫_0^∞ e^{-qt} e^{-λ S_t} g_ε(R_t) dt = q⁻¹ ε⁻¹ (1 - e^{-εΦ}) E e^{-λ S_{e_q}} (E ∫ e^{-qt} G_t dt = q⁻¹ E G(e_q), independence of S_{e_q} and R_{e_q}, R_{e_q} ~ Exp(Φ)).