Everywhere finite measurable modifications on bounded lifetime-truncated boxes.

See Bertoin, Lévy Processes, Chapter IV.

theorem BGW.StableTrees.exists_finite_modification_excursionPointMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (K ε : NNReal) (hε : 0 < ε) : ∃ (ν : Skorokhod.DLoc → MeasureTheory.Measure (NNReal × Excursion)), Measurable ν ∧ (∀ (f : Skorokhod.DLoc), MeasureTheory.IsFiniteMeasure (ν f)) ∧ ν =ᵐ[↑(stableLocalLaw θ)] fun (f : Skorokhod.DLoc) => (excursionPointMeasure f).restrict (Set.Ioc 0 K ×ˢ {e : Excursion | ε < e.lifetime})

On a bounded time window and a positive lifetime slab, the restricted excursion measure has a measurable modification which is a finite measure at every sample path.