Interpolation of vanishing left slopes

A monotone nonnegative numerator with a vanishing dyadic quotient has a vanishing quotient along the full positive filter. The numerator, rather than its quotient, is monotone.

theorem BGW.StableTrees.ae_tendsto_passageTime_leftSlope {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) (hx : 0 < x) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), Filter.Tendsto (fun (ε : ℝ) => (↑(passageTime x f) - ↑(passageTime (x - ε.toNNReal) f)) / ε) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

At a fixed positive level the finite right passage process has a zero full left slope.