Constancy of the auxiliary clock off supremum contact #
With no negative jumps of the original path, reflection at the supremum is lower semicontinuous. On a compact interval with no contact its minimum is positive, so every sufficiently small occupation cutoff is constant there. The same holds for its limit.
References #
- J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.
theorem
BGW.StableTrees.supAuxLocalTime_eq_of_gap
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
{f : Skorokhod.DLoc}
(hf : ∀ (u : NNReal), Function.leftLim (↑f) u ≤ ↑f u)
{s t : NNReal}
(hst : s ≤ t)
(hgap : ∀ u ∈ Set.Icc s t, 0 < supReflected f u)
:
On a compact interval without contact the raw auxiliary clock is constant.
theorem
BGW.StableTrees.ae_supAuxLocalTime_const_of_lt
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
:
∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (s t : NNReal),
s < t →
(∀ u ∈ Set.Icc s t, ↑f u < supRunning f u ∧ Function.leftLim (↑f) u < supRunning f u) →
supAuxLocalTime θ f t = supAuxLocalTime θ f s
Increase only on the contact set: constant on any [s,t] strictly below the running
supremum (also in left limits), for all s < t simultaneously.
theorem
BGW.StableTrees.ae_supAuxStieltjes_support
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
:
∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), (supAuxStieltjes θ f).measure {s : ℝ | 0 ≤ s ∧ s.toNNReal ∉ supContact f} = 0
Support in the contact set {R = 0}: dL^aux charges no time outside it.