Uniform first-moment bound for the initial height occupation

The small-depth estimate cancels the cutoff normalization. The remaining integrated survival tail vanishes with the initial age window.

theorem BGW.StableTrees.exists_lintegral_heightApprox_sub_shift_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t a : NNReal), 0 < t → a + a ≤ t → ∀ (ε : ℝ), 0 < ε → ∫⁻ (e : Excursion) in {e : Excursion | t < e.lifetime}, ENNReal.ofReal |heightApprox ε e.path t - heightApprox ε (Skorokhod.DLoc.shift a e.path) (t - a)| ∂excursionMeasure θ ≤ ENNReal.ofReal (C * (↑t / 2) ^ (-1 / θ)) * ∫⁻ (s : ℝ) in Set.Ioo 0 ↑a, (excursionMeasure θ) {e : Excursion | s.toNNReal < e.lifetime}

Uniform first-moment control of the error from removing an initial age window.