A measurable stopped-clock barrier event

Rational clock tests describe the barrier before a local-time level. This description is prefix-local and separates the reversed prefix from the fresh infimum depth.

def BGW.StableTrees.erasedClockBarrier (θ : ℝ) (t r : NNReal) (v : ℝ) : Set (Skorokhod.DLoc × Skorokhod.DLoc)

A rational clock level above v is reached before the fresh depth is exceeded.

Equations

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

theorem BGW.StableTrees.measurableSet_erasedClockBarrier (θ : ℝ) (t r : NNReal) (v : ℝ) : MeasurableSet (erasedClockBarrier θ t r v)

The rational stopped-clock barrier is measurable.

theorem BGW.StableTrees.erasedClockBarrier_prefix_local (θ : ℝ) (t r : NNReal) (v : ℝ) (f g h : Skorokhod.DLoc) (he : Skorokhod.DLoc.restrict t f = Skorokhod.DLoc.restrict t g) : (f, h) ∈ erasedClockBarrier θ t r v ↔ (g, h) ∈ erasedClockBarrier θ t r v

The barrier reads its first path only on the compact prefix.

theorem BGW.StableTrees.ae_erased_height_exceedance_barrier {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) (r : NNReal) (v : ℝ) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), v < height θ f t - ↑(topHeight (eraseMass (ENNReal.ofReal (-futureInf (Skorokhod.DLoc.shift t f) r 0)) (exploration θ f t))) → (reversedAt t f, Skorokhod.DLoc.shift t f) ∈ erasedClockBarrier θ t r v

Erased-height exceedance implies the rational stopped-clock barrier.

theorem BGW.StableTrees.ae_barrier_supLadderHeight_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t r v : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (g : Skorokhod.DLoc), (f, g) ∈ erasedClockBarrier θ t r ↑v → supLadderHeight θ v f ≤ -runningInfLoc g r

Under the full stable law, the stopped-clock barrier implies the ladder-height bound.