Erdős Problem 886

References:

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

noncomputable def Erdos886.Erdos886Divisors (n : ℕ) (ε C : ℝ) : Finset ℕ

The set of divisors of $n$ in the interval $(n^{1/2}, n^{1/2} + n^{1/2-\epsilon})$.

Equations

• Erdos886.Erdos886Divisors n ε C = {d ∈ n.divisors | ↑n ^ (1 / 2) < ↑d ∧ ↑d < ↑n ^ (1 / 2) + C * ↑n ^ (1 / 2 - ε)}

theorem Erdos886.erdos_886 : sorry ↔ ∀ ε > 0, ∃ (K : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, (Erdos886Divisors n ε 1).card ≤ K

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)$?

Erdős attributes this conjecture to Ruzsa.

theorem Erdos886.erdos_886_variants_rosenfeld_infinite : {n : ℕ | 4 ≤ (Erdos886Divisors n (1 / 4) 16).card}.Infinite

Erdős and Rosenfeld [ErRo97] proved that there are infinitely many $n$ such that there are four divisors of $n$ in $(n^{1/2},n^{1/2}+16n^{1/4})$.

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

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}]$.