Simultaneous auxiliary ladder geometry #
A continuous clock is encoded as a negative continuous path, allowing reuse of the generic strict-passage geometry from the infimum development. The proof uses no identification of the public local time.
References #
- J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.
theorem
BGW.StableTrees.ae_supAuxLadder_spec
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
:
∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), (∀ (z : NNReal), supAuxInverse θ f z = ↑(supAuxLadderTime θ z f)) ∧ supAuxLadderTime θ 0 f = 0 ∧ (Monotone fun (z : NNReal) => supAuxLadderTime θ z f) ∧ (∀ (z : NNReal), ContinuousWithinAt (fun (z : NNReal) => supAuxLadderTime θ z f) (Set.Ici z) z) ∧ Filter.Tendsto (fun (z : NNReal) => supAuxLadderTime θ z f) Filter.atTop Filter.atTop ∧ (Monotone fun (z : NNReal) => supAuxLadderHeight θ z f) ∧ (∀ (z : NNReal), supAuxLocalTime θ f (supAuxLadderTime θ z f) = ↑z) ∧ (∀ (z : NNReal), supAuxLadderTime θ z f ∈ supContact f) ∧ ∀ (z : NNReal), supAuxLadderHeight θ z f = ↑f (supAuxLadderTime θ z f)
Inverse geometry, simultaneously for all levels z: A^* is finite and agrees with
supAuxInverse, A^*_0 = 0, monotone, right continuous, unbounded; B^* monotone;
L^aux(A^*_z) = z; and R_{A^*_z} = 0 (A^*_z ∈ {S = X}, so B^*_z = X_{A^*_z}).