Wirsing [Wi70] proved that if $|f(n+1)−f(n)| ≤ C$ then $f(n) = c \log n + O(1)$ for some constant
$c$.
[Wi70] Wirsing, E., _A characterization of $\log n$ as an additive arithmetic function_.
Symposia Math. (1970), 45-47.
Actions
Submit a Proof
Have a proof attempt? Submit it for zero-trust verification.
theorem erdos_897.variants.log_growth
(f : ℕ → ℝ)
(hf : ∀ᵉ (a > 0) (b > 0), a.Coprime b → f (a * b) = f a + f b)
(C : ℝ) (hf' : ∀ n, |f (n+1) - f n| ≤ C) :
∃ c, ∃ (O : ℕ → ℝ), O =O[Filter.atTop] (1 : ℕ → ℝ) ∧
∀ n, f n ≤ c*Real.log n + O n
