Erdős Problem 887

References:

• erdosproblems.com/887
• [ErRo97] Erdős, Paul and Rosenfeld, Moshe, The factor-difference set of integers. Acta Arith. (1997), 353--359.

theorem Erdos887.erdos_887.parts.i (C : ℝ) : C > 0 → ∀ᶠ (n : ℕ) in Filter.atTop, {d ∈ Finset.Ioo ⌊√↑n⌋₊ ⌈√↑n + C * ↑n ^ (1 / 4)⌉₊ | d ∣ n}.card ≤ sorry

Is there an absolute constant $K$ such that, for every $C > 0$, if $n$ is sufficiently large then $n$ has at most $K$ divisors in $(n^{\frac{1}{2}}, n^{\frac{1}{2}} + C n^{\frac{1}{4}})$.

theorem Erdos887.erdos_887.parts.ii : ∃ (K : ℕ), ∀ C > 0, ∀ᶠ (n : ℕ) in Filter.atTop, {d ∈ Finset.Ioo ⌊√↑n⌋₊ ⌈√↑n + C * ↑n ^ (1 / 4)⌉₊ | d ∣ n}.card ≤ K

Is there an absolute constant $K$ such that, for every $C > 0$, if $n$ is sufficiently large then $n$ has at most $K$ divisors in $(n^{\frac{1}{2}}, n^{\frac{1}{2}} + C n^{\frac{1}{4}})$.

theorem Erdos887.erdos_887.variants.rosenfeld_infinite : ∃ C > 0, Infinite ↑{n : ℕ | 4 ≤ {d ∈ Finset.Ioo ⌊√↑n⌋₊ ⌈√↑n + C * ↑n ^ (1 / 4)⌉₊ | d ∣ n}.card}

A question of Erdős and Rosenfeld, who proved that there are infinitely many $n$ with (at least) $4$ divisors in $(n^{\frac{1}{2}}, n^{\frac{1}{2}} + cn^{\frac{1}{4}})$.

theorem Erdos887.erdos_887.variants.rosenfeld_4 : IsGreatest {K : ℕ | ∃ C > 0, Infinite ↑{n : ℕ | K ≤ {d ∈ Finset.Ioo ⌊√↑n⌋₊ ⌈√↑n + C * ↑n ^ (1 / 4)⌉₊ | d ∣ n}.card}} 4

Erdős and Rosenfeld, ask whether $4$ is the best possible $K$ for the infinitude of $n$ with (at least) $K$ divisors in $(n^{\frac{1}{2}}, n^{\frac{1}{2}} + n^{\frac{1}{4}})$.