Pathwise strict age-window clocks

Rational windows with a positive lower bound detect compact intervals inside excursions. Their first strict age crossings are stopping times on every path, without modification on a null set.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

theorem BGW.StableTrees.exists_excursionAge_stoppingTimes {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) (ht : 0 < t) : ∃ (τ : ℕ → Skorokhod.DLoc → WithTop NNReal) (ρ : ℕ → Skorokhod.DLoc → WithTop NNReal), (∀ (n : ℕ), MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration (τ n)) ∧ (∀ (n : ℕ), MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration (ρ n)) ∧ ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), (∀ x ∈ passageJumpSet f, t < (jumpExcursion x f).lifetime → ∃! n : ℕ, τ n f = ↑(passageTimeMinus x f + t) ∧ ρ n f = ↑(passageTime x f)) ∧ (∀ (n : ℕ), τ n f < ⊤ → ∃ x ∈ passageJumpSet f, t < (jumpExcursion x f).lifetime ∧ τ n f = ↑(passageTimeMinus x f + t) ∧ ρ n f = ↑(passageTime x f)) ∧ (∀ (n : ℕ), τ n f < ⊤ → τ n f < ρ n f) ∧ ∀ (n : ℕ), ρ n f ≤ τ (n + 1) f

Age-clock supplier (selected age-crossing times τ n and restart times ρ n, stopping times of the right-continuous filtration, exact-once coverage of the excursions surviving to age t; strict crossings exclude lifetime exactly t).