Excursion soft gaps #
This module collects the strong-Markov property of the reflected stable process, the Itô family indexed by every positive lifetime, and the source-level supremum/infimum descriptions of the endpoints of the excursion straddling a fixed positive time.
C25: the source definitions of the straddling endpoints #
theorem
BGW.StableTrees.ae_straddleStart_eq_sSup
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
{t : NNReal}
(ht : 0 < t)
:
∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), straddleStart t f = sSup {s : NNReal | s ≤ t ∧ ↑f s = runningInfLoc f s}
C25, last zero before t. O01's straddleStart t f is almost surely
sup {s ≤ t | X_s = I_s}.
theorem
BGW.StableTrees.ae_straddleEnd_eq_sInf
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
{t : NNReal}
(ht : 0 < t)
:
∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), straddleEnd t f = sInf {s : NNReal | t < s ∧ ↑f s = runningInfLoc f s}
C25, first zero after t. O01's straddleEnd t f is almost surely
inf {s > t | X_s = I_s}.