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

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).