Minimum uniqueness on rational windows

Window adapters using barrier inequalities, without assuming an excursion candidate (J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VII).

theorem BGW.StableTrees.isGenMinimizer_supportWindow {f : Skorokhod.DLoc} (hf : NoNegJumps f) {b : ℝ} {r g q : NNReal} (hrg : r < g) (hgq : g < q) (hl : Function.leftLim (↑f) g = b) (hb : ∀ u ≤ q, b ≤ ↑f u) : IsGenMinimizer (Skorokhod.DLoc.restrict (q - r) (Skorokhod.DLoc.shift r f)) (shiftedWindowTime r g q ⋯ ⋯)

A left-limit contact with a lower barrier is a generalized window minimizer.

def BGW.StableTrees.RationalWindowMinima (f : Skorokhod.DLoc) : Prop

On every rational window, every generalized minimizer is continuous and any two such minimizers coincide.

Equations

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

theorem BGW.StableTrees.ae_rationalWindowMinima {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), RationalWindowMinima f

Countable transfer of minimum continuity and uniqueness to all rational windows.

theorem BGW.StableTrees.continuousAt_of_supportWindow {f : Skorokhod.DLoc} {r g q : NNReal} (hrg : r < g) (hgq : g < q) (hc : ContinuousAt (⇑(Skorokhod.DLoc.restrict (q - r) (Skorokhod.DLoc.shift r f))) (shiftedWindowTime r g q ⋯ ⋯)) : ContinuousAt (↑f) g

Continuity of the window at an interior time identifies the path value with its left limit, and hence gives continuity of the original local path there.

theorem BGW.StableTrees.exists_supportWindow {g d : NNReal} (hg : 0 < g) (hgd : g < d) : ∃ (r : ℚ≥0) (q : ℚ≥0), ↑r < g ∧ g < ↑q ∧ ↑q < d

Every strictly positive interval has rational windows around its positive left endpoint.