Compensation for left-continuous adapted processes, deduced from predictable compensation.

See Bertoin, Lévy Processes, Chapter IV, and Kallenberg, Foundations of Modern Probability, Chapters 12 and 22.

theorem BGW.StableTrees.excursion_compensation_predictable {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (K : NNReal) {H : NNReal → Skorokhod.DLoc → ENNReal} (hadapted : ∀ (x : NNReal), Measurable (H x)) (hleft : ∀ (f : Skorokhod.DLoc) (x : NNReal), 0 < x → ContinuousWithinAt (fun (y : NNReal) => H y f) (Set.Iio x) x) {G : Excursion → ENNReal} (hG : Measurable G) : ∫⁻ (f : Skorokhod.DLoc), ∫⁻ (p : NNReal × Excursion) in Set.Ioc 0 K ×ˢ Set.univ, H p.1 f * G p.2 ∂excursionPointMeasure f ∂↑(stableLocalLaw θ) = (∫⁻ (f : Skorokhod.DLoc), ∫⁻ (x : NNReal) in Set.Ioc 0 K, H x f ∂lebNN ∂↑(stableLocalLaw θ)) * ∫⁻ (e : Excursion), G e ∂excursionMeasure θ

Predictable compensation formula: H x · is F_{T_x}-measurable and x ↦ H x f is left-continuous on (0,∞) (a left-continuous adapted, hence predictable, integrand), G ≥ 0 measurable on excursions, K ≥ 0: E ∑_{x ∈ J, x ≤ K} H(x,f) G(e_x) = E[∫_0^K H(x,f) dx] · ∫ G dN.