Exponential bounds for local coefficients of a Dirichlet inverse

theorem NairTenenbaum.arithmeticFunction_mul_prime_pow (f g : ArithmeticFunction ℝ) {p : ℕ} (hp : Nat.Prime p) (k : ℕ) : (f * g) (p ^ k) = ∑ j ∈ Finset.range (k + 1), f (p ^ j) * g (p ^ (k - j))

theorem NairTenenbaum.inverse_prime_pow_exponential_bound {f g : ArithmeticFunction ℝ} (hf1 : f 1 = 1) (hfg : f * g = 1) {p : ℕ} (hp : Nat.Prime p) {C : ℝ} (hC : 0 ≤ C) (hf : ∀ (k : ℕ), |f (p ^ k)| ≤ C ^ k) (k : ℕ) : |g (p ^ k)| ≤ (2 * C) ^ k

theorem NairTenenbaum.convolution_prime_pow_exponential_bound {f g : ArithmeticFunction ℝ} {p : ℕ} (hp : Nat.Prime p) {C : ℝ} (hC : 0 ≤ C) (hf : ∀ (k : ℕ), |f (p ^ k)| ≤ C ^ k) (hg : ∀ (k : ℕ), |g (p ^ k)| ≤ C ^ k) (k : ℕ) : |(f * g) (p ^ k)| ≤ (2 * C) ^ k