Almost sure decay from geometric tail bounds

Summable geometric tails give almost sure convergence to zero of nonnegative difference quotients. The criterion retains countably many thresholds on a single full-measure event.

theorem BGW.StableTrees.ae_tendsto_passageTime_left_dyadic {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) (hx : 0 < x) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), Filter.Tendsto (fun (n : ℕ) => (↑(passageTime x f) - ↑(passageTime (x - x / 2 ^ n) f)) / ↑(x / 2 ^ n)) Filter.atTop (nhds 0)

At each deterministic positive level the left dyadic passage increments have zero slope.