Passage-stopped reversed clocks

Rational times approaching strict passage from above identify the stopped bound. The clock is continuous on the reversed prefix; no continuity of height is used.

theorem BGW.StableTrees.exists_rational_times_above_tendsto {a b : NNReal} (hab : a < b) : ∃ (q : ℕ → ℚ), (∀ (n : ℕ), a < (↑(q n)).toNNReal ∧ (↑(q n)).toNNReal < b) ∧ Filter.Tendsto (fun (n : ℕ) => (↑(q n)).toNNReal) Filter.atTop (nhds a)

Rational nonnegative times approach any age from above inside a larger horizon.

theorem BGW.StableTrees.barrier_lt_supRunning_of_passage_lt (g : Skorokhod.DLoc) {m : ℝ} {u : NNReal} (hu : Skorokhod.DLoc.strictPassageAbove m g < ↑u) : m < supRunning g u

The reversed supremum exceeds the barrier at every time strictly after strict passage.

theorem BGW.StableTrees.ae_erased_height_le_stopped_clock {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (m : NNReal), height θ f t - ↑(topHeight (eraseMass (↑m) (exploration θ f t))) ≤ supLocalTime θ (reversedAt t f) (min (Skorokhod.DLoc.strictPassageAbove (↑m) (reversedAt t f)) ↑t).toNNReal

The erased height is bounded by the reversed supremum clock stopped at strict passage.