Erdős problem 886 · problems.science

Let $\epsilon>0$ . Is it true that, for all large $n$ , the number of divisors of $n$ in $(n^{1/2},n^{1/2}+n^{1/2-\epsilon})$ is $O_\epsilon(1)$ ?

Sources

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

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

886.lean

Retained formal statement2 of 3

Erdős and Rosenfeld [ErRo97] proved that, for any constant $C>0$ , all large $n$ have at most $1+C^2$ many divisors in $[n^{1/2}, n^{1/2}+Cn^{1/4}]$ .

FormalConjectures/ErdosProblems/886.leanErdos886.erdos_886.variants.rosenfeld_bound3 linesExact file

1∀ C > 0,2  ∀ᶠ (n : ℕ) in Filter.atTop,3    ↑{d ∈ n.divisors | ↑n ^ (1 / 2) ≤ ↑d ∧ ↑d ≤ ↑n ^ (1 / 2) + C * ↑n ^ (1 / 4)}.card ≤ 1 + C ^ 2

SolvedStatement only, no proof

Sources

Search problems.science