Strict hitting times of the totalized clock

An increasing crossing predicate is detected by rational times after the crossing. This retains raw prefix measurability without assuming continuity of the extended clock.

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

noncomputable def BGW.StableTrees.supHitting (θ : ℝ) (z : NNReal) (f : Skorokhod.DLoc) : ENNReal

Strict hitting time a_z = inf{t | p(t) > z} of the ENNReal clock (the stopping-time representative of the inverse; ⊤ if never).

Equations

• BGW.StableTrees.supHitting θ z f = ⨅ (t : NNReal), if ↑z < BGW.StableTrees.supLocalTimeENN θ f t then ↑t else ⊤

noncomputable def BGW.StableTrees.supBlowup (θ : ℝ) (f : Skorokhod.DLoc) : ENNReal

Blow-up time b = inf{t | p(t) = ⊤} (⊤ if never; b = ⊤ almost surely).

Equations

• BGW.StableTrees.supBlowup θ f = ⨅ (t : NNReal), if BGW.StableTrees.supLocalTimeENN θ f t = ⊤ then ↑t else ⊤

theorem BGW.StableTrees.measurable_supHitting_uncurry (θ : ℝ) : Measurable fun (p : NNReal × Skorokhod.DLoc) => supHitting θ p.1 p.2

Joint measurability of the strict hitting representative.

theorem BGW.StableTrees.measurable_supBlowup (θ : ℝ) : Measurable (supBlowup θ)

Measurability of the blow-up time.

theorem BGW.StableTrees.isStoppingTime_supHitting (θ : ℝ) (z : NNReal) : MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration (supHitting θ z)

The strict hitting representative is a stopping time, for every real index.