Positivity of the clock after supremum contacts

A countable measurable characterization of positive finite clocks transfers through strong Markov restart. Occupation additivity then gives immediate clock growth after every finite strict upward passage at a fixed level.

theorem BGW.StableTrees.ae_supLocalTime_pos_shiftAt {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {τ : Skorokhod.DLoc → ENNReal} (hτ : MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration τ) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), τ f < ⊤ → ∀ (u : NNReal), 0 < u → 0 < supLocalTime θ (Skorokhod.DLoc.shiftAt τ f) u

The fresh supremum clock after a finite stopping time is positive at every positive age.

theorem BGW.StableTrees.supLocalTime_restart_of_contact (θ : ℝ) (f : Skorokhod.DLoc) (hf0 : ↑f 0 = 0) {s : NNReal} (hs : supReflected f s = 0) (hp : ∀ (u : NNReal), Filter.Tendsto (fun (k : ℕ) => supOccupation (supEps θ k) f u) Filter.atTop (nhds (supLocalTime θ f u))) (u : NNReal) : supLocalTime θ f (s + u) = supLocalTime θ f s + supLocalTime θ (Skorokhod.DLoc.shift s f) u

A convergent occupation clock restarts at every supremum contact of its path.

theorem BGW.StableTrees.ae_clock_increases_after_passage {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (q : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), Skorokhod.DLoc.strictPassageAbove (↑q) f < ⊤ → ∀ (u : NNReal), 0 < u → supLocalTime θ f (ENNReal.toNNReal (Skorokhod.DLoc.strictPassageAbove (↑q) f)) < supLocalTime θ f (ENNReal.toNNReal (Skorokhod.DLoc.strictPassageAbove (↑q) f) + u)

The clock increases immediately after every fixed-level strict upward passage.