Erdős Problem 887

Reference: erdosproblems.com/887

theorem Erdos887.erdos_887 (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.variant_i : ∃ (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.variant_ii : Infinite ↑{n : ℤ | {d ∈ Finset.Ioo ⌊√↑n⌋ ⌈√↑n + ↑n ^ (1 / 4)⌉ | d ∣ n}.card = 4}

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

theorem Erdos887.erdos_887.variant_iii : IsGreatest {K : ℕ | Infinite ↑{n : ℤ | {d ∈ Finset.Ioo ⌊√↑n⌋ ⌈√↑n + ↑n ^ (1 / 4)⌉ | d ∣ n}.card = K}} 4

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