Absolute convergence from summable local Euler tails

theorem NairTenenbaum.summable_multiplicative_of_local_tails {f : ℕ → ℝ} (hf : ∀ (n : ℕ), 0 ≤ f n) (hf1 : f 1 = 1) (hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) (hlocal : ∀ (p : ℕ), Nat.Prime p → Summable fun (k : ℕ) => f (p ^ k)) (htail : Summable fun (p : ℕ) => if Nat.Prime p then ∑' (k : ℕ), f (p ^ (k + 1)) else 0) : Summable f