Supremum occupation approximations

Deterministic bounds and fixed-time measurability for the running supremum and its occupation approximations. The simultaneous occupation-sequence existence theorem and the ascending local-time construction are not established here.

These are preliminary objects for Duquesne and Le Gall, Random Trees, Lévy Processes and Spatial Branching Processes, Astérisque 281 (2002), Section 1.1.

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

Running supremum S_t = sup_{u ≤ t} X_u.

Equations

• BGW.StableTrees.supRunning f t = ⨆ (u : ↑(Set.Iic t)), ↑f ↑u

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

The reflected-at-supremum process S_t - X_t.

Equations

• BGW.StableTrees.supReflected f t = BGW.StableTrees.supRunning f t - ↑f t

noncomputable def BGW.StableTrees.supOccupation (ε : ℝ) (f : Skorokhod.DLoc) (t : NNReal) : ℝ

Occupation approximation ε⁻¹ · Leb{s ≤ t | S_s - X_s < ε}.

Equations

• BGW.StableTrees.supOccupation ε f t = ε⁻¹ * (MeasureTheory.volume {s : ℝ | 0 ≤ s ∧ s ≤ ↑t ∧ BGW.StableTrees.supReflected f s.toNNReal < ε}).toReal

def BGW.StableTrees.IsSupOccupationSeq (θ : ℝ) (ε : ℕ → ℝ) : Prop

A deterministic sequence is a simultaneous occupation sequence: positive, strictly decreasing to 0, and almost surely the approximations converge at every time at once.

Equations

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

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

A local càdlàg path is bounded above on each initial compact interval.

theorem BGW.StableTrees.eval_le_supRunning (f : Skorokhod.DLoc) {u t : NNReal} (hut : u ≤ t) : ↑f u ≤ supRunning f t

Every value before t is bounded above by the running supremum at t.

theorem BGW.StableTrees.supRunning_le (f : Skorokhod.DLoc) (t : NNReal) {a : ℝ} (ha : ∀ (u : ↑(Set.Iic t)), ↑f ↑u ≤ a) : supRunning f t ≤ a

An upper bound for the path on [0,t] bounds its running supremum.

theorem BGW.StableTrees.monotone_supRunning (f : Skorokhod.DLoc) : Monotone (supRunning f)

The running supremum is monotone in time.

theorem BGW.StableTrees.supRunning_zero (f : Skorokhod.DLoc) : supRunning f 0 = ↑f 0

At the origin the running supremum equals the initial value.

theorem BGW.StableTrees.supReflected_nonneg (f : Skorokhod.DLoc) (t : NNReal) : 0 ≤ supReflected f t

Reflection at the running supremum is nonnegative for every path.

theorem BGW.StableTrees.supReflected_zero (f : Skorokhod.DLoc) : supReflected f 0 = 0

Reflection at the running supremum starts at zero for every path.

theorem BGW.StableTrees.supOccupation_set_subset (ε : ℝ) (f : Skorokhod.DLoc) (t : NNReal) : {s : ℝ | 0 ≤ s ∧ s ≤ ↑t ∧ supReflected f s.toNNReal < ε} ⊆ Set.Icc 0 ↑t

The occupation set is contained in the initial compact time interval.

theorem BGW.StableTrees.supOccupation_volume_ne_top (ε : ℝ) (f : Skorokhod.DLoc) (t : NNReal) : MeasureTheory.volume {s : ℝ | 0 ≤ s ∧ s ≤ ↑t ∧ supReflected f s.toNNReal < ε} ≠ ⊤

The occupation set has finite Lebesgue measure, without any measurability premise.

theorem BGW.StableTrees.supOccupation_nonneg {ε : ℝ} (hε : 0 ≤ ε) (f : Skorokhod.DLoc) (t : NNReal) : 0 ≤ supOccupation ε f t

The occupation approximation is nonnegative for a positive cutoff.

theorem BGW.StableTrees.monotone_supOccupation {ε : ℝ} (hε : 0 ≤ ε) (f : Skorokhod.DLoc) : Monotone (supOccupation ε f)

The occupation approximation is monotone in its time horizon.

theorem BGW.StableTrees.supOccupation_zero (ε : ℝ) (f : Skorokhod.DLoc) : supOccupation ε f 0 = 0

The approximation vanishes at time zero.

theorem BGW.StableTrees.supOccupation_of_nonpos {ε : ℝ} (hε : ε ≤ 0) (f : Skorokhod.DLoc) (t : NNReal) : supOccupation ε f t = 0

A nonpositive cutoff gives the empty occupation set.

theorem BGW.StableTrees.measurable_supRunning (t : NNReal) : Measurable fun (f : Skorokhod.DLoc) => supRunning f t

Fixed-time measurability of the running supremum.

theorem BGW.StableTrees.measurable_supReflected (t : NNReal) : Measurable fun (f : Skorokhod.DLoc) => supReflected f t

Fixed-time measurability of the reflected process.

theorem BGW.StableTrees.lt_supRunning_iff (a : ℝ) (f : Skorokhod.DLoc) (t : NNReal) : a < supRunning f t ↔ Skorokhod.DLoc.strictPassageAbove a f < ↑t ∨ a < ↑f t

A strict supremum crossing is detected before the horizon or at its endpoint.

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

Joint measurability of the running supremum in time and path.

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

Joint measurability of reflection at the supremum.

theorem BGW.StableTrees.measurable_supOccupation_uncurry : Measurable fun (p : ℝ × NNReal × Skorokhod.DLoc) => supOccupation p.1 p.2.2 p.2.1

Joint measurability of the occupation approximation in cutoff, horizon, and path.

theorem BGW.StableTrees.measurable_supOccupation_limsup (ε : ℕ → ℝ) : Measurable fun (p : NNReal × Skorokhod.DLoc) => Filter.limsup (fun (k : ℕ) => supOccupation (ε k) p.2 p.1) Filter.atTop

Joint measurability of the real limsup along any deterministic cutoff sequence.

theorem BGW.StableTrees.IsSupOccupationSeq.ae_tendsto_limsup {θ : ℝ} {ε : ℕ → ℝ} (hε : IsSupOccupationSeq θ ε) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), Filter.Tendsto (fun (k : ℕ) => supOccupation (ε k) f t) Filter.atTop (nhds (Filter.limsup (fun (k : ℕ) => supOccupation (ε k) f t) Filter.atTop))

Every simultaneous occupation sequence converges to its real limsup on the same event.

theorem BGW.StableTrees.IsSupOccupationSeq.ae_limsup_zero_nonneg_monotone {θ : ℝ} {ε : ℕ → ℝ} (hε : IsSupOccupationSeq θ ε) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), Filter.limsup (fun (k : ℕ) => supOccupation (ε k) f 0) Filter.atTop = 0 ∧ (∀ (t : NNReal), 0 ≤ Filter.limsup (fun (k : ℕ) => supOccupation (ε k) f t) Filter.atTop) ∧ Monotone fun (t : NNReal) => Filter.limsup (fun (k : ℕ) => supOccupation (ε k) f t) Filter.atTop

Given simultaneous convergence, its limit starts at zero, is nonnegative, and is monotone. This does not supply the simultaneous sequence or continuity of its limit.

noncomputable def BGW.StableTrees.supLadderExponent (θ q lam : ℝ) : ℝ

The ladder exponent κ(q, λ) = (q - λ^θ) / (q^{1/θ} - λ), extended continuously at λ = q^{1/θ} by θ q^{1 - 1/θ}.

Equations

• BGW.StableTrees.supLadderExponent θ q lam = if lam = q ^ (1 / θ) then θ * q ^ (1 - 1 / θ) else (q - lam ^ θ) / (q ^ (1 / θ) - lam)

theorem BGW.StableTrees.supLadderExponent_diagonal (θ q : ℝ) : supLadderExponent θ q (q ^ (1 / θ)) = θ * q ^ (1 - 1 / θ)

The diagonal branch of the ladder exponent.

theorem BGW.StableTrees.supLadderExponent_zero_right {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 ≤ q) : supLadderExponent θ q 0 = q ^ (1 - 1 / θ)

The time marginal of the proposed ladder exponent.

theorem BGW.StableTrees.supLadderExponent_zero_left {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {lam : ℝ} (hlam : 0 ≤ lam) : supLadderExponent θ 0 lam = lam ^ (θ - 1)

The height marginal of the proposed ladder exponent.