Erased height and the reversed supremum clock

Surplus mass in a terminal source window remains after erasure. Its ancestral heights bound the surviving support from below. Only continuity of the reversed supremum clock is used; continuity of the height process is unnecessary.

theorem BGW.StableTrees.eraseMass_Ioi_eq_zero {ρ : MeasureTheory.Measure NNReal} {R : NNReal} (hρ : ρ (Set.Ioi R) = 0) (m : ENNReal) : (eraseMass m ρ) (Set.Ioi R) = 0

Erasure preserves a mass-free upper tail, without a finiteness assumption.

theorem BGW.StableTrees.measure_Ioi_eq_zero_of_topHeight_lt {ρ : MeasureTheory.Measure NNReal} {R h : NNReal} (hR : ρ (Set.Ioi R) = 0) (hh : topHeight ρ < h) : ρ (Set.Ioi h) = 0

An upper bound for the support top makes every strictly higher tail mass-free.

theorem BGW.StableTrees.eraseMass_Ioi_pos {ρ : MeasureTheory.Measure NNReal} [MeasureTheory.IsFiniteMeasure ρ] {m : ENNReal} {h : NNReal} (hm : m < ρ (Set.Ioi h)) : 0 < (eraseMass m ρ) (Set.Ioi h)

A finite measure retains positive upper-tail mass whenever that tail exceeds the erasure.

theorem BGW.StableTrees.exploration_source_terminal_mass (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)) : (explorationStieltjes f t).measure (Set.Ioc ↑(t - u) ↑t) = ENNReal.ofReal (supRunning (reversedAt t f) u)

At a continuity endpoint, the terminal source-window mass is a reversed running supremum.