Identification of the public local time at the supremum #
Every simultaneous occupation sequence converges locally uniformly to the auxiliary clock. The public clock inherits its Stieltjes support and ladder geometry. Its inverse has an everywhere measurable representative and an almost surely equal stopping-time representative.
References #
- J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters IV and VI.
- T. Duquesne and J.-F. Le Gall, Random Trees, Lévy Processes and Spatial Branching Processes, Astérisque 281 (2002), Section 1.1.
theorem
BGW.StableTrees.ae_supLadder_eq_aux
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
:
∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (z : NNReal), supLadderTime θ z f = supAuxLadderTime θ z f ∧ supLadderHeight θ z f = supAuxLadderHeight θ z f
The public ladder processes equal the auxiliary ones at every level simultaneously.
theorem
BGW.StableTrees.ae_supLadder_spec
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
:
∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), (∀ (z : NNReal), supLocalTimeInverse θ f z = ↑(supLadderTime θ z f)) ∧ supLadderTime θ 0 f = 0 ∧ (Monotone fun (z : NNReal) => supLadderTime θ z f) ∧ (∀ (z : NNReal), ContinuousWithinAt (fun (z : NNReal) => supLadderTime θ z f) (Set.Ici z) z) ∧ (Monotone fun (z : NNReal) => supLadderHeight θ z f) ∧ ∀ (z : NNReal), supLocalTime θ f (supLadderTime θ z f) = ↑z
Simultaneous finiteness, monotonicity, right continuity and inversion of the public ladder.
theorem
BGW.StableTrees.ae_supLadder_geometry
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
:
∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), Filter.Tendsto (fun (z : NNReal) => supLadderTime θ z f) Filter.atTop Filter.atTop ∧ (∀ (z : NNReal), supHitting θ z f = ↑(supLadderTime θ z f)) ∧ (∀ (z : NNReal), supReflected f (supLadderTime θ z f) = 0) ∧ (∀ (z : NNReal), supLadderHeight θ z f = ↑f (supLadderTime θ z f)) ∧ ∀ (z : NNReal), ContinuousWithinAt (fun (z : NNReal) => supLadderHeight θ z f) (Set.Ici z) z
Extra simultaneous geometry: unbounded ladder time, finite stopping representatives, contact at ladder times, evaluation of ladder height, and right continuity of ladder height.