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 statement2 of 4

Is it true that there is a constant ckc_k such that for almost all n<xn < x we have gk(n)=cklog⁡x+o(log⁡x)g_k(n)=c_k\log x+o(\log x)?

FormalConjectures/ErdosProblems/400.leanErdos400.erdos_400.parts.ii7 linesExact file
True ↔  ∀ k ≥ 2,    ∃ c,      ∀ ε > 0,        Filter.Tendsto          (fun x => ↑{n ∈ Finset.Icc 1 x | |↑(Erdos400.g k n) - c * Real.log ↑x| ≤ ε * Real.log ↑x}.card / ↑x)          Filter.atTop (nhds 1)
OpenStatement only, no proof