Skip to content

Erdős problem 897

Start work

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

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

897.lean

Retained formal statement3 of 5

Wirsing [Wi70] proved that if ∣f(n+1)−f(n)∣≤C|f(n+1)−f(n)| ≤ C then f(n)=clog⁡n+O(1)f(n) = c \log n + O(1) for some constant cc.

FormalConjectures/ErdosProblems/897.leanErdos897.erdos_897.variants.log_growth3 linesExact file
∀ (f : ℕ → ℝ),  (∀ a > 0, ∀ b > 0, a.Coprime b → f (a * b) = f a + f b) →    ∀ (C : ℝ), (∀ (n : ℕ), |f (n + 1) - f n| ≤ C) → ∃ c O, O =O[Filter.atTop] 1 ∧ ∀ (n : ℕ), f n ≤ c * Real.log ↑n + O n
SolvedStatement only, no proof