Prime-power divisibility counts in the smooth logarithmic mass

theorem NairTenenbaum.factorization_eq_card_primePowers {n p L : ℕ} (hn : n ≠ 0) (hp : Nat.Prime p) (hL : n.factorization p ≤ L) : n.factorization p = {ν ∈ Finset.Icc 1 L | p ^ ν ∣ n}.card

theorem NairTenenbaum.sum_factorization_eq_primePower_counts {ι : Type u_1} (S : Finset ι) (n : ι → ℕ) (hn : ∀ i ∈ S, n i ≠ 0) {p L : ℕ} (hp : Nat.Prime p) (hL : ∀ i ∈ S, (n i).factorization p ≤ L) : ∑ i ∈ S, ↑((n i).factorization p) = ∑ ν ∈ Finset.Icc 1 L, ↑{i ∈ S | p ^ ν ∣ n i}.card

theorem NairTenenbaum.sum_log_smoothPart_eq_primePower_counts {ι : Type u_1} (S : Finset ι) (n : ι → ℕ+) {z : ℝ} (hz : 0 ≤ z) (L : ℕ → ℕ) (hL : ∀ p ∈ Finset.filter Nat.Prime (Finset.range (⌊z⌋₊ + 1)), ∀ i ∈ S, (↑(n i)).factorization p ≤ L p) : ∑ i ∈ S, Real.log ↑↑(smoothPart (n i) z) = ∑ p ∈ Finset.range (⌊z⌋₊ + 1) with Nat.Prime p, (∑ ν ∈ Finset.Icc 1 (L p), ↑{i ∈ S | p ^ ν ∣ ↑(n i)}.card) * Real.log ↑p