Exact Karamata tails on a residue class

A monotone extension of the discrete summand brackets sums on arithmetic progressions between their step integrals. Regular variation identifies the integral on compact windows; Potter bounds supply an integrable tail bound.

Reference: J.-F. Le Gall, Random trees and applications, Probab. Surveys 2 (2005), Section 1.

theorem BGW.StableTrees.regularVariation_progression_tail {ρ : ℝ} {B : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ B) (hmono : Monotone B) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < B n) (hρ : 0 < ρ) {d : ℕ} (hd : 0 < d) {s : ℕ → ℕ} (hs : Filter.Tendsto (fun (n : ℕ) => ↑(s n) / ↑n) Filter.atTop (nhds 1)) : Filter.Tendsto (fun (n : ℕ) => B n * (↑d * ∑' (m : ℕ), 1 / (↑(s n + d * m) * B (s n + d * m)))) Filter.atTop (nhds (1 / ρ))

Exact Karamata tail along an arithmetic progression whose starting point is asymptotic to the base time. The lattice mesh cancels in the leading constant.