Riemann sums on arithmetic progressions

Riemann sums over residue classes, used in the proof of Kendall's identity.

References: (D. G. Kendall, Some problems in the theory of dams, J. Roy. Statist. Soc. Ser. B 19 (1957), 207–212; A. A. Borovkov, Stochastic Processes in Queueing Theory, Springer, 1976; J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VII, Corollary 3).

theorem BGW.StableTrees.tendsto_progression_riemann_sum {d : ℕ} (hd : 0 < d) (ℓ : ℕ → ℕ) {g : ℝ → ℝ} (hg : Continuous g) (hsupp : HasCompactSupport g) (hpos : tsupport g ⊆ Set.Ioi 0) : Filter.Tendsto (fun (n : ℕ) => ∑' (k : ℕ), if ↑d ∣ ↑k - ↑(ℓ n) then ↑d / ↑n * g (↑k / ↑n) else 0) Filter.atTop (nhds (∫ (s : ℝ), g s))

Arithmetic-progression Riemann sum (the lattice factor cancels): for continuous g with compact support inside (0, ∞), d ≥ 1, and any integers ℓ n, (d/n) Σ_{k ≥ 0, d ∣ k - ℓ n} g(k/n) → ∫ g.