General predictable compensation by increasing finite-box exhaustion.

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

theorem BGW.StableTrees.excursion_compensation_predictable_general {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {H : (NNReal × Skorokhod.DLoc) × Excursion → ENNReal} (hH : Measurable H) : ∫⁻ (f : Skorokhod.DLoc), ∫⁻ (p : NNReal × Excursion), H ((p.1, f), p.2) ∂excursionPointMeasure f ∂↑(stableLocalLaw θ) = ∫⁻ (f : Skorokhod.DLoc), ∫⁻ (x : NNReal), ∫⁻ (e : Excursion), H ((x, f), e) ∂excursionMeasure θ ∂lebNN ∂↑(stableLocalLaw θ)

General predictable compensation formula. For every H : (ℝ≥0 × DLoc) × Excursion → ℝ≥0∞ measurable for predictableSigma ⊗ Borel(Excursion), with μ_f = excursionPointMeasure f: E ∫ H((x,f),e) μ_f(dx,de) = E ∫_0^∞ ∫ H((x,f),e) N(de) dx. Proof route: π-λ argument on the generating rectangles (a,b] × F × A using excursion_compensation_step (with Y = 1_F), then monotone class; no pointwise approximation is needed.