Erdős problem 400 · problems.science

Erdős and Graham write that it is easy to show that $g_k(n) \ll_k \log n$ always, but the best possible constant is unknown.

Sources

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

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

400.lean

Retained formal statement2 of 4

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

FormalConjectures/ErdosProblems/400.leanErdos400.erdos_400.parts.ii7 linesExact file

1True ↔2  ∀ k ≥ 2,3    ∃ c,4      ∀ ε > 0,5        Filter.Tendsto6          (fun x => ↑{n ∈ Finset.Icc 1 x | |↑(Erdos400.g k n) - c * Real.log ↑x| ≤ ε * Real.log ↑x}.card / ↑x)7          Filter.atTop (nhds 1)

OpenStatement only, no proof

Sources

Search problems.science