Exponential-clock representation of reflected resolvents

Bounded Borel functions can be evaluated at the independent clock before computing their reflected resolvent.

Reference: A. E. Kyprianou, Fluctuations of Lévy Processes with Applications, 2nd ed., Springer, 2014, Chapter 8.

theorem BGW.StableTrees.integral_expMeasure_eq {q : ℝ} (hq : 0 < q) (F : ℝ → ℝ) : ∫ (t : ℝ), F t ∂ProbabilityTheory.expMeasure q = q * ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-q * t) * F t

Integration against an exponential law is its positive-half-line density integral.

theorem BGW.StableTrees.integral_expClockLaw_eq {θ q : ℝ} (hq : 0 < q) {H : Skorokhod.DLoc × ℝ → ℝ} (hH : Measurable H) (hb : ∃ (C : ℝ), ∀ (p : Skorokhod.DLoc × ℝ), |H p| ≤ C) : ∫ (p : Skorokhod.DLoc × ℝ), H p ∂expClockLaw θ q = q * ∫ (f : Skorokhod.DLoc), ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-q * t) * H (f, t) ∂↑(stableLocalLaw θ)

A bounded measurable function of the path and clock has the discounted-time expectation.

theorem BGW.StableTrees.reflectedResolvent_eq_expClockLaw {θ q : ℝ} (hq : 0 < q) {k : ℝ → ℝ} (hk : Measurable k) (hb : ∃ (C : ℝ), ∀ (r : ℝ), |k r| ≤ C) (y : ℝ) : reflectedResolvent θ q k y = q⁻¹ * ∫ (p : Skorokhod.DLoc × ℝ), k (supReflectedFrom y.toNNReal p.1 p.2.toNNReal) ∂expClockLaw θ q

Positive-rate reflected resolvents are expectations at the independent exponential clock.