Skip to content

Erdős problem 942

Start work

Let h(n)h(n) count powerful integers in [n2,(n+1)2)[n^2, (n+1)^2). What is the extremal order of h(n)h(n)?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

942.lean

Retained formal statement1 of 3

Is there some constant c>0c > 0 such that h(n)<(log⁡n)c+o(1)h(n) < (\log n)^{c + o(1)} and, for infinitely many nn, h(n)>(log⁡n)c−o(1)h(n) > (\log n)^{c - o(1)}.

FormalConjectures/ErdosProblems/942.leanErdos942.erdos_9426 linesExact file
True ↔  ∃ c > 0,    ∃ o,      o =o[Filter.atTop] 1 ∧        (∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos942.erdos_942.h n) < Real.log ↑n ^ (c + o n)) ∧          {n | ↑(Erdos942.erdos_942.h n) > Real.log ↑n ^ (c - o n)}.Infinite
OpenStatement only, no proof