Erasure of finite measures on heights

The tail quantile retains precisely the mass below the cut and the necessary part of its atom. Continuity of measures identifies both sides of the cut, including complete erasure.

theorem BGW.StableTrees.eraseMass_univ {ρ : MeasureTheory.Measure NNReal} [MeasureTheory.IsFiniteMeasure ρ] {m : ENNReal} (hm : m ≤ ρ Set.univ) : (eraseMass m ρ) Set.univ = ρ Set.univ - m

Erasing at most the total (finite) mass removes exactly that mass.

theorem BGW.StableTrees.eraseMass_Iic {ρ : MeasureTheory.Measure NNReal} [MeasureTheory.IsFiniteMeasure ρ] (m : ENNReal) (h : NNReal) : (eraseMass m ρ) (Set.Iic h) = min (ρ (Set.Iic h)) (ρ Set.univ - m)

Distribution-function characterization of erasure (includes m ≥ ρ univ and m = ⊤).