A stopped-clock bound for erased exploration height #
A terminal source window with mass greater than the erasure retains some mass. The ancestral clock bounds its heights from below, and hence bounds the erased height.
theorem
BGW.StableTrees.erased_height_le_clock_of_sup_gt
(θ : ℝ)
(f : Skorokhod.DLoc)
{t u : NNReal}
(hu : u ≤ t)
(hf : ∀ (s : NNReal), Function.leftLim (↑f) s ≤ ↑f s)
(hc : Function.leftLim (↑f) (t - u) = ↑f (t - u))
(hmono : Monotone fun (u : ↑(Set.Iic t)) => supLocalTime θ (reversedAt t f) ↑u)
(hclock :
∀ᵐ (x : ℝ) ∂(explorationStieltjes f t).measure.restrict (Set.Ioc 0 ↑t), 0 < x ∧ x ≤ ↑t ∧ 0 ≤ height θ f x.toNNReal ∧ height θ f x.toNNReal = supLocalTime θ (reversedAt t f) t - supLocalTime θ (reversedAt t f) (t - x.toNNReal))
(habove : (exploration θ f t) (Set.Ioi (height θ f t).toNNReal) = 0)
(m : ENNReal)
(hm : m < ENNReal.ofReal (supRunning (reversedAt t f) u))
:
Surplus terminal-source mass bounds the erased height by the reversed clock.
theorem
BGW.StableTrees.ae_erased_height_le_clock_rational
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
{t : NNReal}
(ht : 0 < t)
:
∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (q : ℚ),
(↑q).toNNReal ≤ t →
∀ m < ENNReal.ofReal (supRunning (reversedAt t f) (↑q).toNNReal),
height θ f t - ↑(topHeight (eraseMass m (exploration θ f t))) ≤ supLocalTime θ (reversedAt t f) (↑q).toNNReal
On one event all rational reversed ages give the stopped-clock comparison, for every mass.