First long excursion and first long block: definitions

The first jump level of the passage process carrying an excursion of lifetime > 1, its marked excursion, endpoints and stopped cut, the deterministic good-path predicate used for extraction, and their discrete counterparts for scaled skip-free walks (ladder times, first long block, endpoints and cut path).

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

Continuum side

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

The jump levels carrying a LONG excursion (lifetime > 1).

Equations

• BGW.StableTrees.longLabelSet f = {x : NNReal | x ∈ BGW.StableTrees.passageJumpSet f ∧ 1 < BGW.StableTrees.passageTime x f - BGW.StableTrees.passageTimeMinus x f}

noncomputable def BGW.StableTrees.firstLongLabel (f : Skorokhod.DLoc) : NNReal

The first long label L = inf {x ∈ J(f) | T_x - T_{x-} > 1} (junk 0 when empty).

Equations

• BGW.StableTrees.firstLongLabel f = sInf (BGW.StableTrees.longLabelSet f)

noncomputable def BGW.StableTrees.firstLongMark (f : Skorokhod.DLoc) : Excursion

The first long mark: the excursion cut at the first long label.

Equations

• BGW.StableTrees.firstLongMark f = BGW.StableTrees.jumpExcursion (BGW.StableTrees.firstLongLabel f) f

noncomputable def BGW.StableTrees.firstLongEnds (f : Skorokhod.DLoc) : ℝ × ℝ

The selected physical interval (T_{L-}, T_L) as reals.

Equations

• BGW.StableTrees.firstLongEnds f = (↑(BGW.StableTrees.passageTimeMinus (BGW.StableTrees.firstLongLabel f) f), ↑(BGW.StableTrees.passageTime (BGW.StableTrees.firstLongLabel f) f))

noncomputable def BGW.StableTrees.longCutTriple (T : NNReal) (f : Skorokhod.DLoc) : ℝ × ℝ × Skorokhod.D ↑T ℝ

The limit triple (g, d, cut restricted to [0,T]).

Equations

• BGW.StableTrees.longCutTriple T f = ((BGW.StableTrees.firstLongEnds f).1, (BGW.StableTrees.firstLongEnds f).2, BGW.StableTrees.excursionRestrict T (BGW.StableTrees.firstLongMark f))

def BGW.StableTrees.IsRegularExcursionLevel (f : Skorokhod.DLoc) (x : NNReal) : Prop

Regular excursion level: the geometric facts at a jump level x (see the module docstring, item (iii)). R = reflectedFrom 0 f; R (t-) is Function.leftLim.

Equations

• One or more equations did not get rendered due to their size.

structure BGW.StableTrees.GoodLongExtractionPath (M : NNReal) (f : Skorokhod.DLoc) : Prop

Good path for first-long-excursion extraction on the horizon [0, M]. A bundle of geometric facts about f; convergence of the extraction is NOT a field.

• zero : ↑f 0 = 0
• passageZero : passageTime 0 f = 0

  passage at level zero happens at time zero (excludes an initial plateau at the minimum; under the stable law this is (ae_passageTime_eq_firstPassageBelow hθ).2)

• noNegJumps : NoNegJumps f
• infContinuous : Continuous (runningInfLoc f)
• finitePassage (x : NNReal) : firstPassageBelow x f = ↑(passageTime x f)
• creeping (x : NNReal) : ↑f (passageTime x f) = -↑x
• strictMono : StrictMono fun (x : NNReal) => passageTime x f
• regular (x : NNReal) : x ∈ passageJumpSet f → IsRegularExcursionLevel f x
• noLifetimeOne (x : NNReal) : x ∈ passageJumpSet f → passageTime x f - passageTimeMinus x f ≠ 1
• hasLongLabel : ∃ (L : NNReal), IsLeast (longLabelSet f) L
• end_lt : passageTime (firstLongLabel f) f < M

def BGW.StableTrees.GoodLongExtractionCutPath (M T : NNReal) (f : Skorokhod.DLoc) : Prop

Good path plus continuity of the selected cut at the cutoff T.

Equations

• BGW.StableTrees.GoodLongExtractionCutPath M T f = (BGW.StableTrees.GoodLongExtractionPath M f ∧ ContinuousAt (↑(BGW.StableTrees.firstLongMark f).path) T)

Discrete side

def BGW.StableTrees.IsSkipFreeIncrement (a : ℝ) : Prop

A skip-free increment: ξ - 1 with ξ ∈ ℕ.

Equations

• BGW.StableTrees.IsSkipFreeIncrement a = ∃ (k : ℕ), a = ↑k - 1

noncomputable def BGW.StableTrees.ladderTime (ω : ℕ → ℝ) (r : ℕ) : ℕ

Ladder time L_r: the (weak) hit of (-∞, -r], finite reading.

Equations

• BGW.StableTrees.ladderTime ω r = (BGW.StableTrees.walkHitTime r ω).toNat

def BGW.StableTrees.longBlockSet (n : ℕ) (ω : ℕ → ℝ) : Set ℕ

Blocks of size at least n (the block must exist: its end is a finite hit).

Equations

• BGW.StableTrees.longBlockSet n ω = {r : ℕ | BGW.StableTrees.walkHitTime (r + 1) ω ≠ ⊤ ∧ n ≤ BGW.StableTrees.ladderTime ω (r + 1) - BGW.StableTrees.ladderTime ω r}

noncomputable def BGW.StableTrees.firstLongIndex (n : ℕ) (ω : ℕ → ℝ) : ℕ

Index of the first long block (junk 0 when none).

Equations

• BGW.StableTrees.firstLongIndex n ω = sInf (BGW.StableTrees.longBlockSet n ω)

noncomputable def BGW.StableTrees.extractionEndpoints (n : ℕ) (ω : ℕ → ℝ) : ℝ × ℝ

Selected endpoints (L_r / n, L_{r+1} / n) of the first long block.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGW.StableTrees.blockIncrements (ω : ℕ → ℝ) (r i : ℕ) : ℝ

Increments of block r with the final -1 step replaced by 0 (and 0 afterwards).

Equations

• BGW.StableTrees.blockIncrements ω r i = if i + 1 < BGW.StableTrees.ladderTime ω (r + 1) - BGW.StableTrees.ladderTime ω r then ω (BGW.StableTrees.ladderTime ω r + i) else 0

noncomputable def BGW.StableTrees.extractionTriple (b : ℝ) (n : ℕ) (T : NNReal) (ω : ℕ → ℝ) : ℝ × ℝ × Skorokhod.D ↑T ℝ

The extraction triple (g_n, d_n, cut_n) at scale n, norming b, cutoff T.

Equations

• One or more equations did not get rendered due to their size.