Discounted integrals of continuous clock paths

A Fubini argument relates the actual Stieltjes integral to an integral of clock increments. Integrability of the latter is an explicit hypothesis and yields integrability of the former; no value of a totalized, potentially nonintegrable real integral is used as an estimate.

References

• J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

theorem BGW.StableTrees.pathStieltjes_integral_exp {m : NNReal → ℝ} (hm : Monotone m ∧ Continuous m) {q : ℝ} (hq : 0 < q) (s : NNReal) (hi : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-q * t) * (m t.toNNReal - m s)) (Set.Ioi ↑s) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-q * t)) (Set.Ioi ↑s) (pathStieltjes m).measure ∧ ∫ (t : ℝ) in Set.Ioi ↑s, Real.exp (-q * t) ∂(pathStieltjes m).measure = q * ∫ (t : ℝ) in Set.Ioi ↑s, Real.exp (-q * t) * (m t.toNNReal - m s)

A discounted cumulative-integral bound gives finiteness and the Fubini formula for the actual Stieltjes future integral of a continuous monotone clock.