Deterministic path facts for passage times

This module develops the order and crossing properties of strict downward passage times and of the running infimum for an arbitrary local càdlàg path (J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VII).

theorem BGW.StableTrees.firstPassageBelow_mono (f : Skorokhod.DLoc) : Monotone fun (x : NNReal) => firstPassageBelow x f

Strict downward passage is monotone in its level.

theorem BGW.StableTrees.firstPassageBelow_le_of_eval_lt {f : Skorokhod.DLoc} {x t : NNReal} (h : ↑f t < -↑x) : firstPassageBelow x f ≤ ↑t

A strict crossing gives an upper bound for the corresponding passage time.

theorem BGW.StableTrees.exists_eval_lt_of_firstPassageBelow_lt {f : Skorokhod.DLoc} {x t : NNReal} (h : firstPassageBelow x f < ↑t) : ∃ u < t, ↑f u < -↑x

If a passage time is strictly below a finite time, a crossing occurs earlier.

theorem BGW.StableTrees.bddBelow_runningInf_range (f : Skorokhod.DLoc) (t : NNReal) : BddBelow (Set.range fun (u : ↑(Set.Iic t)) => ↑f ↑u)

The running infimum is bounded below on every bounded time interval.

theorem BGW.StableTrees.runningInfLoc_le_eval (f : Skorokhod.DLoc) (t : NNReal) (u : ↑(Set.Iic t)) : runningInfLoc f t ≤ ↑f ↑u

The running infimum is smaller than every value on its defining interval.

theorem BGW.StableTrees.le_runningInfLoc (f : Skorokhod.DLoc) (t : NNReal) {a : ℝ} (h : ∀ (u : ↑(Set.Iic t)), a ≤ ↑f ↑u) : a ≤ runningInfLoc f t

A lower bound of all values on an interval bounds its running infimum.

theorem BGW.StableTrees.exists_eval_lt_of_runningInfLoc_lt {f : Skorokhod.DLoc} {t : NNReal} {a : ℝ} (h : runningInfLoc f t < a) : ∃ u ≤ t, ↑f u < a

A value strictly below the running infimum produces a crossing time in the interval.

theorem BGW.StableTrees.eval_le_of_firstPassageBelow_eq_coe {f : Skorokhod.DLoc} {x t : NNReal} (hT : firstPassageBelow x f = ↑t) : ↑f t ≤ -↑x

At a finite strict passage time, the path is on or below its barrier.

theorem BGW.StableTrees.runningInfLoc_le_of_firstPassageBelow_le (f : Skorokhod.DLoc) {x t : NNReal} (h : firstPassageBelow x f ≤ ↑t) : runningInfLoc f t ≤ -↑x

A finite passage time up to t forces the running infimum at t below its level.

theorem BGW.StableTrees.firstPassageBelow_eq_coe_untopD (f : Skorokhod.DLoc) (hfin : ∀ (x : NNReal), firstPassageBelow x f < ⊤) (x : NNReal) : firstPassageBelow x f = ↑(WithTop.untopD 0 (firstPassageBelow x f))

The finite reading of a finite strict passage time coerces back to that time.

theorem BGW.StableTrees.untopD_firstPassageBelow_mono (f : Skorokhod.DLoc) (hfin : ∀ (x : NNReal), firstPassageBelow x f < ⊤) : Monotone fun (x : NNReal) => WithTop.untopD 0 (firstPassageBelow x f)

The finite readings of finite strict passage times are nondecreasing.

theorem BGW.StableTrees.tendsto_untopD_firstPassageBelow_nhdsGT (f : Skorokhod.DLoc) (hfin : ∀ (x : NNReal), firstPassageBelow x f < ⊤) (x : NNReal) : Filter.Tendsto (fun (y : NNReal) => WithTop.untopD 0 (firstPassageBelow y f)) (nhdsWithin x (Set.Ioi x)) (nhds (WithTop.untopD 0 (firstPassageBelow x f)))

Finite strict passage times are right-continuous in the level.

theorem BGW.StableTrees.isCadlag_untopD_firstPassageBelow (f : Skorokhod.DLoc) (hfin : ∀ (x : NNReal), firstPassageBelow x f < ⊤) : IsCadlag fun (x : NNReal) => ↑(WithTop.untopD 0 (firstPassageBelow x f))

Finite strict passage times form a càdlàg nondecreasing real process.

theorem BGW.StableTrees.firstPassageBelow_eq_sInf_runningInf (x : NNReal) (f : Skorokhod.DLoc) : firstPassageBelow x f = sInf {t : WithTop NNReal | ∃ (u : NNReal), t = ↑u ∧ ↑x < -runningInfLoc f u}

Strict passage is the inverse of the negative running infimum.

theorem BGW.StableTrees.runningInfLoc_lt_sandwich (x t : NNReal) (f : Skorokhod.DLoc) : (firstPassageBelow x f < ↑t → runningInfLoc f t < -↑x) ∧ (runningInfLoc f t < -↑x → firstPassageBelow x f ≤ ↑t)

Strict-passage/running-infimum sandwich.

theorem BGW.StableTrees.runningInfLoc_eq_of_firstPassageBelow_eq_coe {f : Skorokhod.DLoc} {x s : NNReal} (hs : firstPassageBelow x f = ↑s) (hval : ↑f s = -↑x) : runningInfLoc f s = -↑x

At a finite creeping passage time, the running infimum is the barrier.

theorem BGW.StableTrees.firstPassageBelow_add_of_creeping {f : Skorokhod.DLoc} {s x y : NNReal} (hs : firstPassageBelow x f = ↑s) (hval : ↑f s = -↑x) : firstPassageBelow (x + y) f = firstPassageBelow x f + firstPassageBelow y (Skorokhod.DLoc.shiftAt (firstPassageBelow x) f)

Creeping at a passage time gives the additive decomposition at the next level.

theorem BGW.StableTrees.reflected_shift_of_creeping {f : Skorokhod.DLoc} {s x : NNReal} (hs : firstPassageBelow x f = ↑s) (hval : ↑f s = -↑x) (t : NNReal) : ↑f (s + t) - runningInfLoc f (s + t) = ↑(Skorokhod.DLoc.shift s f) t - runningInfLoc (Skorokhod.DLoc.shift s f) t

The reflected path after a creeping passage time is the reflected centered shift.

theorem BGW.StableTrees.runningInfLoc_eq_iInf_rat (f : Skorokhod.DLoc) (t : NNReal) : runningInfLoc f t = ⨅ (q : ℚ), if 0 ≤ q ∧ ↑q ≤ ↑t then ↑f (↑q).toNNReal else ↑f t

Rational times, with the terminal value as a fallback, compute the running infimum.

theorem BGW.StableTrees.time_progressive (q : ℚ) : MeasureTheory.IsStronglyProgressive Skorokhod.DLoc.filtration fun (t : NNReal) (x : Skorokhod.DLoc) => min (↑q).toNNReal t

Clamping time at a rational time is strongly progressive.

theorem BGW.StableTrees.isStronglyProgressive_runningInfLoc : MeasureTheory.IsStronglyProgressive Skorokhod.DLoc.filtration fun (t : NNReal) (f : Skorokhod.DLoc) => runningInfLoc f t

The running infimum is strongly progressive for the local filtration.

theorem BGW.StableTrees.measurable_runningInfLoc_uncurry : Measurable fun (p : NNReal × Skorokhod.DLoc) => runningInfLoc p.2 p.1

Joint measurability of the running infimum in time and path.

theorem BGW.StableTrees.stronglyAdapted_runningInfLoc : MeasureTheory.StronglyAdapted Skorokhod.DLoc.filtration fun (t : NNReal) (f : Skorokhod.DLoc) => runningInfLoc f t

The running infimum is adapted to the right-continuous local filtration.