Two-sided regularity of zero for the stable process

Right-continuity identifies the positive- and negative-time regularity events with the vanishing of strict passage times. Stable scaling gives a fixed positive lower bound on each approximating passage event; continuity from above and the germ zero-one law then give almost sure regularity. The strong Markov property transfers the result to finite stopping times (J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VII, Corollary 5, for the spectrally positive case).

def BGW.Skorokhod.DLoc.RegularBelowAtZero (f : DLoc) : Prop

0 is regular for (-∞, 0): the path takes negative values in every (0, ε).

Equations

• f.RegularBelowAtZero = ∀ (ε : NNReal), 0 < ε → ∃ (t : NNReal), 0 < t ∧ t < ε ∧ BGW.Skorokhod.DLoc.eval t f < 0

def BGW.Skorokhod.DLoc.RegularAboveAtZero (f : DLoc) : Prop

0 is regular for (0, ∞): the path takes positive values in every (0, ε).

Equations

• f.RegularAboveAtZero = ∀ (ε : NNReal), 0 < ε → ∃ (t : NNReal), 0 < t ∧ t < ε ∧ 0 < BGW.Skorokhod.DLoc.eval t f

theorem BGW.Skorokhod.DLoc.measurableSet_regularBelowAtZero : MeasurableSet {f : DLoc | f.RegularBelowAtZero}

The negative regularity event is measurable.

theorem BGW.Skorokhod.DLoc.measurableSet_regularAboveAtZero : MeasurableSet {f : DLoc | f.RegularAboveAtZero}

The positive regularity event is measurable.

theorem BGW.Skorokhod.DLoc.measurableSet_filtration_zero_regularBelowAtZero : MeasurableSet {f : DLoc | f.RegularBelowAtZero}

The negative regularity event is germ-measurable.

theorem BGW.Skorokhod.DLoc.measurableSet_filtration_zero_regularAboveAtZero : MeasurableSet {f : DLoc | f.RegularAboveAtZero}

The positive regularity event is germ-measurable.

theorem BGW.StableTrees.ae_regular_both_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), f.RegularBelowAtZero ∧ f.RegularAboveAtZero

regularity of 0 for both half-lines. Almost surely, for every ε > 0 the path takes a negative value and a positive value at times in (0, ε).

theorem BGW.StableTrees.ae_regularBelowAtZero_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), f.RegularBelowAtZero

Almost sure regularity of 0 for the negative half-line.

theorem BGW.StableTrees.ae_regularAboveAtZero_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), f.RegularAboveAtZero

Almost sure regularity of 0 for the positive half-line.

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

Regularity after a stopping time, obtained from the strong Markov property.

theorem BGW.StableTrees.ae_strictPassage_zero_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), Skorokhod.DLoc.strictPassageAbove 0 f = 0 ∧ Skorokhod.DLoc.strictPassageBelow 0 f = 0

Almost surely both strict passage times at level zero vanish.