Vanishing integrated excursion survival tails near age zero

Integrability of the lifetime tail gives vanishing mass on shrinking initial windows.

theorem BGW.StableTrees.measurable_excursion_lifetime_tail {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : Measurable fun (s : ℝ) => (excursionMeasure θ) {e : Excursion | s.toNNReal < e.lifetime}

The survival mass is a measurable function of the observation age.

theorem BGW.StableTrees.tendsto_lintegral_excursion_lifetime_tail_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (T : NNReal) (a : ℕ → NNReal) (ha : Filter.Tendsto a Filter.atTop (nhds 0)) (hle : ∀ (n : ℕ), a n ≤ T) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (s : ℝ) in Set.Ioo 0 ↑(a n), (excursionMeasure θ) {e : Excursion | s.toNNReal < e.lifetime}) Filter.atTop (nhds 0)

Integrated lifetime tails vanish on any sequence of shrinking initial age windows.