Reflection at the running supremum

The measurable reflected family, occupation continuity, contact geometry, and transfer of the stable Markov property. Deterministic restart formulas hold for every path; probabilistic statements use spectral positivity or the sealed shift laws only where needed.

References

• J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters III, IV and VI.
• A. E. Kyprianou, Fluctuations of Lévy Processes with Applications, 2nd ed., Springer, 2014, Chapters 3 and 6.

noncomputable def BGW.StableTrees.supReflectedFrom (x : NNReal) (f : Skorokhod.DLoc) (t : NNReal) : ℝ

Reflected-at-supremum process started from x ≥ 0: t ↦ max x S_t - X_t.

Equations

• BGW.StableTrees.supReflectedFrom x f t = max (↑x) (BGW.StableTrees.supRunning f t) - ↑f t

theorem BGW.StableTrees.isCadlag_supRunning (f : Skorokhod.DLoc) : IsCadlag (supRunning f)

The running supremum is càdlàg.

theorem BGW.StableTrees.isCadlag_supReflectedFrom (x : NNReal) (f : Skorokhod.DLoc) : IsCadlag (supReflectedFrom x f)

Càdlàg-ness of the reflected path for every càdlàg f and every start x.

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

The reflected path as a total DLoc-valued map (no junk case).

Equations

• BGW.StableTrees.supReflectedFromLoc x f = ⟨BGW.StableTrees.supReflectedFrom x f, ⋯⟩

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

The contact set {t | S_t = X_t} (equivalently {R = 0}, R ≥ 0).

Equations

• BGW.StableTrees.supContact f = {t : NNReal | BGW.StableTrees.supReflected f t = 0}

theorem BGW.StableTrees.supReflectedFrom_zero_apply {f : Skorokhod.DLoc} (h0 : ↑f 0 = 0) (t : NNReal) : supReflectedFrom 0 f t = supReflected f t

Started from 0 and with f 0 = 0, the family reduces to supReflected.

theorem BGW.StableTrees.supReflectedFrom_nonneg (x : NNReal) (f : Skorokhod.DLoc) (t : NNReal) : 0 ≤ supReflectedFrom x f t

The reflection is nonnegative, and ≥ x - X_t.

theorem BGW.StableTrees.supReflectedFrom_restart (x : NNReal) (f : Skorokhod.DLoc) (s u : NNReal) : supReflectedFrom x f (s + u) = supReflectedFrom (supReflectedFrom x f s).toNNReal (Skorokhod.DLoc.shift s f) u

Deterministic restart (everywhere, no hypothesis). The reflected path at time s + u is the reflected path of the centered shifted path, started from the value R^x_s.

theorem BGW.StableTrees.supReflectedFrom_restart_shiftAt (x : NNReal) (τ : Skorokhod.DLoc → ENNReal) {f : Skorokhod.DLoc} (hτ : τ f < ⊤) (u : NNReal) : supReflectedFrom x f ((τ f).toNNReal + u) = supReflectedFrom (supReflectedFrom x f (τ f).toNNReal).toNNReal (Skorokhod.DLoc.shiftAt τ f) u

Restart at a random time (on {τ f < ⊤}; junk shift 0 elsewhere).

theorem BGW.StableTrees.measurable_supReflectedFrom_uncurry : Measurable fun (p : NNReal × Skorokhod.DLoc × NNReal) => supReflectedFrom p.1 p.2.1 p.2.2

Joint measurability of (x, f, t) ↦ R^x_t(f).

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

Joint measurability of the DLoc-valued reflection in (x, f).

theorem BGW.StableTrees.supReflectedFrom_le_leftLim {f : Skorokhod.DLoc} (hf : ∀ (s : NNReal), Function.leftLim (↑f) s ≤ ↑f s) (x t : NNReal) : supReflectedFrom x f t ≤ Function.leftLim (supReflectedFrom x f) t

No positive jumps (under spectral positivity of X): R t ≤ leftLim R t, every x ≥ 0.

theorem BGW.StableTrees.ae_supReflectedFrom_le_leftLim {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (x t : NNReal), supReflectedFrom x f t ≤ Function.leftLim (supReflectedFrom x f) t

Almost-sure form for the stable law, simultaneously in x and t.

theorem BGW.StableTrees.supOccupation_sub_mem {ε : ℝ} (hε : 0 < ε) (f : Skorokhod.DLoc) {s t : NNReal} (hst : s ≤ t) : 0 ≤ supOccupation ε f t - supOccupation ε f s ∧ supOccupation ε f t - supOccupation ε f s ≤ ε⁻¹ * (↑t - ↑s)

Increment bounds: monotone and ε⁻¹-Lipschitz increments.

theorem BGW.StableTrees.lipschitzWith_supOccupation {ε : ℝ} (hε : 0 < ε) (f : Skorokhod.DLoc) : LipschitzWith ε⁻¹.toNNReal fun (t : NNReal) => supOccupation ε f t

t ↦ supOccupation ε f t is ε⁻¹-Lipschitz.

theorem BGW.StableTrees.continuous_supOccupation {ε : ℝ} (hε : 0 < ε) (f : Skorokhod.DLoc) : Continuous fun (t : NNReal) => supOccupation ε f t

Continuity (hence continuity and monotonicity together with monotone_supOccupation).

theorem BGW.StableTrees.isCadlag_supReflected (f : Skorokhod.DLoc) : IsCadlag (supReflected f)

Reflection at the running supremum is càdlàg.

theorem BGW.StableTrees.supReflected_le_leftLim {f : Skorokhod.DLoc} (hf : ∀ (s : NNReal), Function.leftLim (↑f) s ≤ ↑f s) (t : NNReal) : supReflected f t ≤ Function.leftLim (supReflected f) t

Spectral positivity prevents positive jumps of the ordinary reflected path.

theorem BGW.StableTrees.supContact_rightClosed (f : Skorokhod.DLoc) {t : NNReal} (h : ∀ (δ : NNReal), 0 < δ → ∃ u ∈ supContact f, t < u ∧ u < t + δ) : t ∈ supContact f

Right-accumulation points of the contact set are contact times.

theorem BGW.StableTrees.isClosed_supContact {f : Skorokhod.DLoc} (hf : ∀ (s : NNReal), Function.leftLim (↑f) s ≤ ↑f s) : IsClosed (supContact f)

With no negative jumps of the path, its supremum-contact set is closed.

theorem BGW.StableTrees.mem_supContact_iff {f : Skorokhod.DLoc} {t : NNReal} : t ∈ supContact f ↔ ↑f t = supRunning f t

Contact occurs exactly when the path attains its running supremum.

theorem BGW.StableTrees.exists_excursionInterval_of_supReflected_pos {f : Skorokhod.DLoc} (h0 : ↑f 0 = 0) (hf : ∀ (s : NNReal), Function.leftLim (↑f) s ≤ ↑f s) {t : NNReal} (ht : 0 < supReflected f t) : ∃ (g : NNReal) (d : ENNReal), g < t ∧ ↑t < d ∧ supReflected f g = 0 ∧ (∀ (u : NNReal), g < u → ↑u < d → 0 < supReflected f u) ∧ ∀ (d' : NNReal), d = ↑d' → supReflected f d' = 0

Every positive reflected value lies between consecutive contact times, with an infinite right endpoint when there is no later contact.

theorem BGW.StableTrees.supRunning_congr_prefix {f g : Skorokhod.DLoc} {t : NNReal} (h : ∀ u ≤ t, ↑f u = ↑g u) : supRunning f t = supRunning g t

The running supremum depends only on the prefix of the path.

theorem BGW.StableTrees.supReflectedFrom_congr_prefix (x : NNReal) {f g : Skorokhod.DLoc} {t : NNReal} (h : ∀ u ≤ t, ↑f u = ↑g u) : supReflectedFrom x f t = supReflectedFrom x g t

Reflection at the supremum depends only on the prefix of the path.

theorem BGW.StableTrees.supOccupation_congr_prefix (ε : ℝ) {f g : Skorokhod.DLoc} {t : NNReal} (h : ∀ u ≤ t, ↑f u = ↑g u) : supOccupation ε f t = supOccupation ε g t

Occupation up to a fixed horizon depends only on the path on that horizon.

theorem BGW.StableTrees.measurable_rawFiltration_supReflectedFrom (x t : NNReal) : Measurable fun (f : Skorokhod.DLoc) => supReflectedFrom x f t

Raw adaptedness: R^x_t is measurable for the raw filtration σ(X_u, u ≤ t).

theorem BGW.StableTrees.measurable_rawFiltration_supOccupation (ε : ℝ) (t : NNReal) : Measurable fun (f : Skorokhod.DLoc) => supOccupation ε f t

Raw adaptedness of the occupation functional, every ε.

theorem BGW.StableTrees.isStronglyProgressive_supReflectedFrom (x : NNReal) : MeasureTheory.IsStronglyProgressive Skorokhod.DLoc.filtration fun (t : NNReal) (f : Skorokhod.DLoc) => supReflectedFrom x f t

The reflected process is progressively measurable for the natural filtration.