Independence of the supremum and drawdown at an exponential time

For the spectrally positive θ-stable process (1 < θ ≤ 2) and an independent exponential clock e_q (expClockLaw θ q), the supremum S_{e_q} and the drawdown S_{e_q} - X_{e_q} are independent (indepFun_supRunning_supReflected_expTime), with product and resolvent forms (lintegral_mul_supRunning_supReflected_expTime, lintegral_resolvent_mul_supRunning_supReflected). The proof splits the clock at the excursion of X - I that straddles it (compensation formula for the excursion point measure) and transfers the resulting factorization of (-I_{e_q}, X_{e_q} - I_{e_q}) by time reversal.

References

• J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters IV and VI.
• A. E. Kyprianou, Fluctuations of Lévy Processes with Applications, 2nd ed., Springer, 2014, Chapter 6 (Wiener–Hopf factorization).

theorem BGW.StableTrees.indepFun_supRunning_supReflected_expTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) : ProbabilityTheory.IndepFun (fun (p : Skorokhod.DLoc × ℝ) => supRunning p.1 p.2.toNNReal) (fun (p : Skorokhod.DLoc × ℝ) => supReflected p.1 p.2.toNNReal) (expClockLaw θ q)

Independence of the supremum and the drawdown at an independent exponential time. S_{e_q} and S_{e_q} - X_{e_q} are independent under P ⊗ Exp(q), for every q > 0.

theorem BGW.StableTrees.lintegral_mul_supRunning_supReflected_expTime {θ : ℝ} (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 = (∫⁻ (p : Skorokhod.DLoc × ℝ), F (supRunning p.1 p.2.toNNReal) ∂expClockLaw θ q) * ∫⁻ (p : Skorokhod.DLoc × ℝ), G (supReflected p.1 p.2.toNNReal) ∂expClockLaw θ q

Product form in ℝ≥0∞ (no integrability needed): for Borel F G : ℝ → ℝ≥0∞, E[F(S_{e_q}) G(R_{e_q})] = E[F(S_{e_q})] · E[G(R_{e_q})].

theorem BGW.StableTrees.lintegral_resolvent_mul_supRunning_supReflected {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) {F G : ℝ → ENNReal} (hF : Measurable F) (hG : Measurable G) : ∫⁻ (t : ℝ) in Set.Ici 0, ENNReal.ofReal (q * Real.exp (-q * t)) * ∫⁻ (f : Skorokhod.DLoc), F (supRunning f t.toNNReal) * G (supReflected f t.toNNReal) ∂↑(stableLocalLaw θ) = (∫⁻ (t : ℝ) in Set.Ici 0, ENNReal.ofReal (q * Real.exp (-q * t)) * ∫⁻ (f : Skorokhod.DLoc), F (supRunning f t.toNNReal) ∂↑(stableLocalLaw θ)) * ∫⁻ (t : ℝ) in Set.Ici 0, ENNReal.ofReal (q * Real.exp (-q * t)) * ∫⁻ (f : Skorokhod.DLoc), G (supReflected f t.toNNReal) ∂↑(stableLocalLaw θ)

Resolvent form (same statement without the clock space): with q e^{-qt} dt weights on [0, ∞), ∫ q e^{-qt} E[F(S_t) G(R_t)] dt factors. Derived from the product form by Tonelli.