Finite-box predictable compensation by equality of measures on generating rectangles.

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

theorem BGW.StableTrees.excursion_compensation_predictable_finite {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (K ε : NNReal) (hε : 0 < ε) {H : (NNReal × Skorokhod.DLoc) × Excursion → ENNReal} (hH : Measurable H) : ∫⁻ (f : Skorokhod.DLoc), ∫⁻ (p : NNReal × Excursion) in Set.Ioc 0 K ×ˢ {e : Excursion | ε < e.lifetime}, H ((p.1, f), p.2) ∂excursionPointMeasure f ∂↑(stableLocalLaw θ) = ∫⁻ (q : (NNReal × Skorokhod.DLoc) × Excursion), H q ∂((lebNN.restrict (Set.Ioc 0 K)).prod ↑(stableLocalLaw θ)).prod ((excursionMeasure θ).restrict {e : Excursion | ε < e.lifetime})

Predictable compensation on a bounded time window and a positive lifetime slab.