Erdős problem 897 · problems.science

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 = ∞$ ?

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

897.lean

Retained formal statement5 of 5

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) = ∞$ ?

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

FormalConjectures/ErdosProblems/897.leanErdos897.erdos_897.variants.parts.ii11 linesExact file

1True ↔2  ∀ (f : ℕ → ℝ),3    (∀ a > 0, ∀ b > 0, a.Coprime b → f (a * b) = f a + f b) →4      Filter.limsup5            (fun x =>6              match x with7              | (p, k) => ↑(f (p ^ k)) / ↑(Real.log (↑p ^ k)))8            (Filter.atTop ⊓ Filter.principal {(p, k) | Nat.Prime p}) =9          ⊤ →10        ((∀ (k p : ℕ), Nat.Prime p → f (p ^ k) = f p) ∨ ∀ (k p : ℕ), Nat.Prime p → f (p ^ k) = ↑k * f p) →11          Filter.limsup (fun n => ↑(f (n + 1)) / ↑(f n)) Filter.atTop = ⊤

OpenStatement only, no proof

Sources

Search problems.science