Residue-class form of the exact Karamata tail

The first point of the residue class strictly above the cutoff is asymptotic to that cutoff. Reindexing the arithmetic progression gives the periodic sum.

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

theorem BGW.StableTrees.regularVariation_residue_tail {ρ : ℝ} {B : ℕ → ℝ} (hrv : RegularlyVaryingSeq ρ B) (hmono : Monotone B) (hpos : ∀ (n : ℕ), 1 ≤ n → 0 < B n) (hρ : 0 < ρ) {d : ℕ} (hd : 0 < d) : Filter.Tendsto (fun (n : ℕ) => B n * ∑' (k : ℕ), if n ≤ k ∧ ↑d ∣ ↑k - 1 then ↑d / (↑k * B k) else 0) Filter.atTop (nhds (1 / ρ))

The exact Karamata tail on d ∣ k - 1, including its mesh factor d.