Compensation for tests measurable in the stopped past at a deterministic local-time level.

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

theorem BGW.StableTrees.lintegral_excursionPointMeasure_window {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {a b : NNReal} (hab : a ≤ b) {A : Set Excursion} (hA : MeasurableSet A) : ∫⁻ (f : Skorokhod.DLoc), (excursionPointMeasure f) (Set.Ioc a b ×ˢ A) ∂↑(stableLocalLaw θ) = ↑(b - a) * (excursionMeasure θ) A

The mean window formula also holds for the original point measure.

theorem BGW.StableTrees.indepFun_stopped_future_excursionPointMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) {Y : Skorokhod.DLoc → ENNReal} (hY : Measurable Y) : ProbabilityTheory.IndepFun Y (fun (f : Skorokhod.DLoc) => excursionPointMeasure (Skorokhod.DLoc.shiftAt (firstPassageBelow a) f)) ↑(stableLocalLaw θ)

The future marked process is independent of every test measurable in the stopped past.

theorem BGW.StableTrees.excursion_compensation_step {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {a b : NNReal} (hab : a ≤ b) {A : Set Excursion} (hA : MeasurableSet A) {Y : Skorokhod.DLoc → ENNReal} (hY : Measurable Y) : ∫⁻ (f : Skorokhod.DLoc), Y f * (excursionPointMeasure f) (Set.Ioc a b ×ˢ A) ∂↑(stableLocalLaw θ) = (∫⁻ (f : Skorokhod.DLoc), Y f ∂↑(stableLocalLaw θ)) * (↑(b - a) * (excursionMeasure θ) A)

Step compensation relative to F_{T_a}: for Y measurable in the stopped σ-algebra of T_a (not merely the natural history of the point measure), a ≤ b, measurable A: E[Y · μ((a,b] × A)] = E[Y] (b - a) N(A).