Zero occupation of the reflected stable process

At each fixed positive time the reflection is positive almost surely: otherwise the terminal time would minimize the compact path, contrary to the regularity and reversal theorem. Fubini then gives zero Lebesgue occupation of the zero set. This avoids a separate construction of the drift coefficient of the passage subordinator (J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VII).

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

At any fixed positive time the reflected stable process is almost surely positive.

theorem BGW.StableTrees.ae_zeroSet_volume_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), MeasureTheory.volume (NNReal.toReal '' {t : NNReal | ↑(reflectedFrom 0 f) t = 0}) = 0

The zero set of the reflected process is Lebesgue-null (a.s.; measured in ℝ through the coercion, since ℝ≥0 carries no MeasureSpace instance).