Immediate positivity of the auxiliary clock

Scaling makes positivity probabilities independent of positive time. Continuity from above identifies their common value with the germ event. The mean potential rules out value zero, and Blumenthal's law then gives immediate positivity on one event.

References

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

theorem BGW.StableTrees.measurable_supAuxLocalTime_eval (θ : ℝ) (t : NNReal) : Measurable fun (f : Skorokhod.DLoc) => supAuxLocalTime θ f t

The clock is measurable at each deterministic time, including exceptional paths.

theorem BGW.StableTrees.measure_supAuxLocalTime_pos_eq_one_time {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | 0 < supAuxLocalTime θ f t} = ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | 0 < supAuxLocalTime θ f 1}

The probability of positive clock value is independent of positive time.

theorem BGW.StableTrees.measure_supAuxLocalTime_one_pos_ne_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | 0 < supAuxLocalTime θ f 1} ≠ 0

The unit-time clock is positive with nonzero probability, by the mean potential.

theorem BGW.StableTrees.measure_supAuxGermClock_positive_eq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | ∀ (n : ℕ), 0 < supAuxGermClock θ f (1 / (↑n + 1))} = ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | 0 < supAuxLocalTime θ f 1}

The extended-helper germ event has the same mass as unit-time clock positivity.

theorem BGW.StableTrees.ae_supAuxLocalTime_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), 0 < t → 0 < supAuxLocalTime θ f t

Immediate increase: L^aux_t > 0 for every t > 0, almost surely.