Erdős Problem 897

Reference: erdosproblems.com/897

theorem erdos_897.parts.i : (∀ (f : ℕ → ℝ), (∀ a > 0, ∀ b > 0, a.Coprime b → f (a * b) = f a + f b) → Filter.limsup (fun (x : ℕ × ℕ) => match x with | (p, k) => ↑(f (p ^ k)) / ↑(Real.log (↑p ^ k))) (Filter.atTop ⊓ Filter.principal {(p, k) : ℕ × ℕ | Nat.Prime p}) = ⊤ → Filter.limsup (fun (n : ℕ) => (↑(f (n + 1)) - ↑(f n)) / ↑(Real.log ↑n)) Filter.atTop = ⊤) ↔ sorry

Let $f(n)$ be an additive function (so that $f(ab)=f(a)+f(b)$ if $(a,b)=1$ such that $\limsup_{p,k} f(p^k) \log(p^k) = ∞$. Is it true that $\limsup_n (f(n+1)−f(n))/ \log n = ∞$?

theorem erdos_897.parts.ii : (∀ (f : ℕ → ℝ), (∀ a > 0, ∀ b > 0, a.Coprime b → f (a * b) = f a + f b) → Filter.limsup (fun (x : ℕ × ℕ) => match x with | (p, k) => ↑(f (p ^ k)) / ↑(Real.log (↑p ^ k))) (Filter.atTop ⊓ Filter.principal {(p, k) : ℕ × ℕ | Nat.Prime p}) = ⊤ → Filter.limsup (fun (n : ℕ) => ↑(f (n + 1)) / ↑(f n)) Filter.atTop = ⊤) ↔ sorry

Let $f(n)$ be an additive function (so that $f(ab)=f(a)+f(b)$ if $(a,b)=1$) such that $\limsup_{p,k} f(p^k) \log(p^k) = ∞$. Is it true that $\limsup_n f(n+1)/ f(n) = ∞$?

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 : ℝ), ∀ (n : ℕ), |f n - c * Real.log ↑n| ≤ O

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 arthemetic function. Symposia Math. (1970), 45-47.

theorem erdos_897.variants.parts.i : (∀ (f : ℕ → ℝ), (∀ a > 0, ∀ b > 0, a.Coprime b → f (a * b) = f a + f b) → Filter.limsup (fun (x : ℕ × ℕ) => match x with | (p, k) => ↑(f (p ^ k)) / ↑(Real.log (↑p ^ k))) (Filter.atTop ⊓ Filter.principal {(p, k) : ℕ × ℕ | Nat.Prime p}) = ⊤ → ((∀ (k p : ℕ), Nat.Prime p → f (p ^ k) = f p) ∨ ∀ (k p : ℕ), Nat.Prime p → f (p ^ k) = ↑k * f p) → Filter.limsup (fun (n : ℕ) => (↑(f (n + 1)) - ↑(f n)) / ↑(Real.log ↑n)) Filter.atTop = ⊤) ↔ sorry

Let $f(n)$ be an additive function (so that $f(ab)=f(a)+f(b)$ if $(a,b)=1$) such that $\limsup_{p,k} f(p^k) \log(p^k) = ∞$ and $f(p^k) = f(p)$ or $f(p^k) = kf(p)$. Is it true that $\limsup_n (f(n+1)−f(n))/ \log n = ∞$?

theorem erdos_897.variants.parts.ii : (∀ (f : ℕ → ℝ), (∀ a > 0, ∀ b > 0, a.Coprime b → f (a * b) = f a + f b) → Filter.limsup (fun (x : ℕ × ℕ) => match x with | (p, k) => ↑(f (p ^ k)) / ↑(Real.log (↑p ^ k))) (Filter.atTop ⊓ Filter.principal {(p, k) : ℕ × ℕ | Nat.Prime p}) = ⊤ → ((∀ (k p : ℕ), Nat.Prime p → f (p ^ k) = f p) ∨ ∀ (k p : ℕ), Nat.Prime p → f (p ^ k) = ↑k * f p) → Filter.limsup (fun (n : ℕ) => ↑(f (n + 1)) / ↑(f n)) Filter.atTop = ⊤) ↔ sorry

Let $f(n)$ be an additive function (so that $f(ab)=f(a)+f(b)$ if $(a,b)=1$) such that $\limsup_{p,k} f(p^k) \log(p^k) = ∞$ and $f(p^k) = f(p)$ or $f(p^k) = kf(p)$. Is it true that $\limsup_n f(n+1)/f(n) = ∞$?