Documentation

BGW.StableTrees.StableExcursionSupportPath

Pathwise passage intervals #

Order and window-infimum facts for the passage process. These facts precede the use of uniqueness of the minimum on rational windows in the excursion-support argument (J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VII).

source
def BGW.StableTrees.passageJumpSet (f : Skorokhod.DLoc) :
Set NNReal

The set of positive jump levels of the passage process: {x > 0 | T_{x-} < T_x}.

Equations
Instances For
    source
    theorem BGW.StableTrees.strictMono_passageTime_of_creeping {f : Skorokhod.DLoc} (hT : ∀ (x : NNReal), firstPassageBelow x f = ↑(passageTime x f)) (hcreep : ∀ (x : NNReal), ↑f (passageTime x f) = -↑x) :
    StrictMono fun (x : NNReal) => passageTime x f

    Creeping at every level makes the passage process strictly increasing.

    source
    theorem BGW.StableTrees.passageTime_lt_passageTimeMinus {f : Skorokhod.DLoc} (hT : ∀ (x : NNReal), firstPassageBelow x f = ↑(passageTime x f)) (hm : StrictMono fun (x : NNReal) => passageTime x f) {x y : NNReal} (hxy : x < y) :
    passageTime x f < passageTimeMinus y f

    Strict increase separates the passage time at one level from the left passage time at every larger level.

    source
    theorem BGW.StableTrees.leftLim_at_passageTimeMinus {f : Skorokhod.DLoc} (hT : ∀ (x : NNReal), firstPassageBelow x f = ↑(passageTime x f)) (hcreep : ∀ (x : NNReal), ↑f (passageTime x f) = -↑x) {x : NNReal} (hx : 0 < x) :
    0 < passageTimeMinus x f ∧ Function.leftLim (↑f) (passageTimeMinus x f) = -↑x

    At a positive level the left passage endpoint is positive, and the path approaches the barrier there from the left. No minimum-uniqueness theorem is used.

    source
    theorem BGW.StableTrees.iInf_window_passageTimeMinus {f : Skorokhod.DLoc} (hT : ∀ (x : NNReal), firstPassageBelow x f = ↑(passageTime x f)) (hcreep : ∀ (x : NNReal), ↑f (passageTime x f) = -↑x) {x r q : NNReal} (hx : 0 < x) (hrg : r < passageTimeMinus x f) (hgq : passageTimeMinus x f < q) (hqd : q < passageTime x f) :
    ⨅ (u : ↑(Set.Icc r q)), ↑f ↑u = -↑x

    A window containing a left passage endpoint, and ending before the right endpoint, has infimum equal to the passage barrier.

    source
    theorem BGW.StableTrees.ae_creeping_passageTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) :
    ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (x : NNReal), ↑f (passageTime x f) = -↑x

    Stable paths creep simultaneously at all passage levels, including level zero.