Support of the Stieltjes measure of local time

The negative running infimum is constant on intervals where the path and its left limits stay strictly above that infimum. This is the deterministic input for the concentration of its Stieltjes measure on the zero set of the reflected path (J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV).

theorem BGW.StableTrees.ae_runningInf_const_off_zeroSet {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (s t : NNReal), s ≤ t → (∀ (u : NNReal), s ≤ u → u ≤ t → runningInfLoc f u < ↑f u ∧ runningInfLoc f u < Function.leftLim (↑f) u) → runningInfLoc f t = runningInfLoc f s

Stieltjes measure of L = -I is carried by {X = I}: a.s., on any interval [s, t] on which both the path and its left limit stay strictly above the running infimum, L is constant.

theorem BGW.StableTrees.ae_localTimeStieltjes_measure_ne_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), (localTimeStieltjes f).measure {s : ℝ | ↑f s.toNNReal ≠ runningInfLoc f s.toNNReal} = 0

Stieltjes measure of L is carried by {X = I}: almost surely dL {t | X_t ≠ I_t} = 0 ({X > I} is the union of an open set on which L is constant and the countable set of jump times; L is continuous so has no atoms). Negative s are harmless: X_0 = I_0 = 0.