Discounted occupation split at the excursion containing the clock

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters IV and VI.

noncomputable def BGW.StableTrees.excursionDiscount (q : ℝ) (G : ℝ → ENNReal) (e : Excursion) : ENNReal

The discounted occupation integral of an infimum excursion, as a function of its mark.

Equations

• BGW.StableTrees.excursionDiscount q G e = ∫⁻ (s : ℝ) in Set.Ioo 0 ↑e.lifetime, ENNReal.ofReal (q * Real.exp (-q * s)) * G (↑e.path s.toNNReal)

theorem BGW.StableTrees.ae_lintegral_split_excursionDiscount {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (q : ℝ) (F : ℝ → ENNReal) {G : ℝ → ENNReal} (hG : Measurable G) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∫⁻ (t : ℝ) in Set.Ici 0, ENNReal.ofReal (q * Real.exp (-q * t)) * F (localTime f t.toNNReal) * G (↑(reflectedFrom 0 f) t.toNNReal) = ∫⁻ (p : NNReal × Excursion), ENNReal.ofReal (Real.exp (-q * ↑(passageTimeMinus p.1 f))) * F ↑p.1 * excursionDiscount q G p.2 ∂excursionPointMeasure f

The clock density splits at the start of the excursion straddling it.