Exact logarithmic expansion of the smooth part #
theorem
NairTenenbaum.log_smoothPart_eq_prime_sum
(n : ℕ+)
{z : ℝ}
(hz : 0 ≤ z)
:
Real.log ↑↑(smoothPart n z) = ∑ p ∈ (↑n).primeFactors with ↑p ≤ z, ↑((↑n).factorization p) * Real.log ↑p
theorem
NairTenenbaum.sum_log_smoothPart_eq_prime_sum
{ι : Type u_1}
(S : Finset ι)
(n : ι → ℕ+)
{z : ℝ}
(hz : 0 ≤ z)
:
∑ i ∈ S, Real.log ↑↑(smoothPart (n i) z) = ∑ p ∈ Finset.range (⌊z⌋₊ + 1) with Nat.Prime p, (∑ i ∈ S, ↑((↑(n i)).factorization p)) * Real.log ↑p
A fixed common prime cutoff allows summing the local logarithmic masses before estimating how often each prime power divides a value.