Exact cancellation of the occupation before an excursion start

A valid excursion cut adds no new minimum before its start. Splitting the occupation at the start therefore gives an exact additive identity for every cutoff, including zero.

theorem BGW.StableTrees.futureInf_eq_before_cut {g d : NNReal} {f : Skorokhod.DLoc} (hcut : cutValid g d f) {u s : NNReal} (hu : u ≤ d - g) (hs : s ≤ g) : futureInf f (g + u) s = futureInf f g s

Extending a horizon inside a valid cut leaves all pre-start future infima unchanged.

theorem BGW.StableTrees.heightApprox_jumpExcursion_add (ε : ℝ) (x : NNReal) (f : Skorokhod.DLoc) (hcut : cutValid (passageTimeMinus x f) (passageTime x f) f) {u : NNReal} (hu : u ≤ passageTime x f - passageTimeMinus x f) : heightApprox ε f (passageTimeMinus x f + u) = heightApprox ε f (passageTimeMinus x f) + heightApprox ε (jumpExcursion x f).path u

Exact finite-cutoff cancellation (deterministic): if the cut of (T(x-), T(x)) is valid, then for every cutoff ε and every age u ≤ T(x) - T(x-), the host approximation at T(x-) + u is the host approximation at T(x-) plus the approximation of the jump excursion at age u (no correction term: the pre-start integrands coincide).

theorem BGW.StableTrees.heightEps_tendsto_nhdsWithin_zero (θ : ℝ) : Filter.Tendsto (heightEps θ) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))

The chosen cutoffs approach zero from above, including the fallback parameter branch.

theorem BGW.StableTrees.heightUniv_jumpExcursion_eq (θ : ℝ) (x : NNReal) (f : Skorokhod.DLoc) (hcut : cutValid (passageTimeMinus x f) (passageTime x f) f) (hpre : Filter.Tendsto (fun (ε : ℝ) => heightApprox ε f (passageTimeMinus x f)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) {u : NNReal} (hu : u ≤ passageTime x f - passageTimeMinus x f) : heightUniv θ (jumpExcursion x f).path u = heightUniv θ f (passageTimeMinus x f + u)

Raw height of a jump excursion (deterministic): with a valid cut and a vanishing pre-start approximation at T(x-), the universal raw height of the excursion at age u ≤ T(x) - T(x-) is the host's universal raw height at T(x-) + u.