First moments of the height occupation near the excursion start

Translation of Lebesgue measure identifies the approximation on the later window, and the difference is exactly the occupation before the split age. Tonelli converts the error from deleting an initial age window into the integral of the small-depth probabilities. No pathwise sequence identification is required.

theorem BGW.StableTrees.heightApprox_sub_shift_eq (ε : ℝ) (f : Skorokhod.DLoc) (t a : NNReal) (hat : a ≤ t) : heightApprox ε f t - heightApprox ε (Skorokhod.DLoc.shift a f) (t - a) = ε⁻¹ * (MeasureTheory.volume {s : ℝ | 0 ≤ s ∧ s < ↑a ∧ ↑f s.toNNReal < futureInf f t s.toNNReal + ε}).toReal

Splitting the approximation leaves precisely its occupation before the split age.

theorem BGW.StableTrees.lintegral_heightApprox_sub_shift (μ : MeasureTheory.Measure Excursion) [MeasureTheory.SFinite μ] (ε : ℝ) (hε : 0 < ε) (t a : NNReal) (hat : a ≤ t) : ∫⁻ (e : Excursion), ENNReal.ofReal |heightApprox ε e.path t - heightApprox ε (Skorokhod.DLoc.shift a e.path) (t - a)| ∂μ = ENNReal.ofReal ε⁻¹ * ∫⁻ (s : ℝ) in Set.Ico 0 ↑a, μ {e : Excursion | ↑e.path s.toNNReal < futureInf e.path t s.toNNReal + ε}

Tonelli's identity for the error from deleting the initial occupation window.