Compact interior lower bounds for excursion paths, using rational-window uniqueness.

See Bertoin, Lévy Processes, Chapter IV.

noncomputable def BGW.StableTrees.excursionWindowInf (a b : NNReal) (e : Excursion) : ℝ

The infimum of the path on the compact window [a,b], expressed with a centered Skorokhod restriction so that its dependence on the path is measurable.

Equations

• BGW.StableTrees.excursionWindowInf a b e = (⨅ (s : ↑(Set.Icc 0 ↑(b - a))), (BGW.Skorokhod.DLoc.restrict (b - a) (BGW.Skorokhod.DLoc.shift a e.path)) s) + ↑e.path a

theorem BGW.StableTrees.measurable_excursionWindowInf (a b : NNReal) : Measurable (excursionWindowInf a b)

Compact window infima are measurable functions of the excursion mark.

theorem BGW.StableTrees.ae_jumpExcursion_leftLim_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, ∀ (t : NNReal), 0 < t → t < (jumpExcursion x f).lifetime → 0 < Function.leftLim (↑(jumpExcursion x f).path) t

Almost surely, every marked excursion has a strictly positive left limit at every strictly interior time. This excludes a second generalized minimizer in a rational window.

theorem BGW.StableTrees.ae_jumpExcursion_windowInf_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, ∀ (a b : NNReal), 0 < a → a ≤ b → b < (jumpExcursion x f).lifetime → 0 < excursionWindowInf a b (jumpExcursion x f)

Every compact window strictly inside a jump excursion has a positive lower bound.