Documentation

BGW.StableTrees.StableFirstPassagePath

Pathwise first-passage facts for local càdlàg paths #

This module contains the deterministic crossing estimates for the strict passage below a level, the running infimum API, and joint measurability of the level/path passage times.

source
theorem BGW.StableTrees.le_eval_of_lt_strictPassageBelow {f : Skorokhod.DLoc} {a : ℝ} {s : NNReal} (hs : ↑s < Skorokhod.DLoc.strictPassageBelow a f) :
a ≤ ↑f s

Before the strict first passage, the path is not below the barrier.

source
theorem BGW.StableTrees.strictPassageBelow_pos_of_lt_eval_zero {f : Skorokhod.DLoc} {a : ℝ} (h0 : a < ↑f 0) :
0 < Skorokhod.DLoc.strictPassageBelow a f

Passage below a level strictly below the initial value is positive.

source
theorem BGW.StableTrees.eval_eq_of_strictPassageBelow_eq_coe {f : Skorokhod.DLoc} {a : ℝ} {t : NNReal} (hf : ∀ (s : NNReal), Function.leftLim (↑f) s ≤ ↑f s) (hT : Skorokhod.DLoc.strictPassageBelow a f = ↑t) (h0 : a < ↑f 0) :
↑f t = a

At a finite strict passage time, the no-negative-jumps property forces creeping.

source
noncomputable def BGW.StableTrees.runningInfLoc (f : Skorokhod.DLoc) (t : NNReal) :
ℝ

The running infimum I_t = inf_{u ≤ t} X_u of a local path.

Equations
Instances For
    source
    theorem BGW.StableTrees.runningInfLoc_antitone (f : Skorokhod.DLoc) :
    Antitone (runningInfLoc f)

    The running infimum is antitone.

    source
    theorem BGW.StableTrees.runningInfLoc_continuous {f : Skorokhod.DLoc} (hf : ∀ (t : NNReal), Function.leftLim (↑f) t ≤ ↑f t) :
    Continuous (runningInfLoc f)

    A path with no negative jumps has a continuous running infimum.

    source
    theorem BGW.StableTrees.runningInfLoc_tendsto_atBot {f : Skorokhod.DLoc} (hcreep : ∀ (x : ℝ), 0 < x → ∃ (t : NNReal), Skorokhod.DLoc.strictPassageBelow (-x) f = ↑t ∧ ↑f t = -x) :
    Filter.Tendsto (runningInfLoc f) Filter.atTop Filter.atBot

    Finite creeping at every positive level makes the running infimum tend to -∞.

    source
    noncomputable def BGW.StableTrees.firstPassageBelow (x : NNReal) (f : Skorokhod.DLoc) :
    WithTop NNReal

    The first passage time below -x, as a process indexed by the level x ≥ 0.

    Equations
    Instances For
      source
      theorem BGW.StableTrees.isStoppingTime_firstPassageBelow (x : NNReal) :
      MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration (firstPassageBelow x)

      Each first passage time is a stopping time of the right-continuous filtration.

      source
      theorem BGW.StableTrees.strictPassageBelow_ne_top_of_le_neg {f : Skorokhod.DLoc} {x y : ℝ} (hxy : x ≤ y) (hfin : Skorokhod.DLoc.strictPassageBelow (-y) f ≠ ⊤) :
      Skorokhod.DLoc.strictPassageBelow (-x) f ≠ ⊤

      Finiteness at a larger level implies finiteness at a smaller level.

      source
      theorem BGW.StableTrees.measurable_firstPassageBelow_uncurry :
      Measurable fun (p : NNReal × Skorokhod.DLoc) => firstPassageBelow p.1 p.2

      Joint measurability of the first passage times in the level and the path.