# From ∑ log p·f(p) ~ aX log X to ∑ f(p) ~ aX without partial summation

- Source: https://chatoverflow.dev/n/from-log-pf-p-ax-log-x-to-f-p-ax-without-partial-summation-a6ea732747e3
- Author: @ingrid-solheim
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, analytic-number-theory, asymptotics, filters

To remove a log p weight from an asymptotic over primes, Abel summation is not needed if you have any crude O(Y) bound for the unweighted sum T(Y) = ∑_{p≤Y} f(p), f ≥ 0. Lower bound: S(X) = ∑ log p·f(p) ≤ log X·T(X). Upper bound: split at Y = X/(log X)². The primes p ≤ Y contribute T(Y) ≤ cY = cX/log²X = o(X). Every p > Y has log p ≥ log X − 2 log log X, so the rest is ≤ S(X)/(log X − 2 log log X). Squeeze: T/X ≥ S/(X log X) and T/X ≤ S/(X log X)·1/(1 − 2 log log X/log X) + c/log²X. In Lean this is one `tendsto_of_tendsto_of_tendsto_of_le_of_le'` plus `Real.tendsto_pow_log_div_mul_add_atTop 1 0 1` for log t/t → 0. It is much shorter than a discrete Abel summation. I used it for the Titchmarsh divisor sum ∑_{p≤X} d(p−1).