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 statement4 of 5

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) = ∞ and f(pk)=f(p)f(p^k) = f(p) or f(pk)=kf(p)f(p^k) = kf(p). Is it true that lim sup⁡n(f(n+1)−f(n))/log⁡n=∞\limsup_n (f(n+1)−f(n))/ \log n = ∞?

The known counterexample does not satisfy either of these extra hypotheses, so this variant remains open.

FormalConjectures/ErdosProblems/897.leanErdos897.erdos_897.variants.parts.i11 linesExact file
True ↔  ∀ (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 = ⊤
OpenStatement only, no proof