Ordinary primitive formula for discounted occupation

The time kernel is bounded at each positive cutoff. Tonelli's cumulative formula therefore identifies the discounted occupation tail with the discounted primitive, path by path.

References

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

theorem BGW.StableTrees.integrableOn_supAuxKernel_Ioc {ε : ℝ} (hε : 0 < ε) (f : Skorokhod.DLoc) (a b : ℝ) : MeasureTheory.IntegrableOn (fun (t : ℝ) => supOccKernel ε (supReflectedFrom 0 f t.toNNReal)) (Set.Ioc a b) MeasureTheory.volume

The reflected kernel is integrable on every bounded half-open time interval.

theorem BGW.StableTrees.supOccupation_sub_eq_integral {ε : ℝ} (hε : 0 < ε) (f : Skorokhod.DLoc) (hf : ↑f 0 = 0) {s t : NNReal} (hst : s ≤ t) : supOccupation ε f t - supOccupation ε f s = ∫ (u : ℝ) in Set.Ioc ↑s ↑t, supOccKernel ε (supReflectedFrom 0 f u.toNNReal)

An increment of the cumulative occupation is the time kernel integral on that interval.

theorem BGW.StableTrees.supAuxOccupationTail_eq_cumulative {q ε : ℝ} (hq : 0 < q) (hε : 0 < ε) (f : Skorokhod.DLoc) (hf : ↑f 0 = 0) (s : NNReal) : supAuxOccupationTail q ε s f = q * ∫ (t : ℝ) in Set.Ioi ↑s, Real.exp (-q * t) * (supOccupation ε f t.toNNReal - supOccupation ε f s)

Discounted occupation tails are discounted cumulative increments, path by path.