Compensation for the straddling excursion

Among the passage marks, exactly one lifetime straddles a fixed positive time. The predictable compensation formula therefore computes its joint test-function integral.

References

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

noncomputable def BGW.StableTrees.straddleTest (θ : ℝ) (t : NNReal) (F : (ℝ × ℝ) × Excursion → ENNReal) (g : NNReal) (e : Excursion) : ENNReal

Test functional for a passage start and a mark whose lifetime straddles the fixed time.

Equations

• BGW.StableTrees.straddleTest θ t F g e = if ↑g < ↑t ∧ ↑t < ↑g + ↑e.lifetime then F ((↑g, ↑e.lifetime), BGW.StableTrees.normalizeExc θ e) else 0

theorem BGW.StableTrees.lintegral_straddleData_compensation (θ : ℝ) (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) {F : (ℝ × ℝ) × Excursion → ENNReal} (hF : Measurable F) : ∫⁻ (f : Skorokhod.DLoc), F (straddleData θ t f) ∂↑(stableLocalLaw θ) = ∫⁻ (f : Skorokhod.DLoc), ∫⁻ (x : NNReal), ∫⁻ (e : Excursion), straddleTest θ t F (passageTimeMinus x f) e ∂excursionMeasure θ ∂lebNN ∂↑(stableLocalLaw θ)

Predictable compensation for the unique excursion straddling a positive fixed time.