Simultaneous vanishing of occupation at every jump start

The compensated dyadic left-slope event is interpolated pathwise on the common finite-passage event. The occupation bound then gives full-filter vanishing at every excursion start.

theorem BGW.StableTrees.passagePast_leftSlope_eq_ofReal (f : Skorokhod.DLoc) (hp : ∀ (y : NNReal), passagePast y f = ↑(passageTimeMinus y f)) (x ε : NNReal) (hε : 0 < ε) : (passagePast x f - passagePast (x - ε) f) / ↑ε = ENNReal.ofReal ((↑(passageTimeMinus x f) - ↑(passageTimeMinus (x - ε) f)) / ↑ε)

On finite passages the extended left quotient is the nonnegative real quotient.

theorem BGW.StableTrees.tendsto_passageTimeMinus_leftSlope_of_not_bad (f : Skorokhod.DLoc) (hp : ∀ (y : NNReal), passagePast y f = ↑(passageTimeMinus y f)) (hm : Monotone fun (y : NNReal) => passageTimeMinus y f) (x : NNReal) (hx : (x, f) ∉ excursionHeightLeftSlopeBad) : Filter.Tendsto (fun (ε : ℝ) => (↑(passageTimeMinus x f) - ↑(passageTimeMinus (x - ε.toNNReal) f)) / ε) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Outside the bad dyadic event, finite monotone left passages have zero full left slope.

theorem BGW.StableTrees.ae_tendsto_heightApprox_passageTimeMinus {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, Filter.Tendsto (fun (ε : ℝ) => heightApprox ε f (passageTimeMinus x f)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Pre-start vanishing: almost surely, at every passage jump level x, the host approximation at the excursion start T(x-) tends to 0 along the full filter ε → 0⁺.