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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/897.lean

Formal Conjectures

FormalConjectures/ErdosProblems/897.leanErdos897.erdos_897.parts.i10 linesExact file
False ↔  ∀ (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 = ⊤
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:897
  • PLBY Lean proofsErdosProblems.Erdos897

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry