Skip to content

Erdős problem 400

Start work

Erdős and Graham write that it is easy to show that gk(n)≪klog⁡ng_k(n) \ll_k \log n always, but the best possible constant is unknown.

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

400.lean

Retained formal statement1 of 4

Can one show that ∑n≤xgk(n)∼ckxlog⁡x\sum_{n\leq x}g_k(n) \sim c_k x\log x for some constant ckc_k?

FormalConjectures/ErdosProblems/400.leanErdos400.erdos_400.parts.i5 linesExact file
True ↔  ∀ k ≥ 2,    ∃ c,      Asymptotics.IsEquivalent Filter.atTop (fun x => ∑ n ∈ Finset.Icc 1 x, ↑(Erdos400.g k n)) fun x =>        c * ↑x * Real.log ↑x
OpenStatement only, no proof