Cumulative representation of weighted occupation

Tonelli identifies the ordinary weighted occupation integral with the same cumulative weight integral used for the limiting clock.

theorem BGW.StableTrees.lintegral_supOccupation_tail {ε : ℝ} (hε : 0 < ε) (f : Skorokhod.DLoc) (hf : ↑f 0 = 0) (ν : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite ν] : ∫⁻ (t : ℝ) in Set.Ioi 0, ν (Set.Ioi t) ∂(pathStieltjes (supOccupation ε f)).measure = ∫⁻ (t : ℝ) in Set.Ioi 0, ν (Set.Ioi t) * ENNReal.ofReal (supOccKernel ε (supReflectedFrom 0 f t.toNNReal))

The occupation Stieltjes measure integrates a measure tail as the ordinary time kernel.

Reference: Bertoin, Lévy Processes, Chapter VI.

theorem BGW.StableTrees.lintegral_supOccupation_supWeight {q lam ε : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) (hε : 0 < ε) (f : Skorokhod.DLoc) (hf : ↑f 0 = 0) : ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (Real.exp (-q * t - lam * supRunning f t.toNNReal)) ∂(pathStieltjes (supOccupation ε f)).measure = ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (Real.exp (-q * t - lam * supRunning f t.toNNReal) * supOccKernel ε (supReflected f t.toNNReal))

The weighted occupation clock integral is the weighted time integral of its kernel.

Reference: Bertoin, Lévy Processes, Chapter VI.