Is it true that, for every $\varepsilon > 0$, $h(N) = \sqrt N + O_{\varespilon}(N^\varespilon)

Erdős problem 30

Is it true that, for every $\varepsilon > 0$ , h(N) `Unparsed notation: = \sqrt N + O_{\varespilon}(N^\varespilon`)

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

30.lean

Retained formal statement1 of 1

Is it true that, for every $\varepsilon > 0$ , h(N) Unparsed notation: = \sqrt N + O_{\varespilon}(N^\varespilon)

FormalConjectures/ErdosProblems/30.leanErdos30.erdos_301 lineExact file

1True ↔ ∀ ε > 0, (fun N => ↑(Erdos30.h N) - √↑N) =O[Filter.atTop] fun N => ↑N ^ ε

OpenStatement only, no proof