The auxiliary clock germ event #
The extended occupation limsup is monotone on every path. This makes immediate positivity a raw-prefix event at every positive horizon, hence an event of the right-continuous germ. The potential has already been constructed independently of the zero-one argument.
References #
- J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.
theorem
BGW.StableTrees.measurableSet_supAuxGermClock_positive
(θ : ℝ)
:
MeasurableSet {f : Skorokhod.DLoc | ∀ (n : ℕ), 0 < supAuxGermClock θ f (1 / (↑n + 1))}
Immediate positivity of the extended helper is measurable in the germ sigma-algebra.
theorem
BGW.StableTrees.measure_supAuxGermClock_positive_zeroOne
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
:
↑(stableLocalLaw θ) {f : Skorokhod.DLoc | ∀ (n : ℕ), 0 < supAuxGermClock θ f (1 / (↑n + 1))} = 0 ∨ ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | ∀ (n : ℕ), 0 < supAuxGermClock θ f (1 / (↑n + 1))} = 1
Blumenthal's law applies to the extended helper's immediate-positivity event.